The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Sorry, I should have said "call by value" in my question.  That is
what I'm most interested in.  References?

Thanks,
--Randy


On Mon, Nov 14, 2016 at 1:01 PM, Pierre Courtieu
<pierre.courtieu AT gmail.com>
 wrote:
> 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
>> >
>
>