Re: Co-recursion question

Jeffrey Harris wrote: My opinion is no.   Every function from an inductive type to an
inductive type defined using co-recursion could have been defined
without co-recursion.  Co-recursion brings in  non-functional
characteristics such as better use of memory and memoizing of
pre-computed results, but not the possibility to model more function (in
an extensional sense).

The paper Ekaterina Komendantskaya and I wrote in 2008 on the subject ,
"Using structural recursion for Corecursion",
http://hal.inria.fr/inria-00322331/en/,  shows how co-recursive
functions on streams can be replaced by structural recursive functions
from nat.  There is a particular brotherhood between nat and
stream that makes the replacement easy, but the brotherhood can be
generalized in two ways.

Here a few quick thoughts,

1/ You take any declaration of a co-inductive datatype T, you add a
singleton constructor "NYE" to represent "not yet explored" and you make
the type inductive (call it T').  Then you can define an order on
elements of this datatype, where NYE <= e for any e, and this order is a
congruence with respect to all the constructors. Then elements of T are
limits of increasing sequences in T'.  The guardedness principle
corresponds to using structural recursion while defining such an
increasing sequence, with an extra constraint that every NYE constructor
present in the term t_n must be replaced by another constructor in the
term t_{n+1}.  This forces you to define the increasing sequence in such
a way that all elements of  T' of size n are obtained in less than n
steps.  The term t_n in the sequence correspond to "what you can
construct after n co-recursive calls".

2/ For every co-inductive datatype T with constructors C1 .... Cn, if
each constructor Ci has type A1 -> ... -> Ap -> T -> ... -> T -> T, you
can define an inductive type T' with n constructors with types
C'i : A1 -> ... -> Ap -> T'.

Then every term of  T can be represented by a structurally recursive
function of type list nat -> T'.

Actually, we can replace nat by any enumerated type containing more
elements than the larger arity in T of the constructors Ci (what I call
the arity in T is the number of T arguments of the constructor).

On a more concrete example, if we consider the following co-inductive type:

CoInductive Yt1 : Type :=
  C1 : Z -> string -> Yt1 -> Yt1 -> Yt1
| C2 : bool -> Yt1 -> Yt1
| C3 : Yt1.

We define the type Yt1' in the following manner:
Inductive Yt1' : Type :=
  C1' : Z -> string -> Yt1'.
| C2' : bool -> Yt1'
| C3' : Yt1'.

The corecursive value v1 defined by:

CoFixpoint v1 : Yt1 := C1 3 "hello" C3 v1.

can be represented by the function

Fixpoint v1' (p : list nat) : Yt1' :=
match p with
  nil => C1' 3 "hello"
| 0::p' => C3'
| 1::p' => v1' p'
end.

However, the same term v1 is also represented by the following different
function:

Fixpoint v1' (p : list nat) : Yt1' :=
match p with
  nil => C1' 3 "hello"
| 0::p' => match p with nil => C3' | _ => C2' true end
| 1::p' => v1' p'
end.

In the case of Streams, the type of paths can be reduced to the type
list unit, because the maximal arity is one.
and list unit is isomorphic to nat.  Also, there is only one
constructor, with only one non-Stream component, so
that the type Stream' would be an inductive type with only one
constructor that has only one component, thus isomorphic to the type of
values carried in the stream. This is why we use functions of type nat
-> A in the paper with Ekaterina, where we show the procedure to
transform every stream value into a structurally recursive function.

The use of dependent types for the constructors adds more complications,
but still I believe that they don't add more on the co-inductive side
than on the inductive side.

Yves

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club