Teorema de Church-Rosser

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 distintas o secuencias de reducciones que se pueden aplicar al mismo término, entonces existe un término que es accesible desde 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 el término a se puede reducir tanto a byc , entonces debe haber un término adicional d (posiblemente igual a b o c ) al que se pueden reducir tanto b como 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 a lo sumo una forma normal , lo que justifica la referencia a " el forma normal "de un término normalizable dado.

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 todas las variables abstractas deben 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 no tipificado fue probado por DE Shroer en 1965. [2]

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 subtermo de la forma . Si la reducción β se denota por y su cierre transitivo reflexivo, entonces el teorema de Church-Rosser es que: [3]

Una consecuencia de esta propiedad es que dos términos iguales en deben reducirse a un término común: [4]