Teorema de Church-Rosser - Church–Rosser theorem

No cálculo lambda , o teorema de Church-Rosser afirma que, ao aplicar regras de redução a termos , a ordem em que as reduções são escolhidas não faz diferença para o resultado final.

Mais precisamente, se houver duas reduções ou sequências de reduções distintas que podem ser aplicadas ao mesmo termo, então existe um termo que pode ser alcançado a partir de ambos os resultados, aplicando sequências (possivelmente vazias) de reduções adicionais. O teorema foi provado em 1936 por Alonzo Church e J. Barkley Rosser , de quem recebeu o nome.

O teorema é simbolizado pelo esquema adjacente: Se termo um pode ser reduzida para ambos b e c , em seguida, tem de haver mais um período d (possivelmente igual, quer b ou c ) para que ambos b e c pode ser reduzida. Vendo o cálculo lambda como um sistema de reescrita abstrato , o teorema de Church-Rosser afirma que as regras de redução do cálculo lambda são confluentes . Como uma consequência do teorema, um termo no cálculo lambda tem, no máximo, uma forma normal , o que justifica a referência a " a forma normal" de um dado prazo normalizable.

História

Em 1936, Alonzo Church e J. Barkley Rosser provaram que o teorema é válido para a redução β no cálculo λI (em que cada variável abstraída deve aparecer no corpo do termo). O método da prova é conhecido como "finitude de desenvolvimentos" e tem consequências adicionais, como o Teorema da Padronização, que se refere a um método no qual as reduções podem ser realizadas da esquerda para a direita para atingir uma forma normal (se houver). O resultado para o cálculo lambda puro não tipado foi provado por DE Shroer em 1965.

Cálculo lambda puro não tipado

Um tipo de redução no cálculo lambda puro não tipado ao qual o teorema de Church-Rosser se aplica é a redução-β, na qual um subtermo da forma é contraído pela substituição . Se a redução β é denotada por e seu fechamento reflexivo e transitivo por, então, o teorema de Church-Rosser é que: ${\ displaystyle (\ lambda xt) s}$${\ displaystyle t [x: = s]}$${\ displaystyle \ rightarrow _ {\ beta}}$${\ displaystyle \ twoheadrightarrow _ {\ beta}}$

${\ displaystyle \ forall M, N_ {1}, N_ {2} \ in \ Lambda: {\ text {if}} \ M \ rightarrow _ {\ beta} N_ {1} \ {\ text {e}} \ M \ rightarrow _ {\ beta} N_ {2} \ {\ text {then}} \ \ exists X \ in \ Lambda: N_ {1} \ twoheadrightarrow _ {\ beta} X \ {\ text {e}} \ N_ {2} \ twoheadrightarrow _ {\ beta} X}$

Uma consequência dessa propriedade é que dois termos iguais em devem se reduzir a um termo comum: ${\ 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 {e}} \ N \ twoheadrightarrow _ {\ beta} X}$

O teorema também se aplica à redução η, na qual um subtermo é substituído por . Também se aplica à redução de βη, a união das duas regras de redução. ${\ displaystyle \ lambda x.Sx}$${\ displaystyle S}$

Prova

Para a redução β, um método de prova origina-se de William W. Tait e Per Martin-Löf . Digamos que uma relação binária satisfaça a propriedade diamante se: ${\ 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}$

Então, a propriedade Church-Rosser é a declaração que satisfaz a propriedade diamante. Apresentamos uma nova redução cujo fechamento transitivo reflexivo é e que satisfaz a propriedade do diamante. Por indução no número de etapas na redução, segue-se que satisfaz a propriedade do diamante. ${\ displaystyle \ twoheadrightarrow _ {\ beta}}$${\ displaystyle \ rightarrow _ {\ |}}$${\ displaystyle \ twoheadrightarrow _ {\ beta}}$${\ displaystyle \ twoheadrightarrow _ {\ beta}}$

A relação tem as regras de formação: ${\ displaystyle \ rightarrow _ {\ |}}$

• ${\ displaystyle M \ rightarrow _ {\ |} M}$
• Se e então e e ${\ displaystyle M \ rightarrow _ {\ |} M '}$${\ displaystyle N \ rightarrow _ {\ |} N '}$${\ displaystyle \ lambda xM \ rightarrow _ {\ |} \ lambda x.M '}$${\ displaystyle MN \ rightarrow _ {\ |} M'N '}$${\ displaystyle (\ lambda xM) N \ rightarrow _ {\ |} M '[x: = N']}$

A regra da redução η pode ser provada diretamente como Church-Rosser. Então, pode-se provar que a redução β e a redução η comutam no sentido de que:

Se e então existe um termo como e . ${\ 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}$

Portanto, podemos concluir que a redução de βη é Church-Rosser.

Normalização

Uma regra de redução que satisfaça a propriedade de Church-Rosser tem a propriedade de que cada termo M pode ter no máximo uma forma normal distinta, como segue: se X e Y são formas normais de M então pela propriedade de Church-Rosser, ambos se reduzem a um termo igual Z . Ambos os termos já são formas normais assim . ${\ displaystyle Z = X = Y}$

Se uma redução está se normalizando fortemente (não há caminhos de redução infinitos), então uma forma fraca da propriedade Church-Rosser implica na propriedade total. A propriedade fraca, para uma relação , é: ${\ displaystyle \ rightarrow}$

${\ displaystyle \ forall M, N_ {1}, N_ {2} \ in \ Lambda:}$ se e então existe um termo tal que e . ${\ displaystyle M \ rightarrow N_ {1}}$${\ displaystyle M \ rightarrow N_ {2}}$${\ displaystyle X}$${\ displaystyle N_ {1} \ rightarrow X}$${\ displaystyle N_ {2} \ rightarrow X}$

Variantes

O teorema de Church-Rosser também é válido para muitas variantes do cálculo lambda, como o cálculo lambda simplesmente digitado , muitos cálculos com sistemas de tipos avançados e o cálculo do valor beta de Gordon Plotkin . Plotkin também utilizado um teorema de Church-Rosser para provar que a avaliação de programas funcionais (tanto para avaliação lenta e avaliação ansiosa ) é uma função de programas para os valores (um subconjunto dos termos lambda).

Em trabalhos de pesquisa mais antigos, diz-se que um sistema de reescrita é Church-Rosser, ou tem a propriedade Church-Rosser, quando é confluente .

Notas

Referências

• Alama, Jesse (2017). Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy (edição do outono de 2017). Laboratório de Pesquisa Metafísica, Universidade de Stanford.
• Church, Alonzo ; Rosser, J. Barkley (maio de 1936), "Some properties of conversion" (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 (edição revisada), North Holland, Amsterdam, ISBN   0-444-87508-5 , arquivado do original em 23/08/2004 CS1 maint: parâmetro desencorajado ( link ) . Errata .