```
module Revise.Coinduction where```

# Import List

```
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Vec using (Vec; _∷_; [])
open import Relation.Binary.PropositionalEquality using (_≡_; refl)```

# Goal

We would like to reperesent infinite data like streams.
Let's try:

```
Stream₀ : Set → Set
Stream₀ A = ℕ → A```

OK, but

• Equality of streams should be stated elementwise.
• This representation may be inefficient.
• Lazy operations on streams are needed.

# Coinductive data

``````data Stream (A : Set) : Set where
_∷_ : A → ∞ (Stream A) → Stream A``````

Coinductive data structures has the following properties:

• Coinductive data may be "infinite".
• Lazy evaluation of functions can be expressed with coinductive arguments/results.
• Coinductive data have no normal form; Values are equal if they have the same behaviour (pattern matching gives the same result).

# Main functions

Three main functions to support coinduction:

``````∞  : (A : Set) → Set       -- laziness set constructor
♯_ : {A : Set} → A → ∞ A   -- compiled as delay
♭  : {A : Set} → ∞ A → A   -- compiled as force``````

These can be found in `Data.Coinduction`:

```
open import Coinduction using (∞; ♯_; ♭)```

• `♯_` is an operator, not a function, so `♯ f x` parses as `♯ (f x)`.
• Termination checking is special as we will see.

# Imaginary definition

One could imagine the main functions defined as follows:

``````infix 1000 ♯_

data ∞ (A : Set) : Set where
♯_ : A → ∞ A

♭ : {A : Set} → ∞ A → A
♭ (♯ x) = x``````

Differences

• No difference in parsing and type checking.
• Different termination checking rules.
• Pattern matching on the original `♯_` is not possible (we use `♭` instead).
• `∞ A` has delayed (not yet computed) values, see later.

# Example

Definition of `ℕω`:

```
data ℕω : Set where
zero :        ℕω
suc  : ∞ ℕω → ℕω```

Some elements:

``````zero : ℕω
suc (♯ zero) : ℕω
suc (♯ suc (♯ zero)) : ℕω``````

If we assume a not yet computed value `v : ∞ ℕω`, we have also

``````suc v : ℕω
suc (♯ suc v) : ℕω
suc (♯ suc (♯ suc v)) : ℕω
...``````

# Information ordering

`Having more information` relation (on open terms):

• `suc v``suc (♯ zero)`.
• `suc v``suc (♯ suc v)`.
• `suc (♯ suc v)``suc (♯ suc (♯ suc v))`.
• ...

Finite or infinite sequences of open terms with increasing information:

`a₁``a₂``a₃` ≺ ..., `aᵢ : A`

# Information merging

If

`v : V``a₁ : A`,
`a₁``a₂``a₃` ≺ ...
and every occurence of `v` is "refined",

then

Lim_`v`(`a₁``a₂``a₃` ≺ ...) `: A`.

Example:

Lim_`v`(`suc v``suc (♯ suc v)``suc (♯ suc (♯ suc v))` ≺ ...) `: ℕω`

Abbreviation:

`suc (♯ suc (♯ suc`...`))`
= Lim_`v`(`suc v``suc (♯ suc v)``suc (♯ suc (♯ suc v))` ≺ ...)

So

`ℕω``ℕ ⊎ ⊤`.

# Exercises

What are the elements of the following set?

```
data ℕ⁻ : Set where
suc  : ℕ⁻ → ℕ⁻```

What are the elements of the following set?

```
data Ω : Set where
suc  : ∞ Ω → Ω```

# Corecursive calls

Consider the following definition:

```
ω : ℕω
ω = suc (♯ ω)```

"Values of coinductive types can be constructed using corecursion, which does not need to terminate, but has to be productive. As an approximation to productivity the termination checker requires that corecursive definitions are guarded by coinductive constructors."

So defintion of `ω` is valid!

# Streams

Streams are important corecursive sets.

```
data Stream (A : Set) : Set where
_∷_ : A → ∞ (Stream A) → Stream A

infixr 5 _∷_```

Tabulation (assuming just two elements in `ℕ`):

