The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 15 juin 08 à 13:29, Arnaud Spiwack a écrit :

> > 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.

Of course, but the only means of informing the reduction machine of  
some strategy is through that information (as of now) and I don't see  
any other way of getting as-reasonable-as-possible reductions with  
unchecked fixpoints. My proposal is geared towards functions that are  
actually structurally decreasing but where the syntactic criterion  
fails. { unchecked-struct } might be a better name?

--
Matthieu Sozeau
http://www.lri.fr/~sozeau