Stream: Coq users

Topic: Documentation for cbv internals


view this post on Zulip Wojciech Nawrocki (Jul 11 2022 at 23:25):

Hello! I am wondering if there is any documentation about how cbv operates when particular rules are turned on/off. In particular, are let-bindings treated as WHNF when zeta is off, and is an additional congruence rule added then to reduce the let-body? Things like this.

view this post on Zulip Paolo Giarrusso (Jul 11 2022 at 23:56):

I don't know of better docs, but it seems the standard ones (https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.cbv) answer this specific question:

Normalization is done by first evaluating the head of the expression into weak-head normal form, i.e. until the evaluation is blocked by [...] or a redex for which flags prevent reduction of the redex. Once a weak-head normal form is obtained, subterms are recursively reduced using the same strategy.

IOW, let x := e1 in e2 must be a WHNF without zeta, and both e1 and e2 will be normalized.

view this post on Zulip Wojciech Nawrocki (Jul 12 2022 at 00:02):

Yes, so I'm guessing that turning zeta off makes the set of WHNFs larger. I was just wondering if this kind of thing was explicitly written down.


Last updated: Feb 01 2023 at 13:03 UTC