Some of the things I've learned every day since Oct 10, 2016
67: Confluence (Rewriting Systems)
December 18, 2016Posted by on
A term within a rewriting system (such as one in the lambda calculus) is confluent if, for any pair of terms such that and (where means is a reduct of under 0 or more reductions), there exists a term such that and . If every term in a system is confluent, the system itself is said to be confluent.
Systems which are both confluent and terminating are especially nice, because any sequence of reductions can be applied to a given term with the resulting irreducible reduct being the same.