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 o secuencias de reducciones distintas que se pueden aplicar al mismo término, entonces existe un término que se puede alcanzar a partir de ambos resultados, aplicando secuencias (posiblemente vacías) de reducciones adicionales. El teorema fue demostrado en 1936 por Alonzo Church y J. Barkley Rosser, de quien recibe su nombre.

El teorema está simbolizado por el diagrama adyacente: si el término a se puede reducir tanto a b como a c, entonces debe haber un término adicional d (posiblemente igual a b o c) al que tanto b como c se puede reducir. Al ver 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 se cumple 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 llegar a una forma normal (si uno existe). El resultado del cálculo lambda puro sin tipo fue demostrado por D. E. Shroer en 1965.

Cálculo lambda puro sin tipo

Un tipo de reducción en el cálculo de lambda pura sin tipo para el cual se aplica el teorema de la Iglesia-Rosser es la reducción β, en la que un subtermio de la forma ()λ λ x.t)s{displaystyle (lambda x.t)s} es contratado por la sustitución t[x:=s]{displaystyle t[x:=s]}. Si β-reducción es denotado por → → β β {displaystyle rightarrow _{beta } y su cierre reflexivo y transitivo ↠ ↠ β β {displaystyle twoheadrightarrow _{beta } entonces el teorema de la Iglesia-Rosser es que:

О О M,N1,N2▪ ▪ ▪ ▪ :siM↠ ↠ β β N1yM↠ ↠ β β N2entonces∃ ∃ X▪ ▪ ▪ ▪ :N1↠ ↠ β β XyN2↠ ↠ β β X{displaystyle forall M,N_{1},N_{2}in Lambda:{text{if} Mtwoheadrightarrow _{beta - No. Mtwoheadrightarrow _{beta No. exists Xin 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 λ λ β β {displaystyle lambda beta } debe reducirse a un término común:

О О M,N▪ ▪ ▪ ▪ :siλ λ β β ⊢ ⊢ M=Nentonces∃ ∃ X:M↠ ↠ β β XyN↠ ↠ β β X{displaystyle forall M,Nin Lambda:{text{if} lambda beta vdash M=N {text{then}\fn}\fnfn} exists X:Mtwoheadrightarrow _{beta }X {text{and} Ntwoheadrightarrow _{beta }X}

El teorema también se aplica a la reducción de la pira, en la cual un subtermino λ λ x.Sx{displaystyle lambda x. Sx! es reemplazado por S{displaystyle S.. También se aplica a la reducción de βega, la unión de las dos reglas de reducción.

Prueba

Para la reducción de β, un método de prueba se origina de William W. Tait y Per Martin-Löf. Digamos que una relación binaria → → {displaystyle rightarrow } satisfecha la propiedad del diamante si:

О О M,N1,N2▪ ▪ ▪ ▪ :siM→ → N1yM→ → N2entonces∃ ∃ X▪ ▪ ▪ ▪ :N1→ → XyN2→ → X{displaystyle forall M,N_{1},N_{2}in Lambda:{text{if} Mrightarrow N_{1} {texto {y}} Mrightarrow N_{2}text{then} exists Xin Lambda:N_{1}rightarrow X ' {text{and} N_{2}rightarrow X.

Entonces la propiedad Iglesia-Rosser es la declaración de que ↠ ↠ β β {displaystyle twoheadrightarrow _{beta } satisface la propiedad de diamantes. Presentamos una nueva reducción → → .. {displaystyle rightarrow _{fncipes} cuyo cierre transitivo reflexivo es ↠ ↠ β β {displaystyle twoheadrightarrow _{beta } y que satisface la propiedad del diamante. Por inducción sobre el número de pasos en la reducción, sigue así que ↠ ↠ β β {displaystyle twoheadrightarrow _{beta } satisface la propiedad de diamantes.

La relación → → .. {displaystyle rightarrow _{fncipes} tiene las reglas de formación:

• M→ → .. M{displaystyle Mrightarrow _{fncip}M}
• Si M→ → .. M.{displaystyle Mrightarrow _{fncip}M'} y N→ → .. N.{displaystyle Nrightarrow _{fncip}N'} entonces λ λ x.M→ → .. λ λ x.M.{displaystyle lambda x. Mrightarrow _{fncip}lambda x.M'} y MN→ → .. M.N.{displaystyle MNrightarrow _{fncip}M'N'} y ()λ λ x.M)N→ → .. M.[x:=N.]{displaystyle (lambda x.M)Nrightarrow _{fncip}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 η se conmutan en el sentido de que:

Si M→ → β β N1{displaystyle Mrightarrow _{beta }N_{1} y M→ → .. N2{displaystyle Mrightarrow _{eta }N_{2} entonces existe un término X{displaystyle X} tales que N1→ → .. X{displaystyle ################################################################################################################################################################################################################################################################ y N2→ → β β X{displaystyle ¿Qué?.

Por lo tanto, podemos concluir que la reducción βη es Church-Rosser.

Normalización

Una regla de reducción que satisface la propiedad Iglesia-Rosser tiene la propiedad que cada término M puede tener en la mayoría de una forma normal distinta, como sigue: si X y Y son formas normales M entonces por la propiedad Iglesia-Rosser, ambos reducen a un término igual Z. Ambos términos ya son formas normales X=Z=Y{displaystyle X=Z=Y.

Si una reducción se normaliza fuertemente (no hay caminos de reducción infinitos) entonces una forma débil de la propiedad Iglesia-Rosser implica la propiedad completa (ver la lema de Newman). La propiedad débil, para una relación → → {displaystyle rightarrow }, es:

О О M,N1,N2▪ ▪ ▪ ▪ :{displaystyle forall M,N_{1},N_{2}in Lambda: si M→ → N1{displaystyle Mrightarrow N_{1} y M→ → N2{displaystyle Mrightarrow N_{2} entonces existe un término X{displaystyle X} tales que N1↠ ↠ X{displaystyle N_{1}twoheadrightarrow X. y N2↠ ↠ 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 de valor beta de Gordon Plotkin. Plotkin también usó 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 programas a 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.