Um quine no cálculo lambda puro

Eu gostaria de um exemplo de quine no cálculo lambda puro . Fiquei bastante surpreso por não encontrar um pesquisando no Google. A página quine lista os quines para muitos idiomas "reais", mas não para o cálculo lambda.

Obviamente, isso significa definir o que quero dizer com uma solução no cálculo lambda, o que eu faço abaixo. (Estou pedindo algo bastante específico.)

Em alguns lugares, por exemplo, Larkin e Stocks (2004), vejo o seguinte citado como uma expressão "auto-replicante": $(\lambda x.x \; x)\;(\lambda x.x \; x)$ . Isso se reduz a si próprio após uma única etapa de redução beta, dando a ele uma sensação de quine. No entanto, é incomparável, pois não termina: reduções beta adicionais continuarão produzindo a mesma expressão, portanto nunca se reduzirá à forma normal. Para mim, um quine é um programa que termina e gera saída, e, portanto, eu gostaria de uma expressão lambda com essa propriedade.

Obviamente, qualquer expressão que não contenha redexes já está na forma normal e, portanto, será encerrada e gerada por si mesma. Mas isso é muito trivial. Portanto, proponho a seguinte definição na esperança de que ela admita uma solução não trivial:

definição (provisória): Um quine no cálculo lambda é uma expressão da forma (onde representa alguma expressão específica de cálculo lambda) de forma que torna-se , ou algo equivalente a ele sob alterações de nomes de variáveis, quando reduzidas à forma normal, para qualquer entrada .

Dado que o cálculo lambda é tão equivalente a Turing quanto qualquer outro idioma, parece que isso seria possível, mas meu cálculo lambda está enferrujado, então não consigo pensar em um exemplo.

Referência

James Larkin e Phil Stocks. (2004) "Expressões auto-replicantes no Lambda Calculus" Conferences in Research and Practice in Information Technology, 26 (1), 167-173. http://epublications.bond.edu.au/infotech_pubs/158

Você quer um termo tal que ∀ M ∈ Λ :$Q$$\forall M \in \Lambda$

Não especificarei mais restrições ao (por exemplo, em relação à sua forma e se está normalizando) e mostrarei que ele definitivamente deve estar não normalizado.$Q$

1. Suponha que esteja na forma normal. Escolha M ≡ x (nós podemos fazê-lo porque as necessidades teorema de segurar para todos M ). Depois, há três casos.$Q$$M \equiv x$$M$

   • é algum átomo a . Então Q M ≡ a x . Esta não é redutível a um .$Q$$a$$QM \equiv ax$$a$
   • é alguma aplicação ( R S ) . Em seguida, Q H ≡ ( R S ) x . ( R S ) é uma forma normal por hipótese, então ( R S ) x também está na forma normal e não pode ser reduzida a ( R S ) .$Q$$(RS)$$QM \equiv (RS)x$$(RS)$$(RS)x$$(RS)$
   • é alguma abstração ( λ x . A ) (se x deve estar livre em A , então, por simplicidade, podemos simplesmente escolher M equivalente a qualquer variável que λ abstraia acima). Em seguida, Q H ≡ ( λ x . A ) x ⊳ p Um [ x / x ] ≡ Uma . Como ( λ x . A ) está na forma normal, o mesmo ocorre com$Q$$(\lambda x.A)$$x$$A$$M$$\lambda$$QM \equiv (\lambda x.A)x \rhd_\beta A[x/x] \equiv A$$(\lambda x.A)$$A$. Consequentemente, não podemos reduzir para ( λ x . A ) .$A$$(\lambda x.A)$

   Portanto, se esse existe, ele não pode estar na forma normal.$Q$

2. Para completar, suponhamos que tem uma forma normal, mas não é em forma normal (talvez seja normalizadora fracamente), ou seja, ∃ N ∈ p -nf com N ≢ Q de tal modo que ∀ M ∈ Ganhe muitos : Q H ⊳ p Q ⊳ p$Q$ $\exists N \in \beta\text{-nf}$$N \not\equiv Q$$\forall M \in \Lambda$

   $$QM \rhd_\beta Q \rhd_\beta N$$

   Em seguida, com deve haver também existir uma sequência de redução Q x ⊳ p N x ⊳ p N , porque:$M \equiv x$$Qx \rhd_\beta Nx \rhd_\beta N$

   • é possível pelo facto de Q ⊳ p N .$Qx \rhd_\beta Nx$$Q \rhd_\beta N$
   • deve normalizar, pois N é um β- nf e x é apenas um átomo.$Nx$$N$$\beta$$x$
   • Se foram para normalizar a qualquer coisa que não seja N , então Q x tem dois β -nfs, que não é possível por um corolário do teorema de Church-Rosser. (O teorema de Church-Rosser afirma essencialmente que as reduções são confluentes, como você provavelmente já sabe.)$Nx$$N$$Qx$$\beta$

   Mas observe que não é possível pelo argumento (1) acima; portanto, nossa suposição de que Q tem uma forma normal não é sustentável.$Nx \rhd_\beta N$$Q$

3. Se permitirmos um , então, temos certeza de que ele não deve ser normalizado. Nesse caso, podemos simplesmente usar um combinador que elimina qualquer argumento que recebe. A sugestão de Denis funciona bem: Q ≡ ( λ z . ( Λ x . Λ z . ( X x ) ) ( λ x . Λ z . ( X x ) ) ) Então, em apenas duas reduções β : Q $Q$

   $$Q \equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x)))$$ $\beta$ $$\begin{align} QM &\equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x))) M \\ & \rhd_{1\beta} (λx.λz.(x x)) (λx.λz.(x x)) \\ & \rhd_{1\beta} (λz.((λx.λz.(x x))(λx.λz.(x x))) \\ & \equiv Q \end{align}$$

Esse resultado não é muito surpreendente, uma vez que você está pedindo um termo que elimine qualquer argumento que receba, e isso é algo que muitas vezes vejo mencionado como uma aplicação direta do teorema do ponto fixo.

Por um lado, isso é impossível, porque um quine deve produzir seu próprio código, e o cálculo lambda puro não tem meios para executar a saída.

Por outro lado, se você assumir que o termo resultante é o resultado, todas as formas normais são válidas.

$(\lambda x. x)$$(\lambda x. x)$$(\lambda x. x)$

Aqui está uma proposição:

$A$$f=\lambda t. (\lambda z.t)$

$Y=\lambda g.((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))$$A=Y f=(\lambda x.\lambda z.(x\ x))\ (\lambda x.\lambda z.(x\ x))$

$A$$A$$\lambda z.A$$y$$(\lambda z.A)y \to_\beta A \to_\beta (\lambda z.A)$