{- Mixing induction and coinduction in Agda Thorsten Altenkirch (based on joint work with Nils Anders Danielsson) School of Computer Science University of Nottingham -} module Tallinn10 where open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import Data.Nat hiding (_+_) {- 0. Introducing Agda -} {- To see the inductive definition of Nat, just click on it. -} {- We can define programs by structural recursion: -} _+_ : ℕ → ℕ → ℕ zero + n = n suc n + n' = suc (n + n') {- If we replace the last line by suc n + n' = suc ((suc n) + n') the termination checker will complain. -} {- We can do proofs by structural recursion. -} +0 : (n : ℕ) → n + zero ≡ n +0 zero = refl +0 (suc n) = cong suc (+0 n) +suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n) +suc zero n = refl +suc (suc m) n = cong suc (+suc m n) +-comm : (m n : ℕ) → m + n ≡ n + m +-comm m zero = +0 m +-comm m (suc n) = trans (+suc m n) (cong suc (+-comm m n)) {- +-comm always retruns refl, hence running it is useless. A more interesting example is the proof of decidability of equality for natural numbers. -} _≡?_ : (m n : ℕ) → Dec (m ≡ n) zero ≡? zero = yes refl zero ≡? suc n = no (λ ()) suc n ≡? zero = no (λ ()) suc n ≡? suc m with n ≡? m suc n ≡? suc m | yes p = yes (cong suc p) suc n ≡? suc m | no ¬p = no (λ sn≡sm → ¬p (cong pred sn≡sm)) {- ≤ is defined inductively (click on the symbol) we can prove properties by structural recursion over this definition. -} ≤-trans : ∀ {l m n} → l ≤ m → m ≤ n → l ≤ n ≤-trans z≤n m≤n = z≤n ≤-trans (s≤s m≤n) (s≤s n≤n') = s≤s (≤-trans m≤n n≤n') {- 1. Coinductive definitions, eg. Streams -} open import Coinduction infixr 5 _∷_ {- We define "coinductive types" like streams by using ∞, where ∞ A stands for the type of delayed computations of type A. -} data Stream (A : Set) : Set where _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A {- ∞ comes with two basic operations: -- ♯ : A → ∞ A (delay) -- ♭ : ∞ A → A (force) -} {- e.g. using ♯ we can define a function computing the stream of natural numbers starting with n. Note that this recursion is permitted because the recursive call is guarded by ♯. The termination checker views functions with coinductive results as functions with an additionional (virtual) argument which gets decreased each time ♯ is used. -} from : ℕ → Stream ℕ from n = n ∷ (♯ from (suc n)) {- defining head and tail, not that we use ♭ in tail. -} head : ∀ {A} → Stream A → A head (a ∷ as) = a tail : forall {A} → Stream A → Stream A tail (x ∷ xs) = ♭ xs {- bad is not guarded. The termination checker will refuse to accept this program because the recursive call is inside the call to tail and tail does not preserve guardedness. -} {- bad : ℕ → Stream ℕ bad n = n ∷ ♯ tail (bad (suc n)) -} infixr 4 _~_ {- We define equality of streams which is called "bisimilarity" The idea is two streams are equal if there is a stream of equality proofs showing that any two corresponding elements are equal. Indeed, we have to use ∞ in the definition of ~. -} data _~_ {A} : (xs ys : Stream A) → Set where _∷_ : ∀ {x y} {xs ys} → x ≡ y → ∞ (♭ xs ~ ♭ ys) → x ∷ xs ~ y ∷ ys {- As an example of a proof involving ~ we show that from (suc n) is the same as map suc (from n) where map is defined below. -} map : ∀ {A B} → (A → B) → Stream A → Stream B map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs) fromLem : (n : ℕ) → from (suc n) ~ map suc (from n) fromLem n = refl ∷ (♯ fromLem (suc n)) {- We compare ~ with the traditional definition using bisimulations: -} record Bisim {A : Set}(_R_ : Stream A → Stream A → Set) : Set where field hd : ∀ {as bs} → as R bs → head as ≡ head bs tl : ∀ {as bs} → as R bs → tail as R tail bs {- If we switch off uinverse checking, i.e. put {-# OPTIONS --type-in-type #-} on the top of the file we can define ~' as the largest bisimulation: data _~'_ {A} : (xs ys : Stream A) → Set where bisim : ∀ {x y : Stream A}(_R_ : Stream A → Stream A → Set) → Bisim _R_ → x R y → x ~' y I would argue that the 1st definition of ~ is simpler, easier to use and doesn't require impredicativity. -} {- The next function is an example of a function which is actually total but the termination checker fails to recognize this. -} {- bad' : ℕ → Stream ℕ bad' n = n ∷ ♯ map suc (bad' n) -} {- 2. Mixed definitions, e.g. SP -} {- We define the type of stream processors SP A B representing functions from Stream A to Stream B. SP is used inductively for the first constructor and coinductively -} data SP (A B : Set) : Set where get : (A → SP A B) → SP A B put : B → ∞ (SP A B) → SP A B {- On the top level mixed definitions correspond to nested ν μ in the categorical sense. E.g. SP A B = ν X.μ Y. (A → Y) + (B × X) more general: data A = F (A , ∞ A) means A = ν X.μ Y.F(Y,X) -} {- As an example: the function pure produces a stream processor that applies a function f pointweise to a strams. -} pure : ∀ {A B} → (A → B) → SP A B pure f = get (λ a → put (f a) (♯ (pure f))) {- A more interesting example is the semantics of a stream processor as a function. -} ⟦_⟧ : ∀ {A B} → SP A B → Stream A → Stream B -- ℕ → B ⟦ get f ⟧ (a ∷ as) = ⟦ f a ⟧ (♭ as) ⟦ put b sp ⟧ as = b ∷ ♯ ⟦ ♭ sp ⟧ as {- The definition uses a lexical product of the inductive order on get and the coinductive order implied by the fact that the result type is stream. This can be visualized by viewing streams as functions over the natural numbers. -} {- Two other examples are the two possible definitions of composition of stream processor. The reader is invited to derive both from categorical combinators fold, unfold to realize how much effort is saved by using Agda. -} -- match left: data driven _>>>_ : ∀ {A B C} → SP A B → SP B C → SP A C get f >>> tq = get (λ a → f a >>> tq) put a sp >>> get f = ♭ sp >>> f a put a sp >>> put b tq = put b (♯ put a sp >>> ♭ tq) -- match right: demand driven _>>>'_ : ∀ {A B C} → SP A B → SP B C → SP A C get g >>>' get f = get (λ a → g a >>>' get f) put b sp >>>' get f = ♭ sp >>>' f b sp >>>' put c tq = put c (♯ (sp >>>' ♭ tq)) {- An example for a mixed definition of a relation is the definition of weak bisimilarity for the partiality monad. -} {- A ν represents (possibly non-terminating) computations over A. -} data _ν (A : Set) : Set where now : A → A ν later : ∞ (A ν) → A ν ⊥ : ∀ {A} → A ν ⊥ = later (♯ ⊥) infix 4 _≈_ {- We identify two computations which only differ by a finite amount of laters. This leads naturally to a mixed coinductive/inductive definition since the cogruence for later has to be coinductive while the rules introducing finite delay have to be inductive. -} data _≈_ {A : Set} : A ν → A ν → Set where now : ∀ {v} → now v ≈ now v later : ∀ {x y} → ∞ ( ♭ x ≈ ♭ y) → later x ≈ later y laterʳ : ∀ {x y} → x ≈ ♭ y → x ≈ later y laterˡ : ∀ {x y} → ♭ x ≈ y → later x ≈ y {- 3. The nesting problem -} {- Finally, we discuss an issue which arises when nesting coinductive definitions inside inductive ones. -} {- Consider the type below which allows only a finite number of [0] in between any two [1]s. However, there can be infinitely many [0]s alltogether, e.g. the infinite sequnce 0,1,0,1... -} data O∞ : Set where [0] : O∞ → O∞ [1] : ∞ O∞ → O∞ [01]∞ : O∞ [01]∞ = [0] ([1] (♯ [01]∞)) {- we read this as ν X.μ Y.[0]:Y + [1]:X -} {- What happens, if we switch the quantfiers? O = μ Y.ν X.[0]:Y + [1]:X corresponds to sequences which may only contain a finite number of 0s, ever sequence will end with an infinite sequence of 1s. In particular, we should not be able to define 0,1,0,1,... However, when we try to encode this in Agda something strange happens. -} {- We use a parametrized definition for the inside O = μ Y. Z O where Z O = ν X.[0]:O + [1]:X -} data Z (O : Set) : Set where [0] : O → Z O [1] : ∞ (Z O) → Z O data O : Set where ↓ : Z O → O {- However, we are still able to define the infinite sequence 0,1,0,1,.. -} 01^ω : O 01^ω = ↓ ([1] (♯ [0] 01^ω)) {- The termination checker considers this definition as guarded, because indeed the recursive call is guarded by ♯. However, the ♯ was intended to be used for recursive definitions only involving Z O not O as well. -} {- On the other hand the termination checker doesn't allow us to derive the fold for O. Here is an attempt: -} {- mutual Ofold : ∀ {A} → (Z A → A) → O → A Ofold f (↓ x) = f (ZmapOfold f x) -- Ofold f (↓ x) = f (Zmap (Ofold f) x) ZmapOfold : ∀ {A} → (Z A → A) → Z O → Z A ZmapOfold f ([0] x) = [0] (Ofold f x) ZmapOfold f ([1] x) = [1] (♯ ZmapOfold f (♭ x)) -} -- if we could define Ofold, we would have a diverging computation. -- however, the termination checker doesn't accept this definition -- because there are recursive paths Ofold --> Ofold which pass -- through #. -- we would prefer the dual: 01^ω should be rejected but Ofold -- should be accepted. {- 4. References: All jointly with Nils Anders Danielsson. Mixing Induction and Coinduction http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html Subtyping, Declaratively - An Exercise in Mixed Induction and Coinduction http://www.cs.nott.ac.uk/~txa/publ/danielsson-altenkirch-subtyping.pdf (to appear in MPC 2010) Termination Checking Nested Inductive and Coinductive Types http://www.cs.nott.ac.uk/~txa/publ/InvertedQuantifiers.pdf (to be presented at PAR 2010) -}