Re: [TYPES] What are congruence rules called?

[ 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.