Простейшая полная пара базисов комбинаторов для плоских выражений

В работе Криса Окасаки « Сглаживание комбинаторов: выживание без скобок » он показывает, что двух комбинаторов достаточно и необходимо в качестве основы для кодирования выражений по Тьюрингу без необходимости использования оператора приложения или скобок.

По сравнению с кодировками комбинаторной логики Джона Трампа в « Бинарном лямбда-исчислении и комбинаторной логике » с помощью префиксного кодирования S и K-комбинаторов с оператором приложения, при использовании только двух комбинаторов для плоских выражений плотность кода возрастает до оптимальной. Результирующая нумерация Гёделя отображает каждое целое число в правильное, правильно сформированное закрытое выражение в отличие от большинства исчислений и релевантных эзолангов с минимальной длиной описания, чьи канонические представления обычно допускают описания синтаксически неверных программ.

Однако кодирование Окасаки должно было быть наиболее полезным в одностороннем отображении терминов лямбда-исчисления в цепочки битов, а не обязательно наоборот, так как два комбинатора, использованные в этом сокращении, являются относительно сложными, когда используются в качестве практических инструкций замещения.

Что такое простейшая полная пара базисов комбинаторов, для которой не требуется оператор приложения?

Возвращаясь к этому почти год спустя, я понял, что пропустил какое-то критическое исследование перед публикацией.

Jot, кажется, соответствует требованиям того, о чем я просил, с двумя относительно простыми комбинаторами B & X, которые могут быть представлены компактной нумерацией Гёделя.

Я упростил его эталонную реализацию с помощью 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) возвращает встроенную функцию, обозначающую программу, представленную ее числом Геделя n.

B (эквивалентно умноженному по Церковью умножению) выполняет функцию функционального приложения (круглые скобки) и может изолировать половины S / K одноосновного комбинатора Iota X.

Есть несколько важных свойств этого языка, которые я (почти) бесстыдно краду с сайта изобретателя языка Криса Баркера, около 2000 года.

Jot - это обычный язык в синтаксисе, но полный по Тьюрингу. Из реализации J (n) видно, что если хост-язык поддерживает хвостовую рекурсию, то для анализа формата программы цепочки битов не требуется стекового пространства.

Доказательство полноты по Тьюрингу также можно найти на сайте Криса, реализующего уже известную комбинаторную логику по Тьюрингу с использованием комбинаторов S и K:

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

Jot не имеет синтаксических ошибок, каждая программа, имеющая номер Геделя n, является допустимой программой. Это, пожалуй, самый важный аспект моего собственного исследования, поскольку он не только упрощает разбор до тривиальности, но и теоретически должен сделать Jot гораздо более экономным, чем любая кодировка, полная по Тьюрингу, которая должна пропускать искаженные программы.

Я написал несколько инструментов, чтобы «решить» с помощью грубой силы полурешаемую проблему нахождения колмогоровской сложности функции в Jot. Он работает, полагаясь на программиста, который задает некоторые очень характерные обучающие примеры отображения функции, затем перечисляет все программы Jot до тех пор, пока не будут сопоставлены все обучающие примеры, и, наконец, пытается доказать равенство найденной функции с исходной подробной реализацией.

В настоящее время он работает только до ~ 40 бит с моими ограниченными ресурсами. Я пытаюсь переписать с помощью SAT Solver, чтобы изучить гораздо большие программы. Если вы знаете, как развернуть вложенные замыкания в виде логической формулы, пожалуйста, помогите с моим новым вопросом .

Теперь для некоторых интересных сравнений с двоичным лямбда-исчислением Джона Тромпа, который известен своей краткостью, но имеет проблему возможных синтаксических ошибок. Следующие программы были сгенерированы моей программой обучения за несколько секунд.

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

Исходя из моих собственных экспериментов, гипотеза о том, что Jot приводит к меньшим программам, постепенно подтверждается, поскольку моя программа изучает простые функции, составляет их, а затем изучает большие функции из улучшенного потолка.