-- * Prelude module InductionFromFold where open import Function open import Data.Unit open import Data.Empty open import Data.Sum open import Data.Product open import Data.Nat open import Relation.Binary hiding (_⇒_) open import Relation.Binary.PropositionalEquality infixr 7 _⇒_ _⇒_ : {I : Set} → (I → Set) → (I → Set) → Set A ⇒ B = {i : _} → A i → B i -- Let's work in a sufficiently extensional type theory: postulate extensionality : {A : Set}{B : A → Set}{f g : (a : A) → B a} → ((x : A) → (f x ≡ g x)) → (f ≡ g) -- Indeed, the constructions in this paper are derived from viewing -- least fixpoint as strong initial objects, while an intensional -- setting only gives weak initials. -- * W-types -- For convenience, I'm going to work on a specific family of -- functors: the polynomial functors, also known as -- "containers". Their least fixpoint corresponds exactly to the -- W-types of Martin-Lof. -- Remark: containers are defined on any LCCC. Here, we are going to -- work on Set, for simplicity. We could consider polynomial functors -- between slices of Set, thus describing inductive *families* -- (ie. indexed W-types). Or, if there is such a thing, the equivalent -- in the homotopic framework. -- ** Definition -- Containers let us describe the so-called "signature functor" of our -- datatype, ie. the set of operations and their arity. record Cont : Set1 where field Shape : Set Pos : Shape → Set open Cont -- Its meaning is made clear through the semantics-giving extension -- function below. -- ** Extension of a container -- The extension of a container computes the (strictly) positive -- functor described by the container. ⟦_⟧ : Cont → Set → Set ⟦ φ ⟧ X = Σ[ s ∶ Shape φ ] ((p : Pos φ s) → X) -- Hence the name polynomial functor: it's a sum indexed by Shape φ of monomials of -- exponent P φ s. -- Exercises: -- * Write the container representing Nat -- * Write the container representing node-labelled binary trees -- * Initial algebra semantics -- ** External fixpoint -- Being strictly positive, these functors admits an initial -- algebra. Agda is very happy to notice it. data μ (φ : Cont) : Set where con : (x : ⟦ φ ⟧ (μ φ)) → μ φ -- Categorically, reading ⟦ φ ⟧ as a functor F, this is nothing but -- that initial algebra: -- -- con : F (μ F) → μ F -- Exercises: -- * Take the fixpoint of Nat and binary trees -- * Check you've indeed described Nat and trees -- * In particular, write their constructors and convince yourself -- that they are the only constructors -- *** Catamorphism: existence -- Pursuing on the categorical analogy, the existence of the initial -- algebra tells us that for any ⟦ φ ⟧-algebra (X, α : ⟦ φ ⟧ X → X), -- there exists a (unique) morphism foldCont α from μ φ to X: foldCont : {φ : Cont}{X : Set} (α : ⟦ φ ⟧ X → X) → μ φ → X foldCont m (con (s , f)) = m (s , \p → foldCont m (f p)) -- Remark: in type theory, we have the existence of the morphism: we -- build the damned thing. However, without extensionality, there is -- no way to prove uniqueness. Our initial algebras are weak. In this -- presentation we shall need unicity: we have therefore postulated -- extensionality and the resulting construction is computationally -- inert :-( -- Exercise: -- * Implement addition of natural numbers using foldCont -- *** Catamorphism: unicity -- I'm not going to prove unicity per se (which would amount to prove -- η for inductive elimination). Instead, I just need to prove that -- foldCont con is equal to the identity (ie. η in the specific case -- of the identity, in a sense). fold∙con≡id : {φ : Cont} → (x : μ φ) → foldCont con x ≡ x fold∙con≡id {φ} (con (sh , pos)) = cong (\p → con (sh , p)) (extensionality (λ p → fold∙con≡id (pos p))) -- * Induction -- The material in this section is a mixture of Bart Jacobs' Yellow -- Pages, Claudio Hermida's PhD thesis and, my favorite, Clément Fumex -- PhD thesis. Clément is the one that explained these things to -- me. Any mistake would be my original contribution. -- I've tried to stick to the categorical terminology and notations, as -- much as Agda would let me. -- ** Comprehension -- The comprehension takes a predicate P and make it a set, the -- obvious way: ⟨_⟩ : {X : Set} → (P : X → Set) → Set ⟨_⟩ P = Σ[ x ∶ _ ] P x -- ** Canonical lifting -- The canonical lifting takes a functor on Set, here presented as a -- container φ, and "lift" it as a functor on predicates, -- ie. functions X → Set: infix 70 _^_ _^_ : (φ : Cont){X : Set}(P : X → Set) → ⟦ φ ⟧ X → Set (φ ^ P) (sh , pos) = (p : Pos φ sh) → P (pos p) -- Intuitively, for a predicate P, the lifting asks that all -- sub-branches of the tree-like structure ⟦ φ ⟧ X satisfy the -- predicate P. This is computing the good ol' induction hypothesis! -- Exercises: -- * Compute the lifting for Nat and binary trees -- * Verify that these are indeed the induction hypothesis -- ** Induction, implemented by a fold -- You might have seen it coming by now: we are going to obtain -- induction by using the initial φ-algebras. To do so, from the -- induction step α : φ^ P ⇒ P ∘ con, we define a φ-algebra: -- -- ( ⟨ P ⟩, α^ : ⟦ φ ⟧ ⟨ P ⟩ → ⟨ P ⟩ ) -- -- As follow: ind : {φ : Cont} (P : μ φ → Set) (α : φ ^ P ⇒ P ∘ con) → (x : μ φ) → ⟨ P ⟩ ind {φ} P α = foldCont {X = ⟨ P ⟩} α^ where α^ : ⟦ φ ⟧ ⟨ P ⟩ → ⟨ P ⟩ α^ (sh , pos) = (con (sh , proj₁ ∘ pos)) , α {sh , proj₁ ∘ pos} (proj₂ ∘ pos) -- Recall that ⟨ P ⟩ is a pair of an X and a P-witness for that X: our -- algebra thus computes the identity for the first element of that -- pair, while unfolding the inductive step on the proof side. Doing -- so, we *know* (because we defined it so) that the result ⟨ P ⟩ is a -- proof of P for the x we started with. -- Remark: I've used a slightly obscure syntax to denote the inductive -- step α : φ ^ P ⇒ P ∘ con. Put explicitly, here is the beast: -- -- α : {xs : ⟦ φ ⟧ (μ φ)} → φ^ P xs → P (con xs) -- -- Intuitively, this functions is nothing but the traditional -- inductive step: for an (here, implicit) object xs : ⟦ φ ⟧ (μ φ), we -- are given φ^ P xs -- the induction hypothesis -- and we are asked -- to prove P (con xs). -- Exercise: -- * Unfold α on Nat and binary trees -- * Check that these are indeed the good ol' inductive steps -- ** Proof: the result of ind is a proof on the initial x: -- To prove this, we proceed in two steps. First, we prove that the -- first element of the computed pair is equal to the folding the -- initial algebra: proj₁∘ind≡fold∙con : {φ : Cont} (P : μ φ → Set) (α : φ ^ P ⇒ P ∘ con) (x : μ φ) → proj₁ (ind P α x) ≡ foldCont con x proj₁∘ind≡fold∙con {φ} P α (con (sh , pos)) = cong (\x → con (sh , x)) (extensionality help) where help : (x : Pos φ sh) → ((proj₁ (ind P α (pos x))) ≡ foldCont con (pos x)) help x = proj₁∘ind≡fold∙con P α (pos x) -- The second step is then to prove by transitivity the desired -- result: the first element of the pair is actually the one we start -- with: proj₁∘ind≡id : {φ : Cont} (P : μ φ → Set) (α : φ ^ P ⇒ P ∘ con) (x : μ φ) → proj₁ (ind P α x) ≡ x proj₁∘ind≡id {φ} P α x = trans (proj₁∘ind≡fold∙con P α x) (fold∙con≡id x) -- * Induction -- So, what is induction? It's simply the second projection of ind! inductionCont : {φ : Cont} (P : μ φ → Set) (α : φ ^ P ⇒ P ∘ con) (x : μ φ) → P x inductionCont P α x = subst P (proj₁∘ind≡id P α x) (proj₂ (ind P α x)) -- Remark: to fix the type, we have to substitute by our -- proofs. Sadly, our proofs are non canonical: they rely on the -- extensionality axiom. Consequently, this definition is -- computationally inert. That's why doing category theory in type -- theory is rarely a good idea ;-)