Qual é o objetivo da conversão no cálculo lambda?

18

Eu acho que não estou entendendo isso, mas -conversion me parece uma conversão que não faz nada, um caso especial de -conversion em que o resultado é apenas o termo na abstração lambda porque não há nada para fazer, uma espécie de conversão inútil .β β βηβββ

Portanto, talvez -conversion seja algo realmente profundo e diferente disso, mas, se for, eu não entendo e espero que você possa me ajudar.η

(Obrigado e desculpe, eu sei que isso faz parte dos princípios básicos do cálculo lambda)

Trylks
fonte

Respostas:

20

Atualização [20/09/2011]: ampliei o parágrafo sobre -expansion e extensionality. Agradecemos a Anton Salikhmetov por apontar uma boa referência.η

η -conversion é um caso especial de - conversão apenas no caso especial quando é uma abstração, por exemplo, se entãoMas e se for uma variável ou um aplicativo que não se reduz a uma abstração?(λx.fx)=fβff=λy.yy

(λx.fx)=(λx.(λy.yy)x)=β(λx.xx)=αf.
f

De certa forma, -rule é como um tipo especial de extensionalidade, mas precisamos ter um pouco de cuidado sobre como isso é afirmado. Podemos afirmar a extensionalidade como:η

  1. para todos -Termos e , se então , ouM N M x = N x M = NλMNMx=NxM=N
  2. para todos os se então .x . f x = g x f = gf,gx.fx=gxf=g

O primeiro é uma meta-declaração sobre os termos do -calculus. Nele aparece como uma variável formal, isto é, faz parte do -calculus. Isso pode ser provado a partir de -rules, veja, por exemplo, o Teorema 2.1.29 em "Lambda Calculus: its Syntax and Semantics" de Barendregt (1985). Pode ser entendido como uma declaração sobre todas as funções definíveis , isto é, aquelas que são denotações de -terms.x λ β η λλxλβηλ

A segunda afirmação é como os matemáticos geralmente entendem afirmações matemáticas. A teoria do -calculus descreve um certo tipo de estruturas, vamos chamá-los de " -models ". Um -model pode ser incontável, portanto não há garantia de que cada elemento corresponda a um -term (assim como existem mais números reais do que expressões que descrevem reais). Extensionalidade então diz: se tomarmos quaisquer duas coisas e em um -model, se para todo no modelo, então . Agora, mesmo que o modelo satisfaça aλ λ λ f g λ f x = g x x f = g ηλλλλfgλfx=gxxf=gη regra, ele não precisa satisfazer a extensionalidade nesse sentido. (Referência necessária aqui, e acho que precisamos ter cuidado com a interpretação da igualdade.)

Existem várias maneiras pelas quais podemos motivar conversões - e . Escolherei aleatoriamente a teoria da categoria, disfarçada como -calculus, e alguém mais pode explicar outras razões.η λβηλ

Vamos considerar o -calculus digitado (porque é menos confuso, mas mais ou menos o mesmo raciocínio funciona para o -calculus não digitado). Uma das leis básicas que deve ser mantida é a lei exponencial(Estou usando as notações e intercambiável, escolhendo o que parecer melhor.) O que os isomorfismos e parecem escritos em -calculus? Presumivelmente, eles seriam eX C Uma × B( C B ) Uma . Um B B A i : C Uma × B( C B ) Um j : ( C B ) UmC Uma × B λ i = λ f : C A x B . λ um : A . λ b :λλ

