# Difference between revisions of "Type Theoretic Interpretation of the Final Chain"

m (Naturals are not predefined any more) |
m (Enable syntax highlighting) |
||

Line 17: | Line 17: | ||

A ''polynomial'' P is a pair A ▹ B with A : Set and B : A → Set, that is, | A ''polynomial'' P is a pair A ▹ B with A : Set and B : A → Set, that is, | ||

if P : Poly: | if P : Poly: | ||

− | < | + | <syntaxhighlight lang="agda"> |

data Poly : Set₁ where | data Poly : Set₁ where | ||

_▹_ : (A : Set) (B : A → Set) → Poly | _▹_ : (A : Set) (B : A → Set) → Poly | ||

− | </ | + | </syntaxhighlight> |

+ | |||

We define an interpretation of polynomials as functors by | We define an interpretation of polynomials as functors by | ||

<math>⟦ A ▹ B ⟧(X) = \Sigma a : A. X^{B_a}</math> and | <math>⟦ A ▹ B ⟧(X) = \Sigma a : A. X^{B_a}</math> and | ||

<math>⟦ A ▹ B ⟧(f) = [\lambda u \in X^{B_a}. f \circ u]_{a : A}</math>. | <math>⟦ A ▹ B ⟧(f) = [\lambda u \in X^{B_a}. f \circ u]_{a : A}</math>. | ||

In Agda, we define two actions: ⟦_⟧ is the action on types and ⟦_⟧₁ is the action on terms. | In Agda, we define two actions: ⟦_⟧ is the action on types and ⟦_⟧₁ is the action on terms. | ||

− | < | + | <syntaxhighlight lang="agda"> |

⟦_⟧ : Poly → Set → Set | ⟦_⟧ : Poly → Set → Set | ||

⟦ A ▹ B ⟧ X = Σ[ a ∈ A ] (B a → X) | ⟦ A ▹ B ⟧ X = Σ[ a ∈ A ] (B a → X) | ||

Line 31: | Line 32: | ||

⟦_⟧₁ : (P : Poly) → ∀{X Y} → (X → Y) → (⟦ P ⟧ X → ⟦ P ⟧ Y) | ⟦_⟧₁ : (P : Poly) → ∀{X Y} → (X → Y) → (⟦ P ⟧ X → ⟦ P ⟧ Y) | ||

⟦ A ▹ B ⟧₁ f (a , α) = (a , (λ x → f (α x))) | ⟦ A ▹ B ⟧₁ f (a , α) = (a , (λ x → f (α x))) | ||

− | </ | + | </syntaxhighlight> |

(Weakly) initial algebras for polynomial functors are called ''W-types'', whereas (weakly) final coalgebras for these are called ''M-types''. | (Weakly) initial algebras for polynomial functors are called ''W-types'', whereas (weakly) final coalgebras for these are called ''M-types''. | ||

</definition> | </definition> | ||

Line 38: | Line 39: | ||

We can also see <math>P^*</math> as the set of trees over the signature P, where we may mark leaves with a variable for which we can substitute other trees. | We can also see <math>P^*</math> as the set of trees over the signature P, where we may mark leaves with a variable for which we can substitute other trees. | ||

Thus <math>P^*</math> is given by | Thus <math>P^*</math> is given by | ||

− | < | + | <syntaxhighlight lang="agda"> |

data _* (P : Poly) : Set where | data _* (P : Poly) : Set where | ||

sup : ⟦ P ⟧ (P *) ⊎ ⊤ → P * | sup : ⟦ P ⟧ (P *) ⊎ ⊤ → P * | ||

− | </ | + | </syntaxhighlight> |

That is, <math>P^*</math> has one constructor sup that takes either a label and a branching map for the subtrees or a variable, and assembles these into one tree. | That is, <math>P^*</math> has one constructor sup that takes either a label and a branching map for the subtrees or a variable, and assembles these into one tree. | ||

Line 49: | Line 50: | ||

We define a relation '''extends''' on <math>P^*</math>, such that T '''extends''' S if we can find trees that we can substitute at the leaves of S to obtain T. | We define a relation '''extends''' on <math>P^*</math>, such that T '''extends''' S if we can find trees that we can substitute at the leaves of S to obtain T. | ||

This relation is defined inductively as follows. | This relation is defined inductively as follows. | ||

− | < | + | <syntaxhighlight lang="agda"> |

_extends_ : ∀{P} → P * → P * → Set | _extends_ : ∀{P} → P * → P * → Set | ||

_extends_ {A ▹ B} (sup (inj₁ (a' , β))) (sup (inj₁ (a , α))) | _extends_ {A ▹ B} (sup (inj₁ (a' , β))) (sup (inj₁ (a , α))) | ||

Line 56: | Line 57: | ||

