------------------------------------------------------------------------ -- An implementation of the Thue-Morse sequence ------------------------------------------------------------------------ -- The paper "Productivity of stream definitions" by Endrullis et al. -- (TCS 2010) uses a certain definition of the Thue-Morse sequence as -- a running example. -- Note that the code below makes use of the fact that Agda's -- termination checker allows "swapping of arguments", which was not -- mentioned when the termination checker was described in the paper -- "Beating the Productivity Checker Using Embedded Languages". -- However, it is easy to rewrite the code into a form which does not -- make use of swapping, at the cost of some code duplication. module ThueMorse where open import Coinduction open import Data.Bool using (Bool; not); open Data.Bool.Bool open import Data.Stream as S using (Stream; _≈_) open S.Stream; open S._≈_ open import Function open import Relation.Binary import Relation.Binary.PropositionalEquality as P import Relation.Binary.EqReasoning as EqReasoning private module SS {A : Set} = Setoid (S.setoid A) open module EqR {A : Set} = EqReasoning (S.setoid A) using (begin_; _∎) renaming (_≈⟨_⟩_ to _≈⟨_⟩′_) ------------------------------------------------------------------------ -- Chunks -- A value of type Chunks describes how a stream is generated. Note -- that an infinite sequence of empty chunks is not allowed. data Chunks : Set where -- Start the next chunk. next : (m : Chunks) → Chunks -- Cons an element to the current chunk. cons : (m : ∞ Chunks) → Chunks -- Equality of chunks. infix 4 _≈C_ data _≈C_ : Chunks → Chunks → Set where next : ∀ {m m′} (m≈m′ : m ≈C m′ ) → next m ≈C next m′ cons : ∀ {m m′} (m≈m′ : ∞ (♭ m ≈C ♭ m′)) → cons m ≈C cons m′ ------------------------------------------------------------------------ -- Chunk transformers tailC : Chunks → Chunks tailC (next m) = next (tailC m) tailC (cons m) = ♭ m mutual evensC : Chunks → Chunks evensC (next m) = next (evensC m) evensC (cons m) = cons (♯ oddsC (♭ m)) oddsC : Chunks → Chunks oddsC (next m) = next (oddsC m) oddsC (cons m) = evensC (♭ m) infixr 5 _⋎C_ -- Note that care is taken to create as few and large chunks as -- possible (see also _⋎W_). _⋎C_ : Chunks → Chunks → Chunks next m ⋎C next m′ = next (m ⋎C m′) -- Two chunks in, one out. next m ⋎C cons m′ = next (m ⋎C cons m′) cons m ⋎C m′ = cons (♯ (m′ ⋎C ♭ m)) ------------------------------------------------------------------------ -- Stream programs -- StreamP m A encodes programs which generate streams with chunk -- sizes given by m. infixr 5 _∷_ _⋎_ data StreamP : Chunks → Set → Set₁ where [_] : ∀ {m A} (xs : ∞ (StreamP m A)) → StreamP (next m) A _∷_ : ∀ {m A} (x : A) (xs : StreamP (♭ m) A) → StreamP (cons m) A tail : ∀ {m A} (xs : StreamP m A) → StreamP (tailC m) A evens : ∀ {m A} (xs : StreamP m A) → StreamP (evensC m) A odds : ∀ {m A} (xs : StreamP m A) → StreamP (oddsC m) A _⋎_ : ∀ {m m′ A} (xs : StreamP m A) (ys : StreamP m′ A) → StreamP (m ⋎C m′) A map : ∀ {m A B} (f : A → B) (xs : StreamP m A) → StreamP m B cast : ∀ {m m′ A} (ok : m ≈C m′) (xs : StreamP m A) → StreamP m′ A data StreamW : Chunks → Set → Set₁ where [_] : ∀ {m A} (xs : StreamP m A) → StreamW (next m) A _∷_ : ∀ {m A} (x : A) (xs : StreamW (♭ m) A) → StreamW (cons m) A program : ∀ {m A} → StreamW m A → StreamP m A program [ xs ] = [ ♯ xs ] program (x ∷ xs) = x ∷ program xs tailW : ∀ {m A} → StreamW m A → StreamW (tailC m) A tailW [ xs ] = [ tail xs ] tailW (x ∷ xs) = xs mutual evensW : ∀ {m A} → StreamW m A → StreamW (evensC m) A evensW [ xs ] = [ evens xs ] evensW (x ∷ xs) = x ∷ oddsW xs oddsW : ∀ {m A} → StreamW m A → StreamW (oddsC m) A oddsW [ xs ] = [ odds xs ] oddsW (x ∷ xs) = evensW xs infixr 5 _⋎W_ -- Note: Uses swapping of arguments. _⋎W_ : ∀ {m m′ A} → StreamW m A → StreamW m′ A → StreamW (m ⋎C m′) A [ xs ] ⋎W [ ys ] = [ xs ⋎ ys ] [ xs ] ⋎W (y ∷ ys) = [ xs ⋎ program (y ∷ ys) ] (x ∷ xs) ⋎W ys = x ∷ ys ⋎W xs mapW : ∀ {m A B} → (A → B) → StreamW m A → StreamW m B mapW f [ xs ] = [ map f xs ] mapW f (x ∷ xs) = f x ∷ mapW f xs castW : ∀ {m m′ A} → m ≈C m′ → StreamW m A → StreamW m′ A castW (next m≈m′) [ xs ] = [ cast m≈m′ xs ] castW (cons m≈m′) (x ∷ xs) = x ∷ castW (♭ m≈m′) xs whnf : ∀ {m A} → StreamP m A → StreamW m A whnf [ xs ] = [ ♭ xs ] whnf (x ∷ xs) = x ∷ whnf xs whnf (tail xs) = tailW (whnf xs) whnf (evens xs) = evensW (whnf xs) whnf (odds xs) = oddsW (whnf xs) whnf (xs ⋎ ys) = whnf xs ⋎W whnf ys whnf (map f xs) = mapW f (whnf xs) whnf (cast m≈m′ xs) = castW m≈m′ (whnf xs) mutual ⟦_⟧W : ∀ {m A} → StreamW m A → Stream A ⟦ [ xs ] ⟧W = ⟦ xs ⟧P ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧W ⟦_⟧P : ∀ {m A} → StreamP m A → Stream A ⟦ xs ⟧P = ⟦ whnf xs ⟧W ------------------------------------------------------------------------ -- The Thue-Morse sequence [ccn]ω : Chunks [ccn]ω = cons (♯ cons (♯ next [ccn]ω)) [cn]²[ccn]ω : Chunks [cn]²[ccn]ω = cons (♯ next (cons (♯ next [ccn]ω))) [cn]³[ccn]ω : Chunks [cn]³[ccn]ω = cons (♯ next [cn]²[ccn]ω) -- Explanation of the proof of lemma₁: -- -- odds [ccn]ω ≈ [cn]ω -- -- [cn]ω ⋎ [ccn]ω ≈ -- c ([ccn]ω ⋎ n[cn]ω) ≈ -- c c (n[cn]ω ⋎ cn[ccn]ω) ≈ -- c c n ([cn]ω ⋎ cn[ccn]ω) ≈ -- c c n c (cn[ccn]ω ⋎ n[cn]ω) ≈ -- c c n c c (n[cn]ω ⋎ n[ccn]ω) ≈ -- c c n c c n ([cn]ω ⋎ [ccn]ω) lemma₁ : oddsC [ccn]ω ⋎C [ccn]ω ≈C [ccn]ω lemma₁ = cons (♯ cons (♯ next (cons (♯ cons (♯ next lemma₁))))) -- Explanation of the proof of lemma: -- -- evens [cn]³[ccn]ω ≈ cnn[cn]ω -- tail [cn]³[ccn]ω ≈ n[cn]²[ccn]ω -- -- cnn[cn]ω ⋎ n[cn]²[ccn]ω ≈ -- c (n[cn]²[ccn]ω ⋎ nn[cn]ω) ≈ -- c n ([cn]²[ccn]ω ⋎ n[cn]ω) ≈ -- c n c (n[cn]ω ⋎ ncn[ccn]ω) ≈ -- c n c n ([cn]ω ⋎ cn[ccn]ω) ≈ -- c n c n c (cn[ccn]ω ⋎ n[cn]ω) ≈ -- c n c n c c (n[cn]ω ⋎ n[ccn]ω) ≈ -- c n c n c c n ([cn]ω ⋎ [ccn]ω) lemma : evensC [cn]³[ccn]ω ⋎C tailC [cn]³[ccn]ω ≈C [cn]²[ccn]ω lemma = cons (♯ next (cons (♯ next (cons (♯ cons (♯ next lemma₁)))))) thueMorse : StreamP [cn]³[ccn]ω Bool thueMorse = false ∷ [ ♯ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ] ------------------------------------------------------------------------ -- Equality programs infix 4 _≈[_]P_ _≈[_]W_ infixr 2 _≈⟨_⟩P_ _≈⟨_⟩_ data _≈[_]P_ : {A : Set} → Stream A → Chunks → Stream A → Set₁ where [_] : ∀ {m A} {xs ys : Stream A} (xs≈ys : ∞ (xs ≈[ m ]P ys)) → xs ≈[ next m ]P ys _∷_ : ∀ {m A} (x : A) {xs ys} (xs≈ys : ♭ xs ≈[ ♭ m ]P ♭ ys) → x ∷ xs ≈[ cons m ]P x ∷ ys tail : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) → S.tail xs ≈[ tailC m ]P S.tail ys evens : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) → S.evens xs ≈[ evensC m ]P S.evens ys odds : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) → S.odds xs ≈[ oddsC m ]P S.odds ys _⋎_ : ∀ {m m′ A} {xs xs′ ys ys′ : Stream A} (xs≈ys : xs ≈[ m ]P ys) (xs′≈ys′ : xs′ ≈[ m′ ]P ys′) → (xs ⟨ S._⋎_ ⟩ xs′) ≈[ m ⋎C m′ ]P (ys ⟨ S._⋎_ ⟩ ys′) map : ∀ {m A B} (f : A → B) {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) → S.map f xs ≈[ m ]P S.map f ys cast : ∀ {m m′ A} (ok : m ≈C m′) {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) → xs ≈[ m′ ]P ys _≈⟨_⟩P_ : ∀ {m A} xs {ys zs : Stream A} (xs≈ys : xs ≈[ m ]P ys) (ys≈zs : ys ≈ zs) → xs ≈[ m ]P zs _≈⟨_⟩_ : ∀ {m A} xs {ys zs : Stream A} (xs≈ys : xs ≈ ys) (ys≈zs : ys ≈[ m ]P zs) → xs ≈[ m ]P zs data _≈[_]W_ : {A : Set} → Stream A → Chunks → Stream A → Set₁ where [_] : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) → xs ≈[ next m ]W ys _∷_ : ∀ {m A} (x : A) {xs ys} (xs≈ys : ♭ xs ≈[ ♭ m ]W ♭ ys) → x ∷ xs ≈[ cons m ]W x ∷ ys program≈ : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈[ m ]P ys program≈ [ xs≈ys ] = [ ♯ xs≈ys ] program≈ (x ∷ xs≈ys) = x ∷ program≈ xs≈ys tail-congW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → S.tail xs ≈[ tailC m ]W S.tail ys tail-congW [ xs≈ys ] = [ tail xs≈ys ] tail-congW (x ∷ xs≈ys) = xs≈ys mutual evens-congW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → S.evens xs ≈[ evensC m ]W S.evens ys evens-congW [ xs≈ys ] = [ evens xs≈ys ] evens-congW (x ∷ xs≈ys) = x ∷ odds-congW xs≈ys odds-congW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → S.odds xs ≈[ oddsC m ]W S.odds ys odds-congW [ xs≈ys ] = [ odds xs≈ys ] odds-congW (x ∷ xs≈ys) = evens-congW xs≈ys infixr 5 _⋎-congW_ -- Note: Uses swapping of arguments. _⋎-congW_ : ∀ {m m′ A} {xs xs′ ys ys′ : Stream A} → xs ≈[ m ]W ys → xs′ ≈[ m′ ]W ys′ → (xs ⟨ S._⋎_ ⟩ xs′) ≈[ m ⋎C m′ ]W (ys ⟨ S._⋎_ ⟩ ys′) [ xs≈ys ] ⋎-congW [ xs′≈ys′ ] = [ xs≈ys ⋎ xs′≈ys′ ] [ xs≈ys ] ⋎-congW (y ∷ xs′≈ys′) = [ xs≈ys ⋎ program≈ (y ∷ xs′≈ys′) ] (x ∷ xs≈ys) ⋎-congW xs′≈ys′ = x ∷ xs′≈ys′ ⋎-congW xs≈ys map-congW : ∀ {m A B} (f : A → B) {xs ys : Stream A} → xs ≈[ m ]W ys → S.map f xs ≈[ m ]W S.map f ys map-congW f [ xs≈ys ] = [ map f xs≈ys ] map-congW f (x ∷ xs≈ys) = f x ∷ map-congW f xs≈ys cast-congW : ∀ {m m′ A} (ok : m ≈C m′) {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈[ m′ ]W ys cast-congW (next m≈m′) [ xs≈ys ] = [ cast m≈m′ xs≈ys ] cast-congW (cons m≈m′) (x ∷ xs≈ys) = x ∷ cast-congW (♭ m≈m′) xs≈ys transPW : ∀ {m A} {xs ys zs : Stream A} → xs ≈[ m ]W ys → ys ≈ zs → xs ≈[ m ]W zs transPW [ xs≈ys ] ys≈zs = [ _ ≈⟨ xs≈ys ⟩P ys≈zs ] transPW (x ∷ xs≈ys) (P.refl ∷ ys≈zs) = x ∷ transPW xs≈ys (♭ ys≈zs) transW : ∀ {m A} {xs ys zs : Stream A} → xs ≈ ys → ys ≈[ m ]W zs → xs ≈[ m ]W zs transW (x ∷ xs≈ys) [ ys≈zs ] = [ _ ≈⟨ x ∷ xs≈ys ⟩ ys≈zs ] transW (P.refl ∷ xs≈ys) (x ∷ ys≈zs) = x ∷ transW (♭ xs≈ys) ys≈zs whnf≈ : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]P ys → xs ≈[ m ]W ys whnf≈ [ xs ] = [ ♭ xs ] whnf≈ (x ∷ xs) = x ∷ whnf≈ xs whnf≈ (tail xs) = tail-congW (whnf≈ xs) whnf≈ (evens xs) = evens-congW (whnf≈ xs) whnf≈ (odds xs) = odds-congW (whnf≈ xs) whnf≈ (xs ⋎ ys) = whnf≈ xs ⋎-congW whnf≈ ys whnf≈ (map f xs) = map-congW f (whnf≈ xs) whnf≈ (cast m≈m′ xs) = cast-congW m≈m′ (whnf≈ xs) whnf≈ (xs ≈⟨ xs≈ys ⟩P ys≈zs) = transPW (whnf≈ xs≈ys) ys≈zs whnf≈ (xs ≈⟨ xs≈ys ⟩ ys≈zs) = transW xs≈ys (whnf≈ ys≈zs) mutual soundW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈ ys soundW [ xs≈ys ] = soundP xs≈ys soundW (x ∷ xs≈ys) = P.refl ∷ ♯ soundW xs≈ys soundP : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]P ys → xs ≈ ys soundP xs≈ys = soundW (whnf≈ xs≈ys) ------------------------------------------------------------------------ -- The definition is correct -- The proof consists mostly of boiler-plate code. program-hom : ∀ {m A} (xs : StreamW m A) → ⟦ program xs ⟧P ≈ ⟦ xs ⟧W program-hom [ xs ] = SS.refl program-hom (x ∷ xs) = P.refl ∷ ♯ program-hom xs mutual tailW-hom : ∀ {A : Set} {m} (xs : StreamW m A) → ⟦ tailW xs ⟧W ≈ S.tail ⟦ xs ⟧W tailW-hom [ xs ] = tail-hom xs tailW-hom (x ∷ xs) = SS.refl tail-hom : ∀ {A : Set} {m} (xs : StreamP m A) → ⟦ tail xs ⟧P ≈ S.tail ⟦ xs ⟧P tail-hom xs = tailW-hom (whnf xs) mutual infixr 5 _⋎W-hom_ _⋎-hom_ -- Note: Uses swapping of arguments. _⋎W-hom_ : ∀ {A : Set} {m m′} (xs : StreamW m A) (ys : StreamW m′ A) → ⟦ xs ⋎W ys ⟧W ≈[ m ⋎C m′ ]P (⟦ xs ⟧W ⟨ S._⋎_ ⟩ ⟦ ys ⟧W) (x ∷ xs) ⋎W-hom ys = x ∷ ys ⋎W-hom xs [ xs ] ⋎W-hom [ ys ] = [ ♯ (xs ⋎-hom ys) ] [ xs ] ⋎W-hom (y ∷ ys′) = [ ♯ (⟦ xs ⋎ program ys ⟧P ≈⟨ xs ⋎-hom program ys ⟩P (begin (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ program ys ⟧P) ≈⟨ SS.refl ⟨ S._⋎-cong_ ⟩ program-hom ys ⟩′ (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ ys ⟧W) ∎)) ] where ys = y ∷ ys′ _⋎-hom_ : ∀ {A : Set} {m m′} (xs : StreamP m A) (ys : StreamP m′ A) → ⟦ xs ⋎ ys ⟧P ≈[ m ⋎C m′ ]P (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ ys ⟧P) xs ⋎-hom ys = whnf xs ⋎W-hom whnf ys mutual evensW-hom : ∀ {A : Set} {m} (xs : StreamW m A) → ⟦ evensW xs ⟧W ≈ S.evens ⟦ xs ⟧W evensW-hom [ xs ] = evens-hom xs evensW-hom (x ∷ xs) = P.refl ∷ ♯ oddsW-hom xs evens-hom : ∀ {A : Set} {m} (xs : StreamP m A) → ⟦ evens xs ⟧P ≈ S.evens ⟦ xs ⟧P evens-hom xs = evensW-hom (whnf xs) oddsW-hom : ∀ {A : Set} {m} (xs : StreamW m A) → ⟦ oddsW xs ⟧W ≈ S.odds ⟦ xs ⟧W oddsW-hom [ xs ] = odds-hom xs oddsW-hom (x ∷ xs) = evensW-hom xs odds-hom : ∀ {A : Set} {m} (xs : StreamP m A) → ⟦ odds xs ⟧P ≈ S.odds ⟦ xs ⟧P odds-hom xs = oddsW-hom (whnf xs) mutual mapW-hom : ∀ {A B : Set} {m} (f : A → B) (xs : StreamW m A) → ⟦ mapW f xs ⟧W ≈ S.map f ⟦ xs ⟧W mapW-hom f [ xs ] = map-hom f xs mapW-hom f (x ∷ xs) = P.refl ∷ ♯ mapW-hom f xs map-hom : ∀ {A B : Set} {m} (f : A → B) (xs : StreamP m A) → ⟦ map f xs ⟧P ≈ S.map f ⟦ xs ⟧P map-hom f xs = mapW-hom f (whnf xs) mutual castW-hom : ∀ {m m′ A} (m≈m′ : m ≈C m′) (xs : StreamW m A) → ⟦ castW m≈m′ xs ⟧W ≈ ⟦ xs ⟧W castW-hom (next m≈m′) [ xs ] = cast-hom m≈m′ xs castW-hom (cons m≈m′) (x ∷ xs) = P.refl ∷ ♯ castW-hom (♭ m≈m′) xs cast-hom : ∀ {m m′ A} (m≈m′ : m ≈C m′) (xs : StreamP m A) → ⟦ cast m≈m′ xs ⟧P ≈ ⟦ xs ⟧P cast-hom m≈m′ xs = castW-hom m≈m′ (whnf xs) -- The intended definition of the Thue-Morse sequence is bs = rhs bs. rhs : Stream Bool → Stream Bool rhs bs = false ∷ ♯ (S.map not (S.evens bs) ⟨ S._⋎_ ⟩ S.tail bs) -- The definition above satisfies the intended defining equation. correct : ⟦ thueMorse ⟧P ≈[ [cn]³[ccn]ω ]P rhs ⟦ thueMorse ⟧P correct = false ∷ [ ♯ cast lemma ( ⟦ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ⟧P ≈⟨ cast-hom lemma (map not (evens thueMorse) ⋎ tail thueMorse) ⟩ ⟦ map not (evens thueMorse) ⋎ tail thueMorse ⟧P ≈⟨ map not (evens thueMorse) ⋎-hom tail thueMorse ⟩P (begin (⟦ map not (evens thueMorse) ⟧P ⟨ S._⋎_ ⟩ ⟦ tail thueMorse ⟧P) ≈⟨ SS.trans (map-hom not (evens thueMorse)) (S.map-cong not (evens-hom thueMorse)) ⟨ S._⋎-cong_ ⟩ tail-hom thueMorse ⟩′ (S.map not (S.evens ⟦ thueMorse ⟧P) ⟨ S._⋎_ ⟩ S.tail ⟦ thueMorse ⟧P) ∎ )) ] -- The defining equation has at most one solution. unique : ∀ bs bs′ → bs ≈ rhs bs → bs′ ≈ rhs bs′ → bs ≈[ [cn]³[ccn]ω ]P bs′ unique bs bs′ bs≈ bs′≈ = bs ≈⟨ bs≈ ⟩ rhs bs ≈⟨ false ∷ [ ♯ cast lemma (map not (evens (unique bs bs′ bs≈ bs′≈)) ⋎ tail (unique bs bs′ bs≈ bs′≈)) ] ⟩P (begin rhs bs′ ≈⟨ SS.sym bs′≈ ⟩′ bs′ ∎)