Teorema de Church-Rosser

En el cálculo lambda , el teorema de Church-Rosser establece que, al aplicar reglas de reducción a términos , el orden en el que se eligen las reducciones no influye en el resultado final.

Más precisamente, si hay dos reducciones o secuencias de reducciones distintas que pueden aplicarse al mismo término, entonces existe un término que es alcanzable a partir de ambos resultados, aplicando secuencias (posiblemente vacías) de reducciones adicionales. ^[1] El teorema fue demostrado en 1936 por Alonzo Church y J. Barkley Rosser , de quien lleva el nombre.

El teorema está simbolizado por el diagrama adyacente: si el término a se puede reducir a b y c , entonces debe haber un término adicional d (posiblemente igual a b o c ) al que se puedan reducir b y c . Al considerar el cálculo lambda como un sistema de reescritura abstracto , el teorema de Church-Rosser establece que las reglas de reducción del cálculo lambda son confluentes . Como consecuencia del teorema, un término en el cálculo lambda tiene como máximo una forma normal , lo que justifica la referencia a " la forma normal" de un término normalizable dado.

Historia

En 1936, Alonzo Church y J. Barkley Rosser demostraron que el teorema es válido para la reducción β en el cálculo λI (en el que cada variable abstraída debe aparecer en el cuerpo del término). El método de prueba se conoce como "finitud de desarrollos" y tiene consecuencias adicionales, como el Teorema de estandarización, que se relaciona con un método en el que se pueden realizar reducciones de izquierda a derecha para alcanzar una forma normal (si existe). El resultado del cálculo lambda puro y sin tipificar lo demostró DE Schroer en 1965. ^[2]

Cálculo lambda puro sin tipo

Un tipo de reducción en el cálculo lambda puro sin tipo para el que se aplica el teorema de Church-Rosser es la reducción β, en la que la sustitución contrae un subtérmino de la forma . Si la reducción β se denota por y su cierre reflexivo y transitivo por entonces el teorema de Church-Rosser es que: ^[3] ${\displaystyle (\lambda x.t)s}$ ${\displaystyle t[x:=s]}$ ${\displaystyle \rightarrow _{\beta }}$ ${\displaystyle \twoheadrightarrow _{\beta }}$

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{if}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{and}}\ M\twoheadrightarrow _{\beta }N_{2}\ {\text{then}}\ \exists X\in \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{and}}\ N_{2}\twoheadrightarrow _{\beta }X}$

Una consecuencia de esta propiedad es que dos términos iguales deben reducirse a un término común: ^[4] ${\displaystyle \lambda \beta }$

${\displaystyle \forall M,N\in \Lambda :{\text{if}}\ \lambda \beta \vdash M=N\ {\text{then}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{and}}\ N\twoheadrightarrow _{\beta }X}$

El teorema también se aplica a la reducción η, en la que un subtérmino se reemplaza por . También se aplica a la reducción βη, la unión de las dos reglas de reducción. ${\displaystyle \lambda x.Sx}$ ${\displaystyle S}$

Prueba

Para la reducción β, un método de prueba proviene de William W. Tait y Per Martin-Löf . ^[5] Digamos que una relación binaria satisface la propiedad del diamante si: ${\displaystyle \rightarrow }$

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{if}}\ M\rightarrow N_{1}\ {\text{and}}\ M\rightarrow N_{2}\ {\text{then}}\ \exists X\in \Lambda :N_{1}\rightarrow X\ {\text{and}}\ N_{2}\rightarrow X}$

Entonces la propiedad de Church-Rosser es la afirmación que satisface la propiedad del diamante. Introducimos una nueva reducción cuyo cierre transitivo reflexivo es y que satisface la propiedad del diamante. Por inducción sobre el número de pasos en la reducción, se deduce que satisface la propiedad del diamante. ${\displaystyle \twoheadrightarrow _{\beta }}$ ${\displaystyle \rightarrow _{\|}}$ ${\displaystyle \twoheadrightarrow _{\beta }}$ ${\displaystyle \twoheadrightarrow _{\beta }}$

