El par de bases de combinador completo más simple para expresiones planas

En el artículo de Chris Okasaki " Combinadores de aplanamiento: sobrevivir sin paréntesis ", muestra que dos combinadores son suficientes y necesarios como base para codificar expresiones completas de Turing sin la necesidad de un operador de aplicación o paréntesis.

En comparación con las codificaciones de John Trump de la lógica combinatoria en " Binary Lambda Calculus and Combinatory Logic " a través de la codificación de prefijos de los combinadores S y K con un operador de aplicación, solo se necesitan dos combinadores para expresiones planas que aumenten la densidad del código hasta la óptima. La numeración de Goedel resultante asigna cada número entero a una expresión de término cerrado válida y bien formada, a diferencia de la mayoría de los cálculos y la longitud mínima de descripción relevante, esolangs cuyas representaciones canónicas generalmente permiten descripciones de programas sintácticamente inválidos.

Sin embargo, la codificación de Okasaki estaba destinada a ser más útil en un mapeo unidireccional de términos de cálculo lambda a cadenas de bits, no necesariamente al revés, ya que los dos combinadores utilizados en esta reducción son relativamente complejos cuando se usan como instrucciones prácticas de sustitución.

¿Cuál es el par de bases de combinador completo más simple que no requiere un operador de aplicación?

Volviendo a esto casi un año después, me di cuenta de que me había perdido algunas investigaciones críticas antes de publicar.

Jot parece encajar en la factura de lo que estaba pidiendo, con dos combinadores relativamente simples B y X que pueden representarse mediante una numeración compacta de Goedel.

He simplificado su implementación de referencia con 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) devuelve la función desarrollada que denota el programa representado por su número de Goedel n.

B (equivalente a la multiplicación codificada de Church) cumple la función de aplicación funcional (paréntesis) y puede aislar las mitades S / K del combinador de Iota X de base única.

Hay algunas propiedades importantes de este lenguaje que estoy (casi) descaradamente robando del sitio web del inventor del lenguaje Chris Barker, alrededor del año 2000.

Jot es un lenguaje regular en sintaxis pero completo de Turing. Puede ver en la implementación de J (n) que si un lenguaje host admite la recursión de cola, no se requiere espacio de pila para analizar el formato del programa de cadena de bits.

La prueba de la integridad de Turing proviene también del sitio de Chris, que implementa la lógica combinatoria de Turing ya conocida utilizando los combinadores S y K:

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

Jot no tiene errores de sintaxis, cada programa dado su número de Goedel n es un programa válido. Este es probablemente el aspecto más importante de mi propia investigación, ya que no solo simplifica el análisis de la trivialidad, sino que, en teoría, también debería hacer que Jot sea mucho más parsimonioso que cualquier codificación completa de Turing que tenga que omitir los programas mal formados.

He escrito algunas herramientas para 'resolver' mediante fuerza bruta el problema semi-decidible de encontrar la complejidad de Kolmogorov de una función en Jot. Funciona confiando en que el programador especifique algunos ejemplos de entrenamiento muy característicos del mapeo de una función, luego enumera todos los programas Jot hasta que todos los ejemplos de entrenamiento coincidan, y finalmente intenta una prueba de igualdad de una función encontrada con la implementación detallada original.

Actualmente solo funciona hasta ~ 40 bits con mis recursos limitados. Estoy intentando reescribir con un solucionador SAT para aprender programas mucho más grandes. Si sabe cómo desenrollar cierres anidados acotados como una fórmula booleana, ayúdeme con mi nueva pregunta .

Ahora para algunas comparaciones interesantes con el cálculo binario de Lambda de John Tromp, que es conocido por su concisión, pero tiene el problema de posibles errores de sintaxis. Los siguientes programas fueron generados por mi programa de aprendizaje en unos 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 mis propios experimentos, la hipótesis de que Jot conduce a programas más pequeños se confirma lentamente a medida que mi programa aprende funciones simples, las compone y luego aprende funciones más grandes desde un techo mejorado.