Monthly Archives: February 2015

Mixed induction/coinduction in Agda (13/2/2015)

I gave an introduction to conduction in Agda using the \infty operator. Basically the idea is that values \infty\, A is the type of computations of A. Using this we can define the type of streams where the tail is a delayed computation:

data _ω (A : Set) : Set where
  _∷_ : A → ∞ (A ω) → A ω 

To create stream programs we use the two operations: delay \sharp : A \to \infty A which creates delayed computations and force \flat : \infty A \to A which evaluates a previously delayed computation. Clearly we have \flat (\sharp a) = a. We can use \sharp to produce the stream of numbers starting from a given number:

from : ℕ → ℕ ω
from n = n ∷ ♯ (from (suc n))

Another example where we need to use both \sharp and \flat is map for streams:

map : {A B : Set} → (A → B) → A ω → B ω
map f (a ∷ as) = (f a) ∷ ♯ (map f (♭ as))

Here we use \sharp to delay the recursive stream computation and within this we use \flat to force the computation of the input stream. We frequently see this sort of force / delay combination.
Using this simple extension we can write simple coinductive programs and a trivial extension of Agda’s termination checker handles this situation: Apart from guard on the left using pattern matching we can also have guard on the right using \#. We can also define predicates coinductively: A standard example is bisimilarity of streams

data _≈_ {A : Set} : A ω → A ω → Set where
  _∷_ : {a a' : A} → a ≡ a'
      → {as as' : ∞ (A ω)} → ∞ ((♭ as) ≈ (♭ as'))
      → (a ∷ as) ≈ (a' ∷ as')

Note that we use \infty for the infinite recursive proof that the tails are equal. It is easy to show reflexivity:

refl≈ : {A : Set} → (as : A ω) → as ≈ as
refl≈ (a ∷ as) = refl ∷ ♯ (refl≈ (♭ as))

A more interesting example is the following simple fact about from and map:

lem : (n : ℕ) → map suc (from n) ≈ from (suc n)
lem n = refl ∷ ♯ (lem (suc n))

It isn’t always so easy because we may have to generalize our theorem so that the recursion goes through. However, this approach compares favourably with the usual definition of bisimilarity as the greatest bisimulation which is defined as a relation which is stable under the destructors, here head and tail. Thinking extensionally, bisimilarity is the equality for streams, or more precisely \mathrm{refl}\approx is an equivalence in the sense of HoTT.

The nice thing about using \inftyis that it is easy to define types which use both induction and conduction. A standard example are stream processors, a representation of functions on streams:

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

we can only read a finite amount of data before outputing however the latter can happen infinitely often. This is reflected by using \infty in the type of the 2nd constructor but not in the first. We can interpret a stream processor as a function on streams:

⟦_⟧ : {A B : Set} → SP A B → A ω → B ω
⟦ get f ⟧ (a ∷ as)  = ⟦ f a ⟧ (♭ as)
⟦ put b sp ⟧ as     = b ∷ ♯ ( ⟦ ♭ sp ⟧ as)

This function uses a mixture of structural recursion and guarded corecursion: the first line is structurally recursive and the 2nd is guarded. While they can also be understood as a nested conductive/inductive type SP\,A\,B = \nu X.\mu Y.A\to Y + B \times X, the Agda approach seems more intuitive. An example are the composition operators, input driven:

_>>>l_ : {A B C : Set} → SP A B → SP B C → SP A C
(put b sp) >>>l (get f)      = (♭ sp) >>>l f b
(get f) >>>l (get g)         = get (λ a → (f a) >>>l (get g))
(put b sp) >>>l (put c sp')  = put c (♯ ((put b sp) >>>l ♭ sp'))
(get f) >>>l (put c sp)      = get (λ a → (f a) >>>l (put c sp))

or output driven:

_>>>r_ : {A B C : Set} → SP A B → SP B C → SP A C
(put b sp) >>>r (get f)      = (♭ sp) >>>r f b
(get f) >>>r (get g)         = get (λ a → (f a) >>>r (get g))
(put b sp) >>>r (put c sp')  = put c (♯ ((put b sp) >>>r ♭ sp'))
(get f) >>>r (put c sp)      = put c (♯ (get f >>>r ♭ sp))

The only difference is in the last line when both output and input is possible. I leave it as an exercise to derive both operators using only categorical combinators (fold, unfold).

Using this very naive approach it is easy to represent types of the form \nu\mu it turns out to be impossible to implement types of the form \mu\nu. I think this problem could be solved by mixing size change termination with parity games. See our short paper for a more detailed description of the problem.