The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

In fact, it is clearer with the term fun n => my_identity n.

Maxime.

On 11/14/16 13:46, Maxime Dénès wrote:
> Hi Randy,
> 
> If I read correctly, this restriction is needed even without axioms as
> soon as you have strong reduction (i.e. under lambdas, match):
> 
> Fixpoint my_identity (n : nat) :=
>   match n with
>   | O => O
>   | S p => S (my_identity p)
>   end.
> 
> Consider the normal form of my_identity. You don't want to infinitely
> expand the recursive call.
> 
> Maxime.
> 
> On 11/14/16 13:35, Randy Pollack wrote:
>> Page 134 of the reference manual (8.5pl2) describes the reduction rule
>> for a fixpoint application:
>>
>> ================================
>> The reduction for fixpoints is:
>>    [...]
>> when aki starts with a constructor. This last restriction is needed in
>> order to keep strong normalization.
>> ==================================
>>
>> Is is known if this last restriction is needed when the context in
>> which the fixpoint application is well typed doesn't contain any
>> axioms?  (References or examples?)
>>
>> What about for specific axioms, such as functional extensionality, axiom 
>> K, ...?
>>
>> Thanks,
>> --Randy
>>