Base incompleta de combinadores

Isso é inspirado por esta pergunta. Seja a coleção de todos os combinadores que possuem apenas duas variáveis ligadas. é combinatoriamente completo? $\mathcal{C}$ $\mathcal{C}$

Acredito que a resposta é negativa, mas não consegui encontrar uma referência para isso. Eu também estaria interessado em referências para provas de incompletude combinatória de conjuntos de combinadores (posso ver por que o conjunto consiste em combinadores com apenas uma variável vinculada está incompleto, portanto esses conjuntos devem conter mais do que apenas elementos de ). $\mathcal{D}$ $\mathcal{D}$

lo.logic lambda-calculus combinatory-logic tci
fonte

Você poderia esclarecer o que quer dizer com o número de variáveis ligadas de um combinador (= termo lambda fechado)? Número total de abstrações lambda?

Noam Zeilberger

Sim, foi isso que eu quis dizer.

tci 27/07

Na verdade, talvez não seja exatamente isso que você quis dizer ... talvez seja o número total de variáveis distintas usadas nas abstrações lambda, de modo que, por exemplo

possui duas variáveis vinculadas distintas, apesar de ter quatro abstrações lambda? Nesse caso, parece que Rick Statman respondeu exatamente a essa pergunta (negativamente), em " Duas variáveis não são suficientes ".

(λ x . x (λ y . y)) (λ x . λ y . x y)

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

Noam Zeilberger

Direita. Acho que essa é a resposta que eu estava procurando e definitivamente esperava que fosse o resultado de Statman. Ainda não verifiquei, mas acho que isso também daria uma resposta negativa à pergunta que mencionei. Se você postar como resposta, eu aceitaria com prazer.

tci 01/08/16

Respostas:

[Expandindo o comentário em uma resposta.]

$t$

the total number of distinct bound variable names in t

$\text{the total number of distinct bound variable names in }t$

t = (λ x . x (λ y . y)) (λ x . λ y . y x)

$t = (\lambda x.x(\lambda y.y))(\lambda x.\lambda y.yx)$

α

$\alpha$

t

$t$

α

$\alpha$

t^{'} = (λ x . x (λ y . y)) (λ a . λ b . b a)

$t' = (\lambda x.x(\lambda y.y))(\lambda a.\lambda b.ba)$

t^{'}

$t'$

t

$t$

the maximum number of free variables in a subterm of t

$\text{the maximum number of free variables in a subterm of }t$

α

$\alpha$

$\mathcal{C}$

Parece que a prova original disso está contida em um relatório técnico de Rick Statman:

Combinadores hereditariamente da ordem dois. Relatório Técnico 88-33 do Departamento de Matemática Carnegie Mellon, agosto de 1988. ( pdf )

$\beta$

Duas variáveis não são suficientes. Anais da 9ª conferência italiana de Ciência da computação teórica, pp. 406-409, 2005. ( acm )

$Hn$ $Hn$ $n+1$ $\beta$ $n$ $S = \lambda x.\lambda y.\lambda z.(xz)(yz)$ $n$ $n$ $Hn$ $n+1$

Noam Zeilberger
fonte