The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT lri.fr>]

On Tue, 9 May 2000, Eduardo Gimenez wrote:

> > Fixpoint Sum [ n: nat] : nat :=
> >  Cases n of
> >  O => (KMCM O)
> > |(S m)=>(plus  (KMCM n) (Sum m))
> > end 
> > with
> >         KMCM [n:nat] : nat :=
> > Cases n of
> >      O => (S O)
> > |(S m) => (Sum m )
> > end.

[...]

> These modifications are necessary for the syntactical condition ensuring 
> termination to hold.

If you unfold a little bit your definition, you obtain a good (non mutual)
definition:

Fixpoint Sum [ n: nat] : nat :=
 Cases n of
 O => (S O)
 |(S m)=>(plus  (Sum m) (Sum m))
end
with
        KMCM [n:nat] : nat :=
Cases n of
     O => (S O)
|(S m) => (Sum m )
end.

> This is yet another example of how nasty is to control termination via a
> syntactical condition on untyped terms. Actually, it would be better
> to do it via a some kind of abstract interpretation technique, or via
> a more refined type system (that is actually the same thing). For a further
> discusion on this subject see my article in ICALP'98 or Bruno Barras'  PhD
> thesis.

Certainly, to introduce more semantics in termination criteria allows
to accept more definitions. However, syntactical criteria more powerful
than the one currently used in the Coq system have been developped:

The General Schema in Inductive Data Type Systems (to appear in TCS)
http://www.lri.fr/~blanqui/publis/idts.ps.gz

The Higher-Order Recursive Path Ordering of Jouannaud and Rubio (LICS'99)
ftp://ftp.lri.fr/LRI/articles/jouannaud/horpo-full.ps.gz

Frederic Blanqui.

------------------------------------------------------------------------------
Laboratoire de Recherche en Informatique (LRI) - Equipe DEMONS
batiment 490, bureau 153, Universite Paris-Sud 91405 ORSAY (FRANCE)
tel:33.1.69.15.42.35 - fax:33.1.69.15.65.86 - web:http://www.lri.fr/~blanqui