Church-Rosser theorem

The Church-Rosser theorem (proven in 1936 by Alonzo Church and John Barkley Rosser ) is an important result from the theory of the lambda calculus . One consequence of this theorem is that each term in the lambda calculus has at most one normal form. The Church-Rosser theorem allows generalizations to abstract reduction systems .

The statement of the theorem

The Church-Rosser theorem says the following: If two different terms a and b are equivalent , i.e. H. can be transformed into each other with reduction steps in any direction, then there is a further term c to which both a and b can be reduced.

Formal definitions

Let be the reduction relation in the lambda calculus; d. H. the relation defined by the -, - and - conversions. This makes the lambda calculus a special case of a reduction system ; especially a term rewriting system . ${\displaystyle \rightarrow }$ ${\displaystyle \alpha }$ ${\displaystyle \beta }$ ${\displaystyle \eta }$

${\displaystyle {\stackrel {*}{\rightarrow }}}$is the transitive envelope of (the union of the relation with the identity relation ), i.e. H. is the smallest quasi-order ( reflexive and transitive relation) that contains. It is also the reflexive and transitive shell of . ${\displaystyle \rightarrow \cup =}$ ${\displaystyle \rightarrow }$ ${\displaystyle {\stackrel {*}{\rightarrow }}}$ ${\displaystyle \rightarrow }$ ${\displaystyle \rightarrow }$

${\displaystyle \leftrightarrow }$is , d. H. the union of the relation with its inverse relation ; is also known as the symmetrical envelope of . is the transitive envelope of . ${\displaystyle \rightarrow \cup \rightarrow ^{-1}}$ ${\displaystyle \rightarrow }$ ${\displaystyle \leftrightarrow }$ ${\displaystyle \rightarrow }$ ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$ ${\displaystyle \leftrightarrow }$

The Church-Rosser theorem can then be formulated as follows:

Theorem (Church-Rosser): Let and be two terms in the lambda calculus and , then there is a term with and . ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a{\stackrel {*}{\leftrightarrow }}b}$ ${\displaystyle c}$ ${\displaystyle a{\xrightarrow {*}}c}$ ${\displaystyle b{\xrightarrow {*}}c}$

Church-Rosser quality and confluence

In abstract reduction systems, the Church-Rosser property is defined as follows:

Definition: The reduction relation is called “Church-Rosser” (or “has the Church-Rosser property”) if the following applies to all terms a and b: From , it follows that a term exists with and . ${\displaystyle \rightarrow }$ ${\displaystyle a{\stackrel {*}{\leftrightarrow }}b}$ ${\displaystyle c}$ ${\displaystyle a{\xrightarrow {*}}c}$ ${\displaystyle b{\xrightarrow {*}}c}$

The following definition of confluence is also important :

Definition (see picture on the right for illustration): A reduction system is called confluent if there are three terms a, b and c with a term d with and . ${\displaystyle a{\xrightarrow {*}}b,a{\xrightarrow {*}}c}$ ${\displaystyle b{\xrightarrow {*}}d}$ ${\displaystyle c{\xrightarrow {*}}d}$

Sentence . In an abstract reduction system (ARS) the following conditions are equivalent: (i) the system has the Church-Rosser property, (ii) it is confluent.

Inference . If in a confluent ARS then ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$

• if x and y are normal forms, then x = y,
• if y is a normal form then is . ${\displaystyle x{\stackrel {*}{\rightarrow }}y}$

literature

• Alonzo Church, J. Barkley Rosser: Some properties of conversion. In: Transactions of the American Mathematical Society. Volume 39, No. 3, May 1936, pp. 472-482.
• Franz Baader, Tobias Nipkow: Term Rewriting and All That . Cambridge University Press 1999, ISBN 0-521-77920-0 , pp. 9-11.

Web links

• Eric W. Weisstein : Church-Rosser Theorem . In: MathWorld (English).

Individual evidence

1. ↑ F. Baader, T. Nipkow, p. 11.