Teorema de Church-Rosser

Teorema en informática teórica

En el cálculo lambda , el teorema de Church-Rosser establece que, al aplicar reglas de reducción a términos , el orden en que se eligen las reducciones no afecta 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 al que se puede llegar 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 quienes recibe su nombre.

El teorema está simbolizado por el diagrama adyacente: Si el término a puede reducirse tanto a b como a c , entonces debe haber un término adicional d (posiblemente igual a b o a c ) al que tanto b como c puedan reducirse. Considerando 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 una). El resultado para el cálculo lambda puro sin tipo fue demostrado por DE Schroer en 1965. ^[2]

Cálculo lambda puro y sin tipo

Un tipo de reducción en el cálculo lambda puro no tipificado para el que se aplica el teorema de Church-Rosser es la β-reducción, en la que un subtérmino de la forma se contrae mediante la sustitución . Si la β-reducción se denota por y su clausura reflexiva y transitiva 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 en 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 se origina 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 el enunciado 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 sigue 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. Luego, 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 lo 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, de la siguiente manera: si X e Y son formas normales de M entonces, por la propiedad de Church-Rosser, ambos se reducen a un término igual Z . Ambos términos ya son formas normales, por lo que . ^[4] ${\displaystyle X=Z=Y}$

Si una reducción es fuertemente normalizante (no hay caminos infinitos de reducción), entonces una forma débil de la propiedad de Church-Rosser implica la propiedad completa (véase 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 tipos simples , muchos cálculos con sistemas de tipos avanzados y el cálculo de valores 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 ansiosa ) es una función de programas a valores (un subconjunto de los términos lambda).

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

Notas

1. Alama (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ág. 64–65.
7. Barendregt (1984), pág. 66.
8. Barendregt (1984), pág. 58.

Referencias

• Alama, Jesse (2017). Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy (edición de otoño de 2017). Metaphysics Research Lab, Universidad de Stanford.
• Church, Alonzo ; Rosser, J. Barkley (mayo de 1936), "Algunas propiedades de conversión" (PDF) , Transactions of the American Mathematical Society , 39 (3): 472–482, doi : 10.2307/1989762 , JSTOR  1989762.
• Barendregt, Hendrik Pieter (1984), El cálculo lambda: su sintaxis y semántica, Estudios de lógica y fundamentos de las matemáticas, vol. 103 (edición revisada), Holanda Septentrional, Ámsterdam, ISBN 0-444-87508-5, archivado desde el original el 23 de agosto de 2004. Fe de erratas.