Wojciech Nawrocki (Jul 11 2022 at 23:25): 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.
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.
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: Sep 23 2023 at 15:01 UTC