Coq Call 2024 02 12 - coq/coq GitHub Wiki

Topics

  • Proposition to talk about primitive projections: which positive/negative simulations, which algebraic presentations, which optimized representations, which control of reduction, which disambiguation of names? (see Zulip, Hugo 10-30 minutes) [postponed]
  • Proposition otherwise to talk about reduction strategies, if no other urgencies (CEP #85, Hugo):
    • do we want fixpoint/cofixpoint refolding in cbv and lazy and, if yes, or if yes at least optionally, how to implement it?
      • by modifying the reduction machines?
        • à la simpl, by computing an optimal refolding for each unfolded constant
        • à la cbn, by incorporating possible refolding in the evaluation stack and choosing the optimal one
      • by telling how to refold (co)fixpoint in the Fix/CoFix node when such refolding exist (drawback: we would refold only to the closest surrounding constant; on the other side, this is what we are doing already for mutual fix; it is also somehow a canonical refolding)?
    • do we try to unify the features of simpl/cbn/cbv/lazy?
      • adding support for selecting a pattern in all of them, and, if yes, with which syntax:
        • a possibility would be to reuse the with syntax of auto, e.g. lazy pattern with [constants], and documenting the syntax lazy [constants] as a shortcut for lazy pattern with [constants]
      • adding support for beta, iota, zeta, delta flags and [ ... ] lists to simpl (even if forbidding beta and iota in simpl looks a bit useless)
    • we may also allow constructors in the transparency state to control iota-reduction, the same way as we can already control primitive projections reduction by name of projection?
    • a syntax to combine databases of constants to unfold, see CEP #84
    • removal of the user access to hnf?

Roles

  • Chairman: Nicolas Tabareau
  • Secretary:

Notes