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

From cLab
Jump to: navigation, search
(Create stub)
 
(Started writing)
Line 1: Line 1:
This is a placeholder for the discussion of how to encode coinductive types into MLTT with inductive types and the related problems.
+
== Introduction ==
 +
 
 +
Barr has shown in <ref>M. Barr, “Terminal coalgebras in well-founded set theory,” Theoretical Computer Science, vol. 114, no. 2, pp. 299–315, 1993.</ref> 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:
 +
<pre>
 +
data Poly : Set₁ where
 +
  _▹_ : (A : Set) (B : A → Set) → Poly
 +
</pre>
 +
We define an interpretation of polynomials as functors, where ⟦_⟧ is the action on other types and ⟦_⟧₁ is the action on terms.
 +
<pre>
 +
⟦_⟧ : 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)))
 +
</pre>
 +
In more standard notation we have  <math>⟦ A ▹ B ⟧(X) = \Sigma a : A. X^{B_a}</math>.
 +
 
 +
 
 +
</definition>
 +
(Weakly) initial algebras for polynomial functors are called ''W-types'', whereas (weakly) final coalgebras for these are called ''M-types''.
 +
 
 +
 
 +
== References ==
 +
<references/>

Revision as of 10:57, 21 January 2016

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, where ⟦_⟧ is the action on other 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)))

In more standard notation we have [math]⟦ A ▹ B ⟧(X) = \Sigma a : A. X^{B_a}[/math].


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


References

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