Type Theoretic Interpretation of the Final Chain

From cLab
Revision as of 14:29, 21 January 2016 by H.basold (talk | contribs) (Proper content)
Jump to: navigation, search

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 [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]. 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 [math]P^*[/math] to be the type of terms with one variable, which marks the holes of such a term. 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

data _* (P : Poly) : Set where
  sup : ⟦ P ⟧ (P *) ⊎ ⊤ → P *

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.

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 [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.

_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 [math]P^*[/math], 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 [math]P^{\infty}[/math] 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 [math]\alpha : B_a \to P^{\infty}[/math]: Put [math]\alpha(b) = (v_{b,n})_{n \in \N}[/math], where [math]v_{b,n}[/math] is the subtree at branch b of [math]u(n)[/math]. All [math]\alpha(b)_0[/math] are non-empty and convergence of [math]\alpha(b)[/math] follows from convergence of u.

Moreover, we also get a corecursion principle for [math]P^{\infty}[/math]:

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

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.

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 [math]\approx[/math]) on PreApprox to be extensional equality of functions but then we lose replacement [math]x = y \Rightarrow P(x) \Rightarrow P(y)[/math]. This will force us to restrict to predicates that satisfy replacement for [math]\approx[/math]. 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

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