sup (inj₁ x) extends sup (inj₂ _) = ⊤ | sup (inj₁ x) extends sup (inj₂ _) = ⊤ | ||

sup (inj₂ _) extends sup (inj₂ _) = ⊥ | sup (inj₂ _) extends sup (inj₂ _) = ⊥ | ||

− | </ | + | </syntaxhighlight> |

This data type essentially states that T '''extends''' S if either T is non-trivial while S is a variable (so we can substitute T for the variable), if both trees are variables, or both are trees with the same root and related subtrees. | This data type essentially states that T '''extends''' S if either T is non-trivial while S is a variable (so we can substitute T for the variable), if both trees are variables, or both are trees with the same root and related subtrees. | ||

Next, we define '''PreApprox''', which are sequences over <math>P^*</math>, and we characterise the converging sequences and non-empty trees. | Next, we define '''PreApprox''', which are sequences over <math>P^*</math>, and we characterise the converging sequences and non-empty trees. | ||

− | < | + | <syntaxhighlight lang="agda"> |

PreApprox : Poly → Set | PreApprox : Poly → Set | ||

PreApprox P = ℕ → P * | PreApprox P = ℕ → P * | ||

Line 70: | Line 71: | ||

non-empty (sup (inj₁ x)) = ⊤ | non-empty (sup (inj₁ x)) = ⊤ | ||

non-empty (sup (inj₂ _)) = ⊥ | non-empty (sup (inj₂ _)) = ⊥ | ||

− | </ | + | </syntaxhighlight> |

This allows us now to define the encoding <math>P^{\infty}</math> of the (weakly) final coalgebra for a polynomial P by | This allows us now to define the encoding <math>P^{\infty}</math> of the (weakly) final coalgebra for a polynomial P by | ||

− | < | + | <syntaxhighlight lang="agda"> |

_∞ : Poly → Set | _∞ : Poly → Set | ||

P ∞ = Σ[ u ∈ PreApprox P ] (non-empty (u 0) × converges u) | P ∞ = Σ[ u ∈ PreApprox P ] (non-empty (u 0) × converges u) | ||

− | </ | + | </syntaxhighlight> |

One can then show that this is indeed a coalgebra for ⟦ P ⟧, that is, we have a map | One can then show that this is indeed a coalgebra for ⟦ P ⟧, that is, we have a map | ||

− | < | + | <syntaxhighlight lang="agda"> |

out : ∀{P} → P ∞ → ⟦ P ⟧ (P ∞). | out : ∀{P} → P ∞ → ⟦ P ⟧ (P ∞). | ||

out {A ▹ B} (u , ne , conv) = (a , α) | out {A ▹ B} (u , ne , conv) = (a , α) | ||

where ... | where ... | ||

− | </ | + | </syntaxhighlight> |

The idea to define this map is as follows. | The idea to define this map is as follows. | ||

First, we can use for ''a'' the label of the root of the first tree in the sequence because u(0) this tree is non-empty (witnessed by ne). | First, we can use for ''a'' the label of the root of the first tree in the sequence because u(0) this tree is non-empty (witnessed by ne). | ||

Line 92: | Line 93: | ||

Moreover, we also get a corecursion principle for <math>P^{\infty}</math>: | Moreover, we also get a corecursion principle for <math>P^{\infty}</math>: | ||

− | < | + | <syntaxhighlight lang="agda"> |

corec : ∀{P} {C : Set} → (C → ⟦ P ⟧ C) → (C → P ∞) | corec : ∀{P} {C : Set} → (C → ⟦ P ⟧ C) → (C → P ∞) | ||

− | </ | + | </syntaxhighlight> |

The idea here is that ''corec f c'' is a sequence <math>(v_{n})_{n \in \N}</math> such that <math>v_n</math> is the tree obtained by the n-fold iteration of f starting at c. | The idea here is that ''corec f c'' is a sequence <math>(v_{n})_{n \in \N}</math> such that <math>v_n</math> is the tree obtained by the n-fold iteration of f starting at c. | ||

This sequence is clearly converging and starts with a non-empty tree. | This sequence is clearly converging and starts with a non-empty tree. |

## Revision as of 15:52, 21 January 2016

## Contents

## Introduction

Barr has shown in ^{[1]} that final coalgebras can be constructed as the Cauchy completion of initial algebras.
We will show in this article how this construction can be carried out in an intuitionistic type theory like Martin-Löf type theory.
Of course, we cannot expect to get a final coalgebra, but only a weakly final one.
However, as it turns out, we can only prove that the coinductive extension (corecursion) is a homomorphism up to bisimilarity, and not up to computational equality.
The latter can be proved if we had function extensionality.

All definitions and proofs in this article will be given in Agda code.

## Polynomials, W-Types and M-types

For simplicity, we restrict ourselves to polynomial functors.
These are given as follows.
<definition id="polynomial-functor">
A *polynomial* P is a pair A ▹ B with A : Set and B : A → Set, that is,
if P : Poly:

