[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.
