- Import List
- Goal
- Coinductive data
- Main functions
- Imaginary definition
- Example
- Information ordering
- Information merging
- Exercises
- Corecursive calls
- Streams
- Recursive functions on streams
- Corecursive functions on streams
- Colists
- Functions on colists
- Equality on streams
- Proofs with stream equality
- Other relations on streams
- Inductive and coinductive sets
- Inductive and coinductive sets (2)
- Sets defined with coinduction
- What Else?

module Revise.Coinduction where

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)

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.

```
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).

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.

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.

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)) : ℕω
...
```

`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`

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

`ℕω`

≃ `ℕ ⊎ ⊤`

.

What are the elements of the following set?

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

What are the elements of the following set?

data Ω : Set where suc : ∞ Ω → Ω

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 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))`

.

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)

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 _⋎_

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`

.

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 _++_

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`

≃ `⊤`

.

≈-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 = {!!}
```

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 _⊑_

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)` ≺ |
... | |||

... |

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!

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`

.

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