Hispanopedia Wiki
Articulo de referencia

Teorema de Church-Rosser

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

Hispanopedia WikiContenido en espanolLectura gratuita

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

Más precisamente, si existen dos reducciones distintas o secuencias de reducciones que se pueden aplicar al mismo término, entonces existe un término que se puede obtener 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 se simboliza mediante el diagrama adjunto: si el término a se puede reducir tanto a b como a c , entonces debe existir otro término d (posiblemente igual a b o a c ) al que se puedan reducir ambos . 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 se cumple para la β-reducción en el cálculo λI (en el que cada variable abstracta debe aparecer en el cuerpo del término). El método de demostración 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 las reducciones se pueden realizar de izquierda a derecha para alcanzar una forma normal (si existe). El resultado para el cálculo lambda puro no tipado fue demostrado por DE Schroer en 1965. [ 2 ]

Cálculo lambda puro sin tipos

Un tipo de reducción en el cálculo lambda puro no tipado para el cual se aplica el teorema de Church-Rosser es la β-reducción, en la cual un subtérmino de la forma(λincógnita.t)s{\displaystyle (\lambda xt)s}se contrae mediante la sustituciónt[incógnita:=s]{\displaystyle t[x:=s]}, dóndet,s{\displaystyle t,s}son dos expresiones lambda. Si la β-reducción se denota por→β{\displaystyle \rightarrow _{\beta }}y su cierre reflexivo y transitivo por↠β{\displaystyle \twoheadrightarrow _{\beta }}Entonces el teorema de Church-Rosser es que: [ 3 ]

∀METRO,norte1,norte2∈Λ:si METRO↠βnorte1 y METRO↠βnorte2 entonces ∃incógnita∈Λ:norte1↠βincógnita y norte2↠βincógnita{\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{si}}\ M\twoheadrightarrow _{\beta }N_{1}\ {\text{y}}\ M\twoheadrightarrow _{\beta }N_{2}\ {\text{entonces}}\ \exists X\in \Lambda :N_{1}\twoheadrightarrow _{\beta }X\ {\text{y}}\ 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: [ 4 ]

∀METRO,norte∈Λ:si λβ⊢METRO=norte entonces ∃incógnita:METRO↠βincógnita y norte↠βincógnita{\displaystyle \forall M,N\in \Lambda :{\text{si}}\ \lambda \beta \vdash M=N\ {\text{entonces}}\ \exists X:M\twoheadrightarrow _{\beta }X\ {\text{y}}\ N\twoheadrightarrow _{\beta }X}

El teorema también se aplica a la η-reducción, en la que un subtérminoλincógnita.Sincógnita{\displaystyle \lambda x.Sx}es reemplazado porS{\displaystyle S}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 proviene de William W. Tait y Per Martin-Löf . [ 5 ] Digamos que una relación binaria→{\displaystyle \rightarrow }Satisface la propiedad del diamante si:

∀METRO,norte1,norte2∈Λ:si METRO→norte1 y METRO→norte2 entonces ∃incógnita∈Λ:norte1→incógnita y norte2→incógnita{\displaystyle \forall M,N_{1},N_{2}\in \Lambda :{\text{si}}\ M\rightarrow N_{1}\ {\text{y}}\ M\rightarrow N_{2}\ {\text{entonces}}\ \exists X\in \Lambda :N_{1}\rightarrow X\ {\text{y}}\ N_{2}\rightarrow X}

Entonces, la propiedad Church-Rosser es la afirmación de que↠β{\displaystyle \twoheadrightarrow _{\beta }}Satisface la propiedad del diamante. Introducimos una nueva reducción.→‖{\displaystyle \rightarrow _{\|}}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, se deduce que↠β{\displaystyle \twoheadrightarrow _{\beta }}Satisface la propiedad del diamante.

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

  • METRO→‖METRO{\displaystyle M\rightarrow _{\|}M}
  • SiMETRO→‖METRO′{\displaystyle M\rightarrow _{\|}M'}ynorte→‖norte′{\displaystyle N\rightarrow _{\|}N'}entoncesλincógnita.METRO→‖λincógnita.METRO′{\displaystyle \lambda xM\rightarrow _{\|}\lambda xM'}yMETROnorte→‖METRO′norte′{\displaystyle MN\rightarrow _{\|}M'N'}y(λincógnita.METRO)norte→‖METRO′[incógnita:=norte′]{\displaystyle (\lambda xM)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 ]

SiMETRO→βnorte1{\displaystyle M\rightarrow _{\beta }N_{1}}yMETRO→ηnorte2{\displaystyle M\rightarrow _{\eta }N_{2}}entonces existe un términoincógnita{\displaystyle X}de tal manera quenorte1→ηincógnita{\displaystyle N_{1}\rightarrow _{\eta }X}ynorte2→βincógnita{\displaystyle N_{2}\rightarrow _{\beta }X}.

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

Variantes

El teorema de Church-Rosser también se cumple para muchas variantes del cálculo lambda, como el cálculo lambda con 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 estricta ) es una función que asigna valores a los programas (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

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.
  • Church, 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), El cálculo lambda: su sintaxis y semántica , Estudios en lógica y fundamentos de las matemáticas, vol.  103 (edición revisada  ), North Holland, Ámsterdam, ISBN 0-444-87508-5Archivado del original el 23 de agosto de 2004.. Errata .