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

Tabulation (assuming just two elements in ℕ):

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

Colists

Definition:

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

Elements:

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

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

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

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

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 ⊤ ℕ.

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.