Reversing the sense of the title: analysis of coinduction by function spaces.

Some isomorphisms

Simple cases ("linear").
  nu x. a * x         = a ^ (mu x. 1 + x)
  nu x. a * x^2       = a ^ (mu x. 1 + 2*x)
  nu x. a * x^b       = a ^ (mu x. 1 + b*x)
Lift 'em.
  (nu f. \x-> x*f x) a       = a ^ (mu x. 1 + x)
  (nu f. \x-> x*(f x)^2) a   = a ^ (mu x. 1 + 2*x)
  (nu f. \x-> x*(f x)^b) a   = a ^ (mu x. 1 + b*x)
Thorsten's trick.
  (nu f. \x-> x*f^2 x) a = a ^ (mu x. 1 + x^2)
The generalised Thorsten trick ("polynomial").
  (nu f. \x-> x * f x * f^2 x) a   = a ^ (mu x. 1 + x + x^2)
  (nu f. \x-> x * f x * ... * f^n x) a = a ^ (mu x. 1 + x + ... + x^n)
  (nu f. \x-> x^c0 * (f x)^c1 * ... * (f^n x)^cn) a = a ^ (mu x. c0 + c1*x + ... + cn*(x^n))
Using exponential notation [1] on the left
  a ^ (nu f. 1 + f + .. + f^n) = a ^ (mu x. 1 + x + ... + x^n)
(There is too much overloading of "^" to do it with coefficient types.)

Thorsten's trick in Haskell

Some (non-dependent) questions

Some (dependent) questions

Infinite terms. (Tait 1967. Consult Helmut S.)

The "infinite terms" used by various proof-theorists have a stream-like, coinductive flavour which emerges when one looks at how the recursor in Gödel's T is translated. Maybe it is possible to generalise these systems of infinitary terms, so as to handle directly more general kinds of concrete data-types?

First, here is the isomorphism between streams and functions on the natural numbers.

Str x = Case_Str x (Str x)
Nat   = Z | S Nat
lam_Str :: (N -> a) -> Str a
app_Str :: Str a -> N -> a
lam_Str f = Case_Str (f Z) (f . S)
app_Str (Case_Str x xs) n = case n of Z -> x
                                      S p -> app_Str xs p
One usually writes (xs !! n) instead of app_Str xs n.

  R' : A -> Str (A -> A) -> Str A
  R' a (b:bs) = a : R' (b a) bs   -- co

  R  : A -> (N -> A -> A) -> N -> A
  R a bf n = case n of 0   -> a    
                       S m -> bf p (R a bf p)

  R a bf n = R' a (lam_Str bf) !! n  
Cumulative product ((*) = flipped composition) and sum (lifted (*))
  cump : Str (A -> A) -> Str (A -> A)
  cump (b:bs) = id : map (b*) (cump bs)   -- * is exp. notn.
  cums : Str ((A -> A)->A->A) -> Str ((A -> A)->A->A)
  cums (b:bs) = zero : map (b+) (cums bs)   -- * is exp. notn.
                where zero flip const
  R a (bs!!) n = (cump bs !! n) a

What should one be doing about coinduction in type theory?

The first thing is to formulate schemes of coinduction within dependent type theory. There must be quite a history of this. Didn't Mendler do it in dependent types? Some people who have written about coinduction. (Mostly for simple types, or set theory.)

Then, one can try to figure out the metatheory of such systems, using whatever principles on the meta-level. (The usual dreary things: church-rosser, subject reduction, ...)

One can also try to find models of such systems, which can be constructed within (well-founded) type theory. (Comparable to Aczel's graph-theoretic models of non-well-founded set-theory. Anton and I came to feel while writing our paper that we should really be developing a (type-)theory of graphs. Perhaps this is not a routine reworking of the classical theory.)

For me, the interest of all this is connected with interactive programming in type theory.

One needs access to a wide variety of coinductively defined types, justified (modelled, analysed, encoded) in well-founded (and predicative) type theory.

Is the direction of this "justification" reversible? (Suggested by the corecursive simulation of natrec, in the infinitary terms stuff. )


[1] Exponential notation

     a ^ b       = b a
     a ^ (b * c) = (a ^ b) ^ c
     a ^ (b + c) = a ^ b * a ^ c
     a ^ 0       = id

The following may not be relevant, but for the moment I think there is a chance. It was pointed out to me by Conor McBride.

  1. Consider binary wellfounded trees:
         B = 1 + B^2
    If we remove a single (not necessarily immediate) subtree from a binary tree, we are left with a structure on type P, where
         P = 1 + 2*B*P
  2. In general, if we consider n-ary wellfounded trees:
         T = 1 + T^n
    and we remove a single (not necessarily immediate) subtree from such a tree, we are left with a structure on type Q, where
         Q = 1 + n*T^(n-1)*Q
Note that there is a kind of formal differentiation in the "business" part of the type expression. (Conor's observation extended to cover familiar rules of differentiation such as D(S*T) = S*D(T) + D(S)*T, but for the moment, I cannot recall exactly how.)

Peter Hancock
Last modified: Fri Apr 7 10:14:21 BST 2000