------------------------------------------------------------------------ -- An investigation of nested fixpoints of the form μX.νY.… in Agda ------------------------------------------------------------------------ module MuNu where open import Coinduction import Data.Colist as Colist open import Data.Digit open import Data.Empty open import Data.List using (List; _∷_; []) open import Data.Product open import Data.Stream open import Relation.Binary.PropositionalEquality open import Relation.Nullary -- Christophe Raffalli discusses (essentially) the type μO. νZ. Z + O -- in his thesis. If Z is read as zero and O as one, then this type -- contains bit sequences of the form (0^⋆1)^⋆0^ω. -- It is interesting to note that currently it is not possible to -- encode this type directly in Agda. One might believe that the -- following definition should work. First we define the inner -- greatest fixpoint: data Z (O : Set) : Set where [0] : ∞ (Z O) → Z O [1] : O → Z O -- Then we define the outer least fixpoint: data O : Set where ↓ : Z O → O -- However, it is still possible to define values of the form (01)^ω: 01^ω : O 01^ω = ↓ ([0] (♯ [1] 01^ω)) -- The reason is the way the termination/productivity checker works: -- it accepts definitions by guarded corecursion as long as the guard -- contains at least one occurrence of ♯_, no matter how the types -- involved are defined. In effect ∞ has global reach. The mistake -- done above was believing that O is defined to be a least fixpoint. -- The type O really corresponds to νZ. μO. Z + O, i.e. (1^⋆0)^ω: data O′ : Set where [0] : ∞ O′ → O′ [1] : O′ → O′ mutual O→O′ : O → O′ O→O′ (↓ z) = ZO→O′ z ZO→O′ : Z O → O′ ZO→O′ ([0] z) = [0] (♯ ZO→O′ (♭ z)) ZO→O′ ([1] o) = [1] (O→O′ o) mutual O′→O : O′ → O O′→O o = ↓ (O′→ZO o) O′→ZO : O′ → Z O O′→ZO ([0] o) = [0] (♯ O′→ZO (♭ o)) O′→ZO ([1] o) = [1] (O′→O o) -- If O had actually encoded the type μO. νZ. Z + O, then we could -- have proved the following theorem: mutual ⟦_⟧O : O → Stream Bit ⟦ ↓ z ⟧O = ⟦ z ⟧Z ⟦_⟧Z : Z O → Stream Bit ⟦ [0] z ⟧Z = 0b ∷ ♯ ⟦ ♭ z ⟧Z ⟦ [1] o ⟧Z = 1b ∷ ♯ ⟦ o ⟧O Theorem : Set Theorem = ∀ o → ¬ (head ⟦ o ⟧O ≡ 0b × head (tail ⟦ o ⟧O) ≡ 1b × tail (tail ⟦ o ⟧O) ≈ ⟦ o ⟧O) -- This would have been unfortunate, though: inconsistency : Theorem → ⊥ inconsistency theorem = theorem 01^ω (refl , refl , proof) where proof : tail (tail ⟦ 01^ω ⟧O) ≈ ⟦ 01^ω ⟧O proof = 0b ∷ ♯ (1b ∷ ♯ proof) -- Using the following elimination principle we can prove the theorem: data ⇑ {O} (P : O → Set) : Z O → Set where [0] : ∀ {z} → ∞ (⇑ P (♭ z)) → ⇑ P ([0] z) [1] : ∀ {o} → P o → ⇑ P ([1] o) O-Elim : Set₁ O-Elim = (P : O → Set) → (∀ {z} → ⇑ P z → P (↓ z)) → (o : O) → P o theorem : O-Elim → Theorem theorem O-elim = O-elim P helper where P : O → Set P o = ¬ (head ⟦ o ⟧O ≡ 0b × head (tail ⟦ o ⟧O) ≡ 1b × tail (tail ⟦ o ⟧O) ≈ ⟦ o ⟧O) head-cong : ∀ {A} {xs ys : Stream A} → xs ≈ ys → head xs ≡ head ys head-cong (x ∷ xs≈) = refl tail-cong : ∀ {A} {xs ys : Stream A} → xs ≈ ys → tail xs ≈ tail ys tail-cong (x ∷ xs≈) = ♭ xs≈ helper : ∀ {z} → ⇑ P z → P (↓ z) helper ([1] p) (() , eq₂ , eq₃) helper ([0] p) (refl , eq₂ , eq₃) = hlp _ eq₂ (head-cong eq₃) (tail-cong eq₃) (♭ p) where hlp : ∀ z → head ⟦ z ⟧Z ≡ 1b → head (tail ⟦ z ⟧Z) ≡ 0b → tail (tail ⟦ z ⟧Z) ≈ ⟦ z ⟧Z → ⇑ P z → ⊥ hlp .([0] _) () eq₂ eq₃ ([0] p) hlp .([1] _) eq₁ eq₂ eq₃ ([1] p) = p (eq₂ , head-cong eq₃ , tail-cong eq₃) -- Fortunately it appears as if we cannot prove this elimination -- principle. The following code is not accepted by the termination -- checker: {- mutual O-elim : O-Elim O-elim P hyp (↓ z) = hyp (Z-elim P hyp z) Z-elim : (P : O → Set) → (∀ {z} → ⇑ P z → P (↓ z)) → (z : Z O) → ⇑ P z Z-elim P hyp ([0] z) = [0] (♯ Z-elim P hyp (♭ z)) Z-elim P hyp ([1] o) = [1] (O-elim P hyp o) -} -- If hyp were known to be contractive, then the code above would be -- correct (if not accepted by the termination checker). This is not -- the case in theorem above.