------------------------------------------------------------------------ -- An implementation of "A Unifying Approach to Recursive and -- Co-recursive Definitions" by Pietro Di Gianantonio and Marino -- Miculan ------------------------------------------------------------------------ -- See the paper for more explanations. module Contractive where open import Relation.Unary open import Relation.Binary import Relation.Binary.EqReasoning as EqR open import Induction.WellFounded open import Function open import Level hiding (lift) -- Well-founded orders. record IsWellFoundedOrder {A} (_<_ : Rel A zero) : Set where field trans : Transitive _<_ isWellFounded : Well-founded _<_ -- Ordered families of equivalences. record OFE : Set1 where field Carrier : Set Domain : Set _<_ : Rel Carrier zero isWellFoundedOrder : IsWellFoundedOrder _<_ Eq : Carrier → Rel Domain zero isEquivalence : ∀ a → IsEquivalence (Eq a) open IsWellFoundedOrder isWellFoundedOrder public open All isWellFounded public setoid : Carrier → Setoid _ _ setoid a = record { Carrier = Domain ; _≈_ = Eq a ; isEquivalence = isEquivalence a } module EqReasoning {a : Carrier} where open EqR (setoid a) public open Setoid (setoid a) public using (refl; sym) -- The set of predecessors of a. ↓ : Carrier → Carrier → Set ↓ a = λ a' → a' < a -- The intersection of all the equivalences. _≅_ : Rel Domain zero x ≅ y = ∀ a → Eq a x y Family : (Carrier → Set) → Set Family I = ∀ x → x ∈ I → Domain lift : ∀ {I} → (Carrier → Domain) → Family I lift P = λ x _ → P x IsCoherent : ∀ {I} → Family I → Set IsCoherent {I} fam = ∀ {a' a} (a'∈I : a' ∈ I) (a∈I : a ∈ I) → a' < a → Eq a' (fam a' a'∈I) (fam a a∈I) IsLimit : ∀ {I} → Family I → Domain → Set IsLimit {I} fam y = ∀ {a'} (a'∈I : a' ∈ I) → Eq a' (fam a' a'∈I) y IsContractive : (Domain → Domain) → Set IsContractive F = ∀ {x y a} → (∀ {a'} → a' < a → Eq a' x y) → Eq a (F x) (F y) -- Complete ordered families of equivalences. record COFE : Set1 where field ofe : OFE open OFE ofe field limU : (Carrier → Domain) → Domain isLimitU : ∀ {fam} → IsCoherent {U} (lift fam) → IsLimit {U} (lift fam) (limU fam) lim↓ : ∀ a → Family (↓ a) → Domain isLimit↓ : ∀ a {fam : Family (↓ a)} → IsCoherent fam → IsLimit fam (lim↓ a fam) open OFE ofe public -- Contractive functions over complete ordered families have -- fixpoints. record ContractiveFun (cofe : COFE) : Set where open COFE cofe field F : Domain → Domain isContractive : IsContractive F open EqReasoning -- The fixpoint is the limit of the following family. fam : Carrier → Domain fam = wfRec _ (const Domain) (λ a rec → F (lim↓ a rec)) fixpoint : Domain fixpoint = limU fam -- I am not sure if this lemma can be proved without assuming some -- kind of proof irrelevance and/or extensionality. It is not -- central to the ideas developed here, though, so I leave it as a -- postulate. postulate unfold : ∀ a → fam a ≅ F (lim↓ a (lift fam)) -- The family is coherent in several ways. fam-isCoherent-↓ : ∀ a → IsCoherent {↓ a} (lift fam) fam-isCoherent-↓ = wfRec _ P step where P : Carrier → Set P a = IsCoherent {↓ a} (lift fam) step : ∀ a → WfRec _<_ P a → P a step a rec {c} {b} c