CUMA×B(CB)UMA.
UMABBUMAEu:CUMA×B(CB)UMAj:(CB)UMACUMA×BλJ = λ g : ( C B ) Uma . λ p : Um × B . g ( π 1 p ) ( π 2 p ) . p p π 1um , b = um π 2um , b = b g : (
Eu=λf:CUMA×B.λuma:UMA.λb:B.fuma,b
j=λg:(CB)A.λp:A×B.g(π1p)(π2p).
Um breve cálculo com um par de -reductions (incluindo o -reductions e para produtos) nos que, diz para cada temos Como e são inversos um do outro, esperamos que , mas para provar isso de fato, precisamos usar reduction duas vezes:ββπ1a,b=aπ2a,b=b i ( j g ) = λ um : Uma . λ b : B . g a b . i j i ( j g ) = g η i ( j g ) = ( λ um : Um . λ b : B . g um b ) = η ( λ um :g:(CB)A
i(jg)=λa:A.λb:B.gab.
iji(jg)=gη
i(jg)=(λa:A.λb:B.gab)=η(λa:A.ga)=ηg.
Portanto, esse é um motivo para ter reduções. Exercício: que é necessário -rule para mostrar que ?η j ( i f ) = fηηj(if)=f
Andrej Bauer
fonte
"Além disso, ouvi dizer que a regra η trata da extensionalidade de funções. Isso é falso" Se você aumentar os axiomas de igualdade de e as regras de inferência com a regra de extensionalidade (veja minha resposta), esse conjunto de regras de inferência captura exatamente igualdade, não é? (ou seja, dois termos são iguais nesta teoria sse eles são -equal)β η β ηββηβη
Marcin Kotowski
@ Marcin: sim, a extensionalidade implica regra, mas não vice-versa. Como você extrairia a extensionalidade de - e -rules? β ηηβη
Andrej Bauer
1
let denota a menor congruência que contém e satisfaz a extensionalidade (se , então ). Então se (veja, por exemplo, o primeiro capítulo de Urzyczyn, Sorensen "Palestra sobre isomorfismo de Curry-Howard) e, nesse sentido, capitula captura a noção de extensionalidade.= β M x = N x M = N M = N M = β η N η==βMx=NxM=NM=NM=βηNη
Marcin Kotowski
Eu vejo, você está pensando de extensionalidade como um esquema, ou seja, provamos que detém para cada par particular de termos e . Eu estava pensando na extensionalidade como uma afirmação. Eu acho que. Agora eu tenho que pensar sobre isso. NMN
Andrej Bauer
1
@AndrejBauer Concordo que a regra-η não é extensionalidade total, mas você não acha que ainda é uma forma limitada de extensionalidade, ou seja, representa uma classe de casos óbvios de extensionalidade. A pergunta original está em busca de motivações e conceitos e, neste caso, acredito que o pensamento em termos de extensionalidade é útil (com alguns cuidados, é claro, para não ir longe demais).
Marc Hamann 20/09
9

Para responder a essa pergunta, podemos fornecer a seguinte citação da monografia correspondente “Cálculo Lambda. Sua sintaxe e semântica “(Barendregt, 1981):

O objetivo da introdução de reduction é fornecer um axioma para declarações prováveis ​​na extensão -calculus [a teoria , em que representa a regra ], de tal forma que teria propriedades Church-Rosser.λ λ + ext ext M x = N x M = Nβηλλ+extextMx=NxM=N

Proposição. .M=βηNληM=Nλ+extM=N

[Sua prova é baseada no seguinte teorema.]

Teorema (de Curry). As teorias e são equivalentes… [Sua prova consiste em duas partes: e vice-versa.]λ η ( ext ) ( η )λ+extλη(ext)(η)

Uma das razões para considerar o sistema é que ele possui uma certa propriedade de completude ... [Nomeadamente, no sentido do seguinte teorema.]λη

Teorema. Permita que e tenham uma forma normal. Então, ou é inconsistente…N λ η M = N λ η + M = NMNληM=Nλη+M=N

As teorias HP-complete [depois de Hilbert-Post] correspondem a teorias consistentes máximas na teoria dos modelos para a lógica de primeira ordem.


fonte
7

Apenas para acrescentar à muito boa resposta de Andrej: a teoria das regras de redução sem tipo -calculus com e satisfaz algumas propriedades muito boas:β ηλβη

  • É consistente no sentido de que existem dois termos, por exemplo, e que não são equivalentes. Isso é uma conseqüência do teorema da confluência para a redução .λ x y . y β η β ηλxy.xλxy.y βηβη

  • É uma teoria consistente máxima , no seguinte sentido: se é uma relação de equivalência em termos tais que:ι

    1. É fechado por congruência: etc.u =ι vt u =ι t v

    2. É equivale 2 não equivalente termosβη que são formas normais : não existe e na forma normal de tal modo que e .tut=ιutβηu

Então a teoria é inconsistente : para cada termo , na forma normal, .tut=βηιu

Isso é uma consequência do teorema de Böhm.

cody
fonte
6

η

=βηβηM=Nλx.M=λx.N=β

=β=βηλx.Mx=MMx=NxM=N

Marcin Kotowski
fonte
η
Veja o Teorema 2.1.29 na monografia de Barendregt (Lambda Calculus e sua Semântica, 1985).
2
ξ
E, por sua vez, não estou muito feliz com o fato de a felicidade e as respostas "ouvidas sobre" ganharem mais atenção do que citações diretas relevantes com as referências correspondentes.
ξξαβ