The Coq mailing list

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

Dear Samuel,

I did not see a question in your message, but yes, your program violates 
the guardedness
condition.

The guardedness condition for corecursive definitions is much more 
restrictive than
the "well-definedness" conditions for Haskell and other lazy programming 
languages.

Simply put, a co-recursive definitions is guarded if all recursive 
references to the
function you are defining appear in branches of pattern-matching 
constructs and
as sub-terms of constructors of the same co-recursive type (or 
constructors of
a co-recursive type that was defined co-inductively in a mutual 
definition with
their type), with at least one constructor involved.

Your definition violates this condition, because co-recursive calls 
appear under
a call to dPlus, and dPlus is neither a pattern-matching construct  nor 
a constructor
of the co-inductive type.

I am aware of work to circumvent the limitations of guardedness to get 
closer to
"general corecursion".  The experiments done in my team only make it 
possible
to cope with the cases where functions are not accepted because the "at 
least one
constructor" clause in not satisfied.  But your code does not fall in 
this category.  It
has been nagging us for a long time, but we haven't found a way in yet.

I believe work by Miculan and di Giantonio (FOSSACS'04 ?) and recent work
published by Christine Paulin on her Web page

http://www.lri.fr/~paulin/PUBLIS/paulin07kahn.pdf

are related to this topic.

I hope this helps,

Yves



Samuel Bronson wrote:
> I'm trying to implement
> http://conal.net/blog/posts/beautiful-differentiation/ but having
> trouble with the guardedness condition -- at least, that's what I
> think it must be. My latest attempt is:
>
> Section Foo.
>   Variable N : Type.
>   Variable zero : N.
>   Variable plus : N -> N -> N.
>   Variable times : N -> N -> N.
>   Variable opp : N -> N.
>
>   Infix    "+"   := plus    : N_scope.
>   Infix    "*"   := times   : N_scope.
>   Notation "- x" := (opp x) : N_scope.
>
>   Bind Scope N_scope with N.
>
>   (* <roconnor> SamB: how about
>    *   x@(D x0 x') * y@(D y0 y') = D (x0 * y0) (x' * y) + D 0 (x * y')
>    *)
>
>   CoInductive Dif :=
>    D : N -> Dif -> Dif.
>
>   Delimit Scope Dif_scope with Dif.
>   Bind Scope Dif_scope with Dif.
>
>   CoFixpoint dZero := D zero (dZero).
>
>   CoFixpoint dOpp (x : Dif) : Dif :=
>     match x with
>       D x0 x' => D (-x0) (-x')%Dif
>     end
>   where "- x" := (dOpp x).
>
>   CoFixpoint dPlus (x y : Dif) : Dif :=
>     match x, y with
>       D x0 x', D y0 y' => D (x0 + y0) (x' + y')%Dif
>     end
>   where "x + y" := (dPlus x y).
>
>   CoFixpoint dTimes (x y : Dif) : Dif :=
>     match x, y with
>       D x0 x', D y0 y'
>         => D (x0 * y0) (x' * y + x * y')
>     end%Dif
>   where "x * y" := (dTimes x y).
> End Section.
>
> but the definition of dTime fails, with the error message:
>
> Error:
> Recursive definition of dTimes is ill-formed.
> In environment
> N : Type
> zero : N
> plus : N -> N -> N
> times : N -> N -> N
> opp : N -> N
> dTimes : Dif -> Dif -> Dif
> x : Dif
> y : Dif
> x0 : N
> x' : Dif
> y0 : N
> y' : Dif
> Unguarded recursive call in
> "cofix dPlus (x y : Dif) : Dif :=
>    match x with
>    | D x0 x' => match y with
>                 | D y0 y' => D (x0 + y0) (x' + y')
>                 end
>    end".
> Recursive definition is:
> "fun x y : Dif =>
>  match x with
>  | D x0 x' =>
>      match y with
>      | D y0 y' => D (x0 * y0) (dTimes x' y + dTimes x y')
>      end
>  end".
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.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
>