The Coq mailing list

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

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
>