[TYPES] What are congruence rules called?
Gabriel Scherer
gabriel.scherer at gmail.com
Tue Jul 4 12:09:38 EDT 2017
In your 2003 paper "Call-by-value is dual to call-by-name", you use ς
(\varsigma) for a rule that brings a subterm under an evaluation
context to the head of the term -- this is a sequent calculus so the
operational semantics is more like abstract machines than lambda
terms. Guillaume Munch-Maccagnoni reused this letter, starting in
"Focalisation and Classical Realisability", 2009, for rules that bring
the head focus into reducible subterms, but his presentation does it
in a more atomic way, with a family of rules for each connective. A
non-deterministic presentation of these rules would be
<(t, t') | u> →ς(⊗)₁ <t | μx. <(x, t') | u>>
<(t', t) | u> →ς(⊗)₂ <t | μx. <(t', x) | u>>
<t | t' · u> →ς(→)₁ <t | μx. <x | t' · u>>
<t' | t · u> →ς(→)₂ <t | μx. <t' | x · u>>
etc. (when t is not a value)
I think it would be reasonable to name lambda-term congruence rules in
the same way.
They directly reduce a subterm instead of bringing it in head position
in an abstract machine, but they are similar.
Aside: note that these confluence rules may not be the most flexible
way to describe reduction. If you want to describe parallel reduction
(for a confluence proof for example), you need to give different
rules. Both can be subsumed by defining multi-hole contexts E[□₁, □₂,
..., □ₙ], and having a single confluence rule over those; various
flavors of parallel reduction, as well as the standard reduction,
arise as special cases. Didier Rémy and I used this presentation in
"Full reduction in the face of absurdity", 2015.
More information about the Types-list
mailing list