The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Like Maxime said the fix-reduction is only the unfolding of the fixpoint definition, which leads to infinite unfolding if not constrained.

I guess people in this list will give examples of some deeper modifications of the whole reduction relation (like using the call-by-value strategy?) that lead to special good properties on closed terms under axiom-free environments.

P.

2016-11-14 13:46 GMT+01:00 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
>