The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

---

De: "Abhishek Anand" <abhishek.anand.iitg AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mercredi 11 Janvier 2017 19:34:15
Objet: Re: [Coq-Club] Question about the formal definition of the guard condition

For a fix, can I ask Coq to give me the version of its body for which the guard conditions were checked?

The kernel does not implement this feature, unfortunately :(

Is it the same as doing "Eval compute in (fix ...)"?

No, see below.

I understand that this version may be excessively bloated (beyond the limits of human understanding) due to all the unfoldings.

Instead of blindly normalizing the body of a fixpoint, can Coq proceed lazily, only normalizing subterms of the body where the guard condition fails?

This is what Coq does, roughly. It is slightly less lazy as it performs beta-iota-zeta eagerly.

Suppose that Coq stored only the versions (of bodies of fix) on which guard checks were done, and discarded whatever the user wrote.

Would Coq then be strongly normalizing?

As far as I can tell, yes, but I'm not aware of any proof if this.

Another useful meta-theoretic property of interest is that all typing judgments are closed under definitional equality.

Not sure what this property would be really useful for, but it does not hold for Coq because of cumulativity:

|- True : Prop holds but |- let x:Type :=True in x : Prop does not.

Only reduction is supposed to preserve typing (a.k.a subject reduction)

 Thus, it seems that Coq's kernel (not what user writes) cannot accept 

"fix F (n : nat) := 0" and reject "fix F (n : nat) := let x := F n in 0", as long as reductions are allowed inside bodies of fixpoints.

No, we could imagine a fix of the guard condition that rejects the second example, and I conjecture it would restore SN: before beta-reducing ((fun x:T=>e1) e2), we could check that T and e2 do not do illegal recursive calls (but yet allow partial application of the fixpoint). Similarly for zeta and iota, checking that all subterms that disappear are not doing illegal recursive calls.

Do we also need to ban reductions inside bodies of fixpoints?

Banning reductions under binders without extreme care breaks subject-reduction.

Hope this helps.

Bruno Barras.