Confluence

Summary

A rewriting system is confluent when any two ways of rewriting an object can be continued so that they meet again. Confluence implies that each object has at most one normal form. So the result of a computation does not depend on the order of the steps. It is equivalent to the Church–Rosser property: two objects are equivalent exactly when they rewrite to a common object. Confluence of the lambda calculus is the Church–Rosser theorem.