```
data Poly : Set₁ where
_▹_ : (A : Set) (B : A → Set) → Poly
```

We define an interpretation of polynomials as functors by

and . In Agda, we define two actions: ⟦_⟧ is the action on types and ⟦_⟧₁ is the action on terms.```
⟦_⟧ : Poly → Set → Set
⟦ A ▹ B ⟧ X = Σ[ a ∈ A ] (B a → X)
⟦_⟧₁ : (P : Poly) → ∀{X Y} → (X → Y) → (⟦ P ⟧ X → ⟦ P ⟧ Y)
⟦ A ▹ B ⟧₁ f (a , α) = (a , (λ x → f (α x)))
```

(Weakly) initial algebras for polynomial functors are called *W-types*, whereas (weakly) final coalgebras for these are called *M-types*.
</definition>

Given a polynomial P, we interpret it as a signature and define

to be the type of terms with one variable, which marks the holes of such a term. We can also see as the set of trees over the signature P, where we may mark leaves with a variable for which we can substitute other trees. Thus is given by```
data _* (P : Poly) : Set where
sup : ⟦ P ⟧ (P *) ⊎ ⊤ → P *
```

That is,

has one constructor sup that takes either a label and a branching map for the subtrees or a variable, and assembles these into one tree.## Cauchy sequences of finite trees

The first step to the construction of M-types from W-types is to define what it means for a sequence of finite trees to converge.
We define a relation **extends** on , such that T **extends** S if we can find trees that we can substitute at the leaves of S to obtain T.
This relation is defined inductively as follows.

```
_extends_ : ∀{P} → P * → P * → Set
_extends_ {A ▹ B} (sup (inj₁ (a' , β))) (sup (inj₁ (a , α)))
= Σ[ e ∈ a' ≡ a ] (∀ (b : B a') → (β b) extends α (subst B e b))
sup (inj₂ _) extends sup (inj₁ _) = ⊥
sup (inj₁ x) extends sup (inj₂ _) = ⊤
sup (inj₂ _) extends sup (inj₂ _) = ⊥
```

This data type essentially states that T **extends** S if either T is non-trivial while S is a variable (so we can substitute T for the variable), if both trees are variables, or both are trees with the same root and related subtrees.

Next, we define **PreApprox**, which are sequences over , and we characterise the converging sequences and non-empty trees.

```
PreApprox : Poly → Set
PreApprox P = ℕ → P *
converges : ∀{P} → PreApprox P → Set
converges u = ∀ n → u (1 + n) extends u n
non-empty : ∀{P} → P * → Set
non-empty (sup (inj₁ x)) = ⊤
non-empty (sup (inj₂ _)) = ⊥
```

This allows us now to define the encoding

of the (weakly) final coalgebra for a polynomial P by```
_∞ : Poly → Set
P ∞ = Σ[ u ∈ PreApprox P ] (non-empty (u 0) × converges u)
```

One can then show that this is indeed a coalgebra for ⟦ P ⟧, that is, we have a map

```
out : ∀{P} → P ∞ → ⟦ P ⟧ (P ∞).
out {A ▹ B} (u , ne , conv) = (a , α)
where ...
```

The idea to define this map is as follows.
First, we can use for *a* the label of the root of the first tree in the sequence because u(0) this tree is non-empty (witnessed by ne).
Second, we know from convergence that all trees in the sequence have *a* as root label.
This allows us to now define :
Put , where is the subtree at branch b of .
All are non-empty and convergence of follows from convergence of *u*.

Moreover, we also get a corecursion principle for

:`corec : ∀{P} {C : Set} → (C → ⟦ P ⟧ C) → (C → P ∞)`

The idea here is that *corec f c* is a sequence such that is the tree obtained by the n-fold iteration of f starting at c.
This sequence is clearly converging and starts with a non-empty tree.

## The Problem

Having defined all of this, we would now expect that *corec f* is actually a coalgebra homomorphism, i.e., that *out (corec f c) = ⟦ P ⟧₁ (corec f) (f c)*.
However, it is fairly clear that this equality (up to reduction) cannot hold in an intensional type theory, as both sides are functions.
Thus, the best we can hope for is to define equality (say ) on **PreApprox** to be extensional equality of functions but then we lose replacement .
This will force us to restrict to predicates that satisfy replacement for .
Hence, we need to reason using Setoids, which becomes very cumbersome.

## Conclusion

The conclusion of this is, so far, that from a practical perspective native coinductive types are better as we obtain from corecursion a coalgebra homomorphism up to syntactic reduction, and not just up to some external equality. This makes them more usable in practice.

## References

- ↑ M. Barr, “Terminal coalgebras in well-founded set theory,” Theoretical Computer Science, vol. 114, no. 2, pp. 299–315, 1993.