\subsection{Streams and Bisimilarity} \label{sec:appl:streams} \AgdaHide{ \begin{code} {-# OPTIONS --without-K #-} \end{code} } To define the substream relation, we first need to introduce streams. We have done this already in the simple type system in \exRef{basic-types} but to have a complete example, we recast the definition of streams here again in Agda. This allows us to also explain the syntax of Agda's coinductive types. Moreover, we will introduce bisimilarity on streams as a coinductively defined relation and prove that it is an equivalence relation. \begin{code} module Stream where \end{code} \AgdaHide{ \begin{code} open import Level as Level using (zero) import Relation.Binary as BinRel open import Relation.Binary as BinRel hiding (Setoid; Rel) Setoid = BinRel.Setoid Level.zero Level.zero Rel : Set → Set₁ Rel A = BinRel.Rel A Level.zero \end{code} } Before we come to the actual definitions, we import a few modules that we use throughout this section. The module \AgdaModule{Relation.Binary} contains definitions surrounding binary relations. In particular, we can write R : \AgdaFunction{Rel} \AgdaBound{A} to express that R is a type with two parameters of type A, that is, if R is of type A \AgdaSymbol{→} A \AgdaSymbol{→} \AgdaPrimitiveType{Set}. We will later show that bisimilarity of streams implies point-wise equality. Since point-wise equality is defined in terms of indexing into streams by natural numbers, we also need to import the module \AgdaModule{Data.Nat}. Finally, the module \AgdaModule{PropsAsTypes} was given in \secRef{appl:agda-preliminaries} above. \begin{code} import Relation.Binary as BinRel open import Data.Nat using (ℕ; zero; suc) open import PropsAsTypes \end{code} Let us now come to the definition of streams and their corresponding coiteration principle. The following coinductive record type corresponds to what we have called so far codata types. Thus, instead of \begin{lstlisting} codata Stream (A : Set) : Set where hd : A tl : Stream A \end{lstlisting} the type of streams is given in Agda by the following record type. \begin{code} record Stream (A : Set) : Set where coinductive field hd : A tl : Stream A \end{code} A record type in Agda is a type that is defined by its destructors, which are called fields in Agda. If a record is recursive, that is, it uses itself in its own definition, then we need to specify whether it this recursion is to be interpreted inductively or coinductively. Since we never encounter inductive record types here, we stick to the codata terminology. The reader should thus just replace the verbose coinductive record syntax in her head by the simpler codata syntax. \AgdaHide{ \begin{code} open Stream public \end{code} } The coiteration principle for streams is given in Agda by the following equational specification. \begin{code} coiter : {X A : Set} → (X → A × X) → (X → Stream A) coiter c x .hd = π₁ (c x) coiter c x .tl = coiter c (π₂ (c x)) \end{code} Note that we define the coiteration principle in terms of copattern equations, which are the same as in the calculus $\CopatCalc$. Agda ensures that this definition is well-formed by performing covering and guardedness checks.\endnote{% Agda also supports more sophisticated termination checks by using sized types. We will not discuss these further here though. } These checks intuitively work for coinductive types as follows. First, if we specify an element of a coinductive type, like for example a stream, then we are required to specify the outcome of each destructor. In the case of streams, we need to give both head and tail of a stream. Second, the guardedness condition requires that the element we are specifying does not occur in another term on the right-hand side of an equation. This ensures that the result of a destructor application does not depend on this very result itself, an instance of which we have seen in \exRef{non-productive-term}. Note that \AgdaFunction{coiter}, as given above, is thus well-defined because it appears directly and in another term on the right-hand side of the equation that specifies the tail. It is possible, though very tedious, to translate all the following equational specification into instances of iteration and coiteration schemes. But this translation largely obscures the proof idea and so we refrain from carrying it out. However, we should also make clear that this translation from such Agda specifications into the given calculus has the status of a conjecture for the time being. Some evidence that such a translation should be possible is given by~\cite{Gimenez-RecursiveSchemes} and~\cite{Goguen06:EliminatingDepPattern}. The following two functions are straightforward definitions of higher derivatives of streams, that is, repeated applications of the tail destructor, and indexing of stream positions by natural numbers. Since we have seen such definitions before, we will not explain these further here. \begin{code} δ : ∀{A} → ℕ → Stream A → Stream A δ 0 s = s δ (suc n) s = δ n (s .tl) _at_ : ∀{A} → Stream A → ℕ → A s at n = (δ n s) .hd \end{code} We now come to the definition of bisimilarity for streams. In \exRef{stream-bisimilarity}, we defined stream bisimilarity as a coinductive relation in the category theoretical setup of recursive type closed categories. The idea of that definition was that stream bisimilarity is given by two destructors: one that extracts from a proof of bisimilarity a proof that the heads of related streams are equivalent, and one that extracts a bisimilarity proof for their tails. To facilitate reuse, we define bisimilarity in terms of a so called \term{setoid}, which is a set $A$ together with an equivalence relation $\approx$ on it. Such a pair is given by the term $S$ of type \AgdaDatatype{Setoid}. To avoid further complications, we directly introduce names for the carrier $A$ of the setoid, the relation $\approx$ and for the proof that that $\approx$ is an equivalence relation. \begin{code} module Bisim (S : Setoid) where open BinRel.Setoid S renaming (Carrier to A; _≈_ to _≈_; isEquivalence to S-equiv) \end{code} \AgdaHide{ \begin{code} infix 2 _~_ \end{code} } Given such a setoid, let us now define bisimilarity for streams over $A$. We define it as a binary relations that can be written in infix notation. This is signalled by the following declaration, which says that $\sim$ is a relation with two positions (marked by the underscores). The relation itself is then defined as a coinductive type in the expected way. \begin{code} record _~_ (s t : Stream A) : Prop where coinductive field hd≈ : s .hd ≈ t .hd tl~ : s .tl ~ t .tl \end{code} \AgdaHide{ \begin{code} open _~_ public \end{code} } Since bisimilarity is a coinductive type, it comes with a coiteration principle. This principle is, as we have explained in \exRef{stream-bisimilarity}, by the usual bisimulation proof (or coinduction) principle. We briefly show how this principle can be derived from equational specifications. First, we define what it means for a relation $R$ to be a bisimulation on streams. This is witnessed by the following predicate on relations, which should be intuitively clear: A relation $R$ is a bisimulation if for all streams $s$ and $t$ that are related by $R$, their heads must be equivalent (in the setoid A) and their tails must again be related by $R$. \begin{code} isBisim : Rel (Stream A) → Prop isBisim _R_ = ∀ s t → s R t → (s .hd ≈ t .hd) ∧ (s .tl R t .tl) \end{code} Given this notion of bisimulation relation we can now derive the usual proof principle: \begin{code} ∃-bisim→~ : ∀ {_R_} → isBisim _R_ → ∀ (s t : Stream A) → s R t → s ~ t ∃-bisim→~ R-isBisim s t q .hd≈ = ∧-elim₁ (R-isBisim s t q) ∃-bisim→~ R-isBisim s t q .tl~ = ∃-bisim→~ R-isBisim (s .tl) (t .tl) (∧-elim₂ (R-isBisim s t q)) \end{code} Note the striking similarity to the coiteration principle for streams, only that in this case we construct a bisimilarity proof rather than a stream. Let us briefly go through the types that appear in the definition of \AgdaFunction{∃-bisim→~}. First, we are given a binary relation $R$ and the following arguments. \begin{align*} & \RisBisim : \AgdaFunction{isBisim} \> R \\ & s, t : \AgdaFunction{Stream} \> \AgdaField{A} \\ & q : s \mathrel{R} t \end{align*} To show that $s$ and $t$ are bisimilar, we need to provide now proofs that their heads are equivalent and that the tails are related. These are the two copattern cases of \AgdaFunction{∃-bisim→~}. By the definition of \AgdaFunction{isBisim}, we have \begin{equation*} \RisBisim \> s \> t : (s \phead \approx t \phead) \conj (s \ptail \mathrel{R} t \ptail). \end{equation*} Thus, the first conjunction elimination gives us the sought after proof for the head case. The tail case is given by recursively constructing a bisimilarity proof for the tails from the second part of the above conjunction. This should intuitively clarify how proofs of coinductive predicates are given in Agda, and it should also highlight the similarity to the definition of the coiteration principle for streams. As a sanity check for the correctness of the definition of bisimilarity, we prove that bisimilar streams are point-wise equivalent. \begin{code} bisim→ext-≈ : ∀ {s t} → s ~ t → (∀ n → s at n ≈ t at n) bisim→ext-≈ p zero = p .hd≈ bisim→ext-≈ p (suc n) = bisim→ext-≈ (p .tl~) n \end{code} We finish this section by showing that bisimilarity is an equivalence relation, where we appeal to the fact that $\approx$ is an equivalence relation. This allows us to show that streams form a setoid with bisimilarity as equivalence relation on them. These proofs should speak for themselves, thus we will not go through them in detail. \begin{code} module SE = IsEquivalence S-equiv s-bisim-refl : ∀ {s : Stream A} → s ~ s s-bisim-refl .hd≈ = SE.refl s-bisim-refl {s} .tl~ = s-bisim-refl {s .tl} s-bisim-sym : ∀ {s t : Stream A} → s ~ t → t ~ s s-bisim-sym p .hd≈ = SE.sym (p .hd≈) s-bisim-sym p .tl~ = s-bisim-sym (p .tl~) s-bisim-trans : ∀ {r s t : Stream A} → r ~ s → s ~ t → r ~ t s-bisim-trans p q .hd≈ = SE.trans (p .hd≈) (q .hd≈) s-bisim-trans p q .tl~ = s-bisim-trans (p .tl~) (q .tl~) stream-setoid : Setoid stream-setoid = record { Carrier = Stream A ; _≈_ = _~_ ; isEquivalence = record { refl = s-bisim-refl ; sym = s-bisim-sym ; trans = s-bisim-trans } } \end{code} \AgdaHide{ \begin{code} import Relation.Binary.EqReasoning as EqR module ~-Reasoning where module _ where open EqR (stream-setoid) public hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _~⟨_⟩_; begin_ to begin_; _∎ to _∎) \end{code} } This concludes the definition of streams and bisimilarity as their canonical notion of equivalence.