The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Jeffrey Harris wrote:
> Hello!
>
> I apologize for the imprecise phrasing, but does anyone know if the ability
> to do coinduction/corecursion in Coq expands the class of definable
> functions on inductive types? For instance, is there any function from
> nat->nat which is definable in Coq, but would not be definable without the
> use of coinduction/corecursion? (So, perhaps, a composition of functions
> f1:nat->stream and f2:stream->nat).
>
> Thanks,
> Jeffrey
>
>   
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