The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

> Actually, one would still need to tell on which argument to recurse, 
> as the reduction functions need this to decide when to unfold. So I 
> think a { general x } annotation would be the right way to do it. I'm 
> willing to make the change (I have a patch somewhere doing that 
> already), but maybe there are some arguments against it?
Well, most non structurally recursive functions in Coq lead to 
non-termination, for instance:

F x y :=
 if x < y then
    0
 else
    F (S x) y


F X (S Y)   has a normal form but is not strongly normalizing
F (S X) (S Y) doesn't have a normal form.

You need to do some transformation to recover termination (for instance 
my suggested :

F x y :=
 ( if x < y then  fun _ => 0 then fun G => G (S x) y ) F

)

If it is understood that this sort of function need a lot of care, we 
might as well decide arbitrarily that iota-reduction watches the first 
argument everytime (it would be quite of an interesting accident that 
choosing another argument would be of any interest whatsoever). Anyway, 
the need to check that a particular argument is constructed before 
unfolding the fixpoint is an artefact of structural recursion, therefore 
we shouldn't need any for non-structural recursion.

I personnally have no problem with an Unsafe Fixpoint feature. It's 
nothing worse than using "Axiom" anyway (plus it doesn't block 
reduction, so it's even better). As long as when I Print an Unsafe 
Fixpoint, I can see it is such (and more generally, that it's an 
accessible information to the kernel).



Arnaud Spiwack