The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hello Cedric,

reduction is designed in a way that it is strongly normalizing in 
arbitrary contexts.

On 2/8/12 10:08 AM, AUGER Cédric wrote:
> Furthermore, in your example, the recursive call to "non_wf_not_wf"
> is under a "match with", so it is already in head normal form; to fit
> my examples,
>
>   Fixpoint non_wf_not_wf (n:nat) (Hacc:Acc non_wf n)
>     {struct Hacc} : False :=
>   non_wf_not_wf (S n) match Hacc with
>                       | Acc_intro f =>  f (S n) (non_wf_const n))
>                       end.
> would have been better; and shows a case where a fixpoint is a direct
> application to itself (and thus breaking one of the comments on my
> previous mail), but in fact, I don't see any case where you can define
> fxpoints from non empty types to non empty types (in a consistent
> environment) which is defined by a direct call to itself applied to
> some wisely chosen parameters. I guess it is not possible, since it
> seems such functions would be endlessly reduceable.

More reductions are safe in for closed terms, as you observe.  To enable 
these consistently, one would have to carry around for each term whether 
it is closed.  I am not sure the infrastructure for this is there in Coq.

> > On a somewhat related note, I've been wondering whether it would be
> > possible to add a reduction of
> >
> > match (match a with
> >             | const1 =>  expr1
> >             | const2 =>  expr2
> >             end) with
> > | const1' =>  expr1'
> > | const2' =>  expr2'
> > end
> >
> > to
> >
> > match a with
> > | const1 =>  match expr1 with
> >    | const1' =>  expr1'
> >    | const2' =>  expr2'
> >    end
> > | const2 =>  match expr2 with
> >    | const1' =>  expr1'
> >    | const2' =>  expr2'
> >    end
> > end.

Hugo has a lot to say about these "commutative cuts", see p32 of his 
talk here:

  http://yquem.inria.fr/~herbelin/talks/cic.pdf

These reductions are difficult for dependent eliminations.

Cheers,
Andreas

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/