Set 1st, 2nd, 3rd, ...
Stream ℕ ={ `0 ∷ v` `0 ∷ ♯ 0 ∷ v` `0 ∷ ♯ 0 ∷ ♯ 0 ∷ v` ...
`0 ∷ ♯ 0 ∷ ♯ 1 ∷ v` ...
...
`0 ∷ ♯ 1 ∷ v` `0 ∷ ♯ 1 ∷ ♯ 0 ∷ v` ...
`0 ∷ ♯ 1 ∷ ♯ 1 ∷ v` ...
...
`1 ∷ v` `1 ∷ ♯ 0 ∷ v` `1 ∷ ♯ 0 ∷ ♯ 0 ∷ v` ...
`1 ∷ ♯ 0 ∷ ♯ 1 ∷ v` ...
...
`1 ∷ ♯ 1 ∷ v` `1 ∷ ♯ 1 ∷ ♯ 0 ∷ v` ...
`1 ∷ ♯ 1 ∷ ♯ 1 ∷ v` ...
...

`Stream A``ℕ → A`.

Note that `0 ∷ ♯ 0 ∷ ♯ 1 ∷ v` parses as `0 ∷ ♯(0 ∷ ♯(1 ∷ v))`.

# Recursive functions on streams

```
head : {A : Set} → Stream A → A
head (x ∷ xs) = x

tail : {A : Set} → Stream A → Stream A
tail (x ∷ xs) = ♭ xs

lookup : {A : Set} → ℕ → Stream A → A
lookup zero    (x ∷ xs) = x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

take : {A : Set} (n : ℕ) → Stream A → Vec A n
take zero    xs       = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

drop : {A : Set} → ℕ → Stream A → Stream A
drop zero    xs       = xs
drop (suc n) (x ∷ xs) = drop n (♭ xs)```

# Corecursive functions on streams

```
repeat : {A : Set} → A → Stream A
repeat x = x ∷ ♯ repeat x

iterate : {A : Set} → (A → A) → A → Stream A
iterate f x = x ∷ ♯ iterate f (f x)

map : {A B : Set} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

zipWith : {A B C : Set} → (A → B → C) → Stream A → Stream B → Stream C
zipWith _∙_ (x ∷ xs) (y ∷ ys) = (x ∙ y) ∷ ♯ zipWith _∙_ (♭ xs) (♭ ys)

-- interleaving
_⋎_ : {A : Set} → Stream A → Stream A → Stream A
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)

infixr 5 _⋎_  ```

# Colists

Definition:

```
data Colist (A : Set) : Set where
[]  :                    Colist A
_∷_ : A → ∞ (Colist A) → Colist A```

Elements:

Set 1st, 2nd, 3rd, ...
Colist ℕ ={ `[]`;
`0 ∷ v` `0 ∷ []`;
`0 ∷ ♯ 0 ∷ v` `0 ∷ ♯ 0 ∷ []`;
`0 ∷ ♯ 0 ∷ ♯ 0 ∷ v` ...
`0 ∷ ♯ 0 ∷ ♯ 1 ∷ v` ...
...
`0 ∷ ♯ 1 ∷ v` `0 ∷ ♯ 1 ∷ []`;
`0 ∷ ♯ 1 ∷ ♯ 0 ∷ v` ...
`0 ∷ ♯ 1 ∷ ♯ 1 ∷ v` ...
...
...

`Colist A``List A ⊎ Stream A`.

# Functions on colists

```
toColist : {A : Set} → Stream A → Colist A
toColist (x ∷ xs) = x ∷ ♯ toColist (♭ xs)

_++_ : {A : Set} → Colist A → Stream A → Stream A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

infixr 5 _++_```

# Equality on streams

The set for stream equality is corecursive itself:

```
data _≈_ {A : Set} : Stream A → Stream A → Set where
_∷_ : (x : A) {xs ys : ∞ (Stream A)} →
∞ (♭ xs ≈ ♭ ys) → x ∷ xs ≈ x ∷ ys

infix 4 _≈_```

Examples:

Let `s : Stream ℕ` be fixed.

`0 ∷ s ≈ 1 ∷ s` = {}.

Let `v : ∞ (0 ∷ s ≈ 1 ∷ s)`.

`1 ∷ ♯ 0 ∷ s ≈ 1 ∷ ♯ 1 ∷ s` = { `1 ∷ v` }, after erasing `v` it is {}.

Let `x = repeat 0` and `v : ∞ (x ≈ x)`.

`x ≈ x` = { `0 ∷ v``0 ∷ ♯ 0 ∷ v``0 ∷ ♯ 0 ∷ ♯ 0 ∷ v` ≺ ... }

`x ≈ x``⊤`.

# Proofs with stream equality

```
≈-refl : {A : Set} {xs : Stream A} → xs ≈ xs
≈-refl {A} {x ∷ _} = x ∷ ♯ ≈-refl

≈-sym : {A : Set} {xs ys : Stream A} → xs ≈ ys → ys ≈ xs
≈-sym (x ∷ xs≈) = x ∷ ♯ ≈-sym (♭ xs≈)

≈-trans : {A : Set} {xs ys zs : Stream A} → xs ≈ ys → ys ≈ zs → xs ≈ zs
≈-trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ ≈-trans (♭ xs≈) (♭ ys≈)

map-cong : {A B : Set} (f : A → B) {xs ys : Stream A} →
xs ≈ ys → map f xs ≈ map f ys
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)

elem-≡ : {A : Set} {xs ys : Stream A} →
xs ≈ ys → (n : ℕ) → lookup n xs ≡ lookup n ys
elem-≡ (x ∷ xs)  zero   = refl
elem-≡ (x ∷ xs) (suc n) = elem-≡ (♭ xs) n```

It this possible?

``````func-≡ : {A : Set} (f : Stream A → ℕ) (xs ys : Stream A) →
xs ≈ ys → f xs ≡ f ys
func-≡ f xs ys e = {!!}``````

# Other relations on streams

Element relation:

```
data _∈_ {A : Set} : A → Stream A → Set where
here  : {x : A}   {xs : ∞ (Stream A)}              → x ∈ x ∷ xs
there : {x y : A} {xs : ∞ (Stream A)} → (x ∈ ♭ xs) → x ∈ y ∷ xs

infix 4 _∈_```

Prefix-of relation:

```
data _⊑_ {A : Set} : Colist A → Stream A → Set where
[]  : {ys : Stream A}                → [] ⊑ ys
_∷_ : {x : A} {xs : ∞ (Colist A)} {ys : ∞ (Stream A)} →
∞ (♭ xs ⊑ ♭ ys) → x ∷ xs ⊑ x ∷ ys

infix 4 _⊑_```

# Inductive and coinductive sets

Set of stream processors:

```
data SP (A B : Set) : Set where
get : (A → SP A B)   → SP A B
put : B → ∞ (SP A B) → SP A B```

Meaning: we can produce infinite many elements (`put`), but can consume only finite elements (`get`) before production.

Examples:

Let `v : SP ⊤ ℕ`.

Set 1st, 2nd, 3rd, ...
SP ⊤ ℕ = { `put 3 v` `put 3 (♯ put 4 v)` `put 3 (♯ put 4 (♯ put 9 v)` ...
`put 4 v` ...
`get (λ tt → put 3 v)` `get (λ tt → put 3 (♯ put 4 v))` ...
`get (λ tt → put 4 v)` ...
`get (λ tt → get (λ tt → put 3 v)` ...
...

# Inductive and coinductive sets (2)

Application of a stream processor:

```
eat : {A B : Set} → SP A B → Stream A → Stream B
eat (get f)    (a ∷ as) = eat (f a) (♭ as)
eat (put b sp) as       = b ∷ ♯ eat (♭ sp) as```

Composition of stream processors:

```
_∘_ : {A B C : Set} → SP B C → SP A B → SP A C
get f₁    ∘ put x sp₂ = f₁ x ∘ ♭ sp₂
put x sp₁ ∘ sp₂       = put x (♯ (♭ sp₁ ∘ sp₂))
sp₁       ∘ get f₂    = get (λ x → sp₁ ∘ f₂ x)```

Exercise: Find the recursive and corecursive calls!

# Sets defined with coinduction

Definition of `Rec`:

```
data Rec (A : ∞ Set) : Set where
fold : ♭ A → Rec A```

`Rec (♯ B)``B`, but `Rec` is useful to cheat termination checking:

``````ℕ′ : Set
ℕ′ = ⊤ ⊎ Rec (♯ ℕ′)``````

`ℕ′``ℕ`.

This is still experimental in Agda. It can be enabled with `--guardedness-preserving-type-constructors`.

# What Else?

You can find lots of examples on Nils Anders Danielssons home page.