Church–Rosser theorem

In the untyped lambda calculus, any two terms related by beta-conversion can each reduce by beta-reduction to a common term. This establishes confluence of beta-reduction.

Beta reduction: The lambda-calculus operation that substitutes an argument for a bound variable in an application. The theorem says divergent sequences of these steps can reach a shared result.
Lambda calculus: A formal system for expressing computation using function abstraction, application, and variable binding. The theorem is a central property of its untyped version.
Alonzo Church: An American mathematician and logician who developed the lambda calculus and the Church–Turing thesis. The theorem bears his name and belongs to the calculus he developed.
Unique normal form: A property stating that each term has at most one irreducible result under a reduction relation. Confluence ensures any beta-normal forms of a term are identical up to renaming bound variables.
Confluence: A property of a rewriting system in which divergent rewrite paths can be extended to a common result. The theorem establishes this property for beta-reduction.
Beta-conversion: The equivalence relation generated by beta-reduction and its inverse. The theorem's premise is that two terms are equivalent under this relation.
J. Barkley Rosser: An American logician and mathematician known for work in logic, number theory, and computation. Rosser collaborated with Church on the theorem's original proof.
Normalization: The process of reducing an expression to a form with no applicable reduction steps. The theorem guarantees agreement among normal forms when reduction reaches them.
Parallel reduction: A lambda-calculus relation that contracts multiple beta-redexes simultaneously in one step. Its diamond property provides a proof route to confluence of ordinary beta-reduction.
Beta-normal form: A lambda term containing no subexpression to which beta-reduction applies. When convertible terms have normal forms, confluence makes those forms unique.

Linked from 3 pages

Combinatory logicRelated: It explains why different reduction paths can still agree when they reach normal forms.