The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hi Milad,

> I know that allowing recursion on impredicative polymorphic types leads
> to terms that are structurally smaller than themselves, and this is bad
> for well-foundedness. But what is the problem in the case of coinductive
> types? 

There is a dual problem with co-inductive definitions: impredicative 
definitions of co-inductive types may introduce non-normalizable terms
(see my article "Codifying guarded definitions with recursive schemes", 
Proceedings of the 1994 Workshop on Types for Proofs and Programs, LNCS No. 
996, pages 39-59).

The main idea can be sketched as follows:

(* An impredicative co-inductive proposition *)
CoInductive T : Prop := C : (A:Prop)A->~A->T.

(* The type T is equivalent to (EX A | A & ~A), so it is empty *)
Lemma empty : ~T.
Red;Intro H;Case H;Intros;Absurd A;Auto.
Qed.

(* But there is a circular proof of T resulting from the quantification over T
    in the constructor of T. *)
CoFixpoint u : T := (C T u empty).

The problem can be avoided if the recursive ocurrences are restricted to those
that were explicitly declared in the definition of the type T. If this is the 
case, you can always codify the guarded definition using the usual 
co-recursor associated to T. This is why Coq rejects your definition.

Cheers,
Eduardo.


On Friday 18 July 2003 13:40, you wrote:
> Dear All,
>
>   I am trying to define a cofixpoint on an impredicative type.
>
> ---------------------------------------------------------------------------
> CoInductive T :Set :=  c0 : (A:Set)A->T.
>
>
> Definition Zero_T := (c0 nat O).
>
>
> CoFixpoint omega:T ->T:= [t:T]Cases t of
>                                (c0 A x) => (c0 T (omega Zero_T))
>                            end.
>
> (*
> Error: Recursive definition of G is ill-formed.
> In environment
> G :
> T ->T
> Not allowed recursive call in a non-recursive argument of constructor
> *)
>
> ---------------------------------------------------------------------------
>-
>
> Intuitively the definition of omega is productive, it just generates the
> infinite application of constructor c0.
> Moreover, the definition of omega seems to be guarded (the recursive
> occurence of omega in second branch is guarded by constructor c0 and by
> nothing else);
> and the error I get does not complain about unguardedness, rather about
> the position of the recursive call.
> I know that allowing recursion on impredicative polymorphic types leads
> to terms that are structurally smaller than themselves, and this is bad
> for well-foundedness. But what is the problem in the case of coinductive
> types? Here we don't need the computation tree to be well-founded and
> guardedness can be checked syntacticaly, So why doesn't Coq accept this
> term?
>
> Thanks in advance for any remark,