The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

If I understand correctly, your question is about the aki in the right hand side, and you're asking why the constructor wasn't stripped off of the term, is that correct?

If so, then the answer is that the right-hand side is correct, as deconstructing a term and unfolding a fix (doing recursion) are different operations: they are separated into the fix and match construct.

The restriction makes it impossible to infinitely apply the Fix unfolding *in the case that aki is de-constructed by the term ti before being applied to the recursive call*, which much happen if the *guard condition* for termination is satisfied.

I think the last sentence simply means that with this restriction (and the guardedness condition), we can exactly simulate the recursors' operational semantics, even on open terms (and vice-versa, I think, but this is non-trivial).

Best,

Cody

On Sat, Jun 11, 2016 at 5:12 PM, Randy Pollack <rpollack0 AT gmail.com> wrote:

I don't understand this description of fixpoint reduction from p. 134
of the Reference Manual (.pdf, version 8.5pl1).

====================================
Let F be the set of declarations: f1/k1:A1 := t1 ... fn/kn:An := tn.
The reduction for fixpoints is:

(Fix fi{F} a1 . . . aki)  >_i
       ti {(fk /Fix fk {F})k=1...n} a1 . . . aki

when aki starts with a constructor. This last restriction is needed
in order to keep strong normalization and corresponds to the reduction
for primitive recursive operators.
====================================

Is a_{k_i} in the reduction rule a typo?  Can someone explain the
phrase "and corresponds to the reduction
for primitive recursive operators".

Thanks,
Randy
--