Rho Calculus (Rewriting Calculus)

Origin. Horatiu Cirstea and Claude Kirchner, "The rewriting calculus, parts I and II" (Logic Journal of the IGPL, 2001), with the ELAN system as the practical setting; developed with Liquori, Wack, and Bertolissi through the 2000s. The aim: λ-calculus and term rewriting are the two computational models of the field and are always presented separately, so give them one calculus.

Models. In λ, abstraction binds a variable: λx. t. In rewriting, a rule matches a pattern: l → r. The ρ-calculus makes the pattern the binder — ρ generalizes λ by abstracting over an arbitrary term rather than a variable, so λx. t is the special case where the pattern is a variable and matching is trivial. Rewriting is not added to λ; λ is recovered as a fragment.

Formalism.

Abstraction on patterns: P → t — the rule abstracting pattern P, body t λx. t is P → t with P = x. Application (P → t) u fires by matching u against P, not by substitution.

Terms: t ::= x | f(t̄) | P → t | t t | t ⋏ t | ∅ ⋏ is the structure operator: a collection of results, since matching may succeed several ways. ∅ is failure: matching did not apply.

Reduction: (P → t) u →_ρ σ(t) where σ = the solution of the matching problem P ≪ u If no solution: →_ρ ∅. If several: →_ρ the ⋏ of the instances. Non-determinism is a first-class result, not a choice.

Matching theory as a parameter: The calculus is parametrized by the matching theory T. Syntactic matching gives λ back. Associative-commutative matching gives AC-rewriting. Higher-order matching gives higher-order rewriting. One calculus, one parameter, the whole family.

What ∅ and ⋏ add: Rule failure and rule non-determinism are terms, so strategies are expressible inside the calculus. In ELAN and Tom, strategy languages are ρ-terms rather than a meta-level.

Confluence: Not automatic — the calculus is confluent only under conditions on the matching theory and the patterns. The unrestricted calculus is not confluent, which is the standard difficulty of combining rewriting with λ.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Rightwards arrow	Rule abstraction, pattern to body; generalizes λ
≪	U+226A	Much less-than	Matching problem, P ≪ u: match u against P
⋏	U+22CF	Curly logical and	Structure operator, a collection of results
∅	U+2205	Empty set	Failure: matching did not apply
ρ	U+03C1	Greek small letter rho	The calculus, and its reduction relation →_ρ
λ	U+03BB	Greek small letter lamda	Abstraction, the case where the pattern is a variable
σ	U+03C3	Greek small letter sigma	The substitution solving a matching problem
t̄	—	Vector notation	A sequence of arguments; the overbar is a combining macron, U+0304
P	—	Pattern	The term abstracted over
T	—	Matching theory	The parameter the calculus is taken relative to
→_ρ	—	Rho reduction	One step of the calculus
::=	—	Grammar production	Defines the term syntax

Metatheory. Making the pattern the binder is the move: it subsumes λ without extending it, since abstraction over a variable is abstraction over the trivial pattern, and it makes rewriting's matching the application rule rather than a separate mechanism. Restricting patterns to variables and the theory to syntactic matching recovers the λ-calculus exactly, so the ρ-calculus is a conservative extension of it and is Turing complete. Parametrizing by the matching theory is the second move: the same calculus is λ, AC-rewriting, or higher-order rewriting depending on one input, which is what a unification of the two models should look like. The cost shows in confluence. Combining rewriting with λ has always broken it, and the ρ-calculus does not repair the failure so much as locate it precisely — Cirstea and Kirchner obtain confluence only under restrictions on the patterns, algebraic and linear, and on the matching theory, while the unrestricted calculus is not confluent. Typed versions exist: the Pure Pattern Type Systems of Barthe, Cirstea, Kirchner and Liquori (2003) generalize Barendregt's pure type systems to pattern abstraction.

Applies to. Rule-based programming — ELAN, Tom, and the strategy languages built on them. Unified accounts of λ and rewriting. Pattern matching as a primitive rather than a compilation target. Strategy languages, which become object-level.

Limitations. Confluence is a property of an instantiation rather than of the calculus. The conditions sit on the matching theory and on the shape of patterns, so the same syntax is confluent or not depending on a parameter supplied from outside, and no theorem about the ρ-calculus as such may assume unique normal forms. Normalization and typing are in the same position and have to be re-established for each theory. Reduction is effective only when the matching problem is decidable, which is again a condition on the parameter — higher-order unification is undecidable (Goldfarb 1981). Non-linear patterns, where a variable occurs twice, require an equality test on the matched subterms, so a decision procedure is smuggled into the reduction rule itself. And the generality comes from leaving the properties one wants as parameters, over a literature that is small and largely one group's.