Par de bases combinador completo mais simples para expressões planas

No artigo de Chris Okasaki, " Achatando Combinadores: Sobrevivendo Sem Parênteses ", ele mostra que dois combinadores são suficientes e necessários como base para codificar expressões completas de Turing sem a necessidade de um operador de aplicativo ou parênteses.

Comparado às codificações de John combinatória da lógica combinatória em " Cálculo lambda binário e lógica combinatória " por meio do prefixo que codifica combinadores S e K com um operador de aplicativo, a necessidade de apenas dois combinadores para expressões planas aumenta a densidade do código para otimizar. A numeração Goedel resultante mapeia todos os números inteiros para uma expressão válida a termo fechado, bem diferente da maioria dos esolangs relevantes de comprimento de cálculo e descrição mínima, cujas representações canônicas geralmente permitem descrições de programas sintaticamente inválidos.

No entanto, a codificação de Okasaki foi projetada para ser mais útil no mapeamento unidirecional dos termos do cálculo lambda para as cadeias de bits, não necessariamente o contrário, pois os dois combinadores usados ​​nessa redução são relativamente complexos quando usados ​​como instruções práticas de substituição.

Qual é o par básico mais simples do combinador que não requer um operador de aplicativo?

Voltando a isso quase um ano depois, percebi que havia perdido algumas pesquisas críticas antes de postar.

Jot parece se encaixar no que eu estava pedindo, com dois combinadores relativamente simples B & X que podem ser representados por uma numeração compacta de Goedel.

Simplifiquei sua implementação de referência com o Python:

def S(x): return lambda y: lambda z: x(z)(y(z))
def K(x): return lambda y: x
def X(x): return x(S)(K)
def B(x): return lambda y: lambda z: x(y(z))
def I(x): return x
def J(n): return (B if n & 1 else X)(J(n >> 1)) if n else I

J (n) retorna a função acumulada que denota o programa representado pelo seu número Goedel n.

B (equivalente à multiplicação codificada pela Igreja) serve para a função de aplicação funcional (parênteses) e pode isolar as metades S / K do combinador Iota de base única X.

Existem algumas propriedades importantes dessa linguagem que eu estou (quase) descaradamente roubando do site do inventor da língua, Chris Barker, por volta de 2000.

Jot é uma linguagem regular na sintaxe, mas completa em Turing. Você pode ver na implementação de J (n) que, se um idioma host suportar recursão de cauda, ​​não haverá espaço na pilha necessário para analisar o formato do programa da cadeia de bits.

A prova da integridade de Turing também vem do site de Chris, implementando a lógica combinatória já conhecida de Turing usando os combinadores S e K:

K  ==> 11100
S  ==> 11111000
AB ==> 1[A][B], where A & B are arbitrary CL combinators built up from K & S

O Jot não possui erros de sintaxe, todos os programas com o seu número Goedel n são válidos. Esse é provavelmente o aspecto mais importante da minha própria pesquisa, pois não apenas simplifica a análise da trivialidade, mas também deve, em teoria, tornar o Jot muito mais parcimonioso do que qualquer codificação completa de Turing que precise ignorar programas malformados.

Escrevi algumas ferramentas para 'resolver' via força bruta o problema semi-decidível de encontrar a complexidade de Kolmogorov de uma função no Jot. Ele funciona contando com o programador para especificar alguns exemplos de treinamento muito característicos do mapeamento de uma função, depois enumera todos os programas Jot até que todos os exemplos de treinamento sejam correspondidos e, finalmente, tenta uma prova de igualdade de uma função encontrada com a implementação detalhada original.

Atualmente, ele só funciona para até 40 bits com meus recursos limitados. Estou tentando reescrever com um solucionador SAT para aprender programas muito maiores. Se você sabe como desenrolar fechamentos aninhados limitados como uma fórmula booleana, ajude com minha nova pergunta .

Agora, vamos fazer algumas comparações interessantes com o Binary Lambda Calculus de John Tromp, conhecido por sua concisão, mas tem o problema de possíveis erros de sintaxe. Os seguintes programas foram gerados pelo meu programa de aprendizado em alguns segundos.

Function    Jot       Binary Lambda Calculus   |J| |B|
--------|----------|--------------------------|---|---
SUCC      J(18400)  "000000011100101111011010" 15  24
CHURCH_0  J(154)    "000010"                    8   6
CHURCH_1  J(0)      "00000111010"               1  11
CHURCH_2  J(588826) "0000011100111010"         20  16
IS_ZERO   J(5)      "00010110000000100000110"   3  23
MUL       J(280)    "0000000111100111010"       9  19
EXP       J(18108)  "00000110110"              15  11
S         J(8)      "00000001011110100111010"   4  23
K         J(4)      "0000110"                   3   7
AND       J(16)     "0000010111010000010"       5  19
OR        J(9050)   "00000101110000011010"     14  20

A partir de minhas próprias experiências, a hipótese de que o Jot leva a programas menores está sendo lentamente confirmada, à medida que meu programa aprende funções simples, as compõe e depois aprende funções maiores com um teto aprimorado.