En el cálculo lambda , el teorema de Church-Rosser establece que, al aplicar las reglas de reducción a los 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 se pueden aplicar al mismo término, entonces existe un término que es accesible a partir de ambos resultados, aplicando secuencias (posiblemente vacías) de reducciones adicionales. [1] El teorema fue probado en 1936 por Alonzo Church y J. Barkley Rosser , de quienes recibe su nombre.
El teorema está simbolizado por el diagrama adyacente: Si término una puede reducirse a ambos b y c , entonces debe ser un término más d (posiblemente igual a o bien b o c ) a la que tanto b y c pueden ser reducidos. 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 a lo sumo una forma normal , lo que justifica la referencia a " el 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 los 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 no tipificado fue probado por DE Shroer 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 un subtermo de la forma es contratado por la sustitución . Si la reducción β se denota por y su cierre reflexivo, transitivo por entonces el teorema de Church-Rosser es que: [3]
Una consecuencia de esta propiedad es que dos términos iguales en debe reducirse a un término común: [4]
El teorema también se aplica a la reducción η, en la que un subtermo es reemplazado por . También se aplica a la reducción βη, la unión de las dos reglas de reducción.
Prueba
Para la reducción β, un método de prueba se origina en William W. Tait y Per Martin-Löf . [5] Digamos que una relación binaria satisface la propiedad del diamante si:
Entonces, la propiedad Church-Rosser es la afirmación de 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.
La relación tiene las reglas de formación:
- Si y luego y y
Se puede probar directamente que la regla de reducción η es 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 .
Por tanto, podemos concluir que βη-reducción es 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 por la propiedad de Church-Rosser, ambos se reducen a un plazo igual Z . Ambos términos ya son formas normales, así que. [4]
Si una reducción se normaliza fuertemente (no hay caminos de reducción infinitos), entonces una forma débil de la propiedad Church-Rosser implica la propiedad completa. La propiedad débil, para una relación, es: [8]
- Si y entonces existe un término tal que y .
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 de valores beta de Gordon Plotkin . Plotkin también se utiliza un teorema Iglesia-Rosser para demostrar que la evaluación de los programas funcionales (tanto para la evaluación perezosa y evaluación ansiosos ) 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 confluye .
Notas
- ↑ Alama (2017) .
- ^ Barendregt (1984) , p. 283.
- ^ Barendregt (1984) , p. 53–54.
- ↑ a b Barendregt (1984) , p. 54.
- ^ Barendregt (1984) , p. 59-62.
- ^ Barendregt (1984) , p. 64–65.
- ^ Barendregt (1984) , p. 66.
- ^ Barendregt (1984) , p. 58.
Referencias
- Alama, Jesse (2017). Zalta, Edward N. (ed.). La Enciclopedia de Filosofía de Stanford (edición de otoño de 2017). Laboratorio de Investigación en Metafísica, Universidad de Stanford.
- Iglesia, Alonzo ; Rosser, J. Barkley (mayo de 1936), "Algunas propiedades de la conversión" (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, 103 (Ed. Revisada), North Holland, Amsterdam, ISBN 0-444-87508-5, archivado desde el original el 23 de agosto de 2004. Errata .