La relación tiene las reglas de formación: ${\displaystyle \rightarrow _{\|}}$

• ${\displaystyle M\rightarrow _{\|}M}$
• Si y entonces y y ${\displaystyle M\rightarrow _{\|}M'}$ ${\displaystyle N\rightarrow _{\|}N'}$ ${\displaystyle \lambda x.M\rightarrow _{\|}\lambda x.M'}$ ${\displaystyle MN\rightarrow _{\|}M'N'}$ ${\displaystyle (\lambda x.M)N\rightarrow _{\|}M'[x:=N']}$

Se puede demostrar que la regla de reducción η es directamente de Church-Rosser. Entonces, se puede demostrar que la reducción β y la reducción η conmutan en el sentido de que: ^[6]

Si y entonces existe un término tal que y . ${\displaystyle M\rightarrow _{\beta }N_{1}}$ ${\displaystyle M\rightarrow _{\eta }N_{2}}$ ${\displaystyle X}$ ${\displaystyle N_{1}\rightarrow _{\eta }X}$ ${\displaystyle N_{2}\rightarrow _{\beta }X}$

Por tanto, podemos concluir que la reducción βη es de Church-Rosser. ^[7]

Normalización

Una regla de reducción que satisface la propiedad de Church-Rosser tiene la propiedad de que cada término M puede tener como máximo una forma normal distinta, como sigue: si X e Y son formas normales de M entonces, según la propiedad de Church-Rosser, ambos se reducen a un término igual Z . Ambos términos ya son formas normales . ^[4] ${\displaystyle X=Z=Y}$

Si una reducción es fuertemente normalizante (no hay caminos de reducción infinitos), entonces una forma débil de la propiedad de Church-Rosser implica la propiedad completa (ver el lema de Newman ). La propiedad débil, para una relación , es: ^[8] ${\displaystyle \rightarrow }$

${\displaystyle \forall M,N_{1},N_{2}\in \Lambda :}$si y entonces existe un término tal que y . ${\displaystyle M\rightarrow N_{1}}$ ${\displaystyle M\rightarrow N_{2}}$ ${\displaystyle X}$ ${\displaystyle N_{1}\twoheadrightarrow X}$ ${\displaystyle N_{2}\twoheadrightarrow X}$

Variantes

El teorema de Church-Rosser también es válido para muchas variantes del cálculo lambda, como el cálculo lambda de tipo simple , muchos cálculos con sistemas de tipos avanzados y el cálculo del valor beta de Gordon Plotkin . Plotkin también utilizó un teorema de Church-Rosser para demostrar que la evaluación de programas funcionales (tanto para la evaluación perezosa como para la evaluación entusiasta ) es una función de los programas a los valores (un subconjunto de los términos lambda).

En trabajos de investigación más antiguos, se dice que un sistema de reescritura es Church-Rosser, o que tiene la propiedad Church-Rosser, cuando es confluente .

Notas

1. Alma (2017).
2. Barendregt (1984), pág. 283.
3. Barendregt (1984), pág. 53–54.
4. Barendregt (1984), pág. 54.
5. Barendregt (1984), pág. 59-62.
6. Barendregt (1984), p. 64–65.
7. Barendregt (1984), p. 66.
8. Barendregt (1984), p. 58.

References

• Alama, Jesse (2017). Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy (Fall 2017 ed.). Metaphysics Research Lab, Stanford University.
• Church, Alonzo; Rosser, J. Barkley (May 1936), "Some properties of conversion" (PDF), Transactions of the American Mathematical Society, 39 (3): 472–482, doi:10.2307/1989762, JSTOR 1989762.
• Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103 (Revised ed.), North Holland, Amsterdam, ISBN 0-444-87508-5, archived from the original on 2004-08-23. Errata.