Какие функции могут вычислять выражения исчисления комбинатора?

Выражение комбинатора (скажем, в основе SK) можно рассматривать как функцию, которая отображает выражения исчисления комбинатора в выражения исчисления комбинатора. То есть выражение как функцию , где - множество всех синтаксически допустимых выражений комбинатора в базисе SK. Это отображение выполняется путем применения ввода к выражению, а затем приведение к нормальной форме, чтобы получить вывод. $X$ $X:L \to L$ $L$

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

Поэтому вместо этого я мог думать о выражениях исчисления SK как о преобразовании $L'$ в $L'$ , где $L'$ - это набор выражений SK в нормальной форме. Это тот случай, когда для любой вычислимой карты $f:L'\to L'$ существует SK-выражение $X$ которое реализует эту карту? Или есть дополнительные ограничения на набор функций, которые могут быть вычислены с помощью выражений комбинаторного исчисления таким образом?

lambda-calculus combinatory-logic Натаниель
источник

Ответы:

Чтобы заставить мяч двигаться вперед, и в надежде на то, что другие люди дадут более глубокие и подробные ответы о структуре определяемых функций , позвольте мне привести следствие 20.3.3 из Барендрегса « Лямбда-исчисление, его Синтаксис и семантика (он же «Библия»). $\lambda$ $L'\to L'$

Следствие 20.3.3. Функция , определяемая как не определим в нетипизированном -calculus, т. Е. Нет термина такого как для всех . $\delta:L'^2\to L'$
$δ (M, N) знак равно {\begin{cases} T р U е если M {знак равно}_{β η} N \\ F a L s е в противном случае \end{cases}$ $\delta(M, N) = \cases{\mathrm{True}\mbox{ if }M=_{\beta\eta}N\\ \mathrm{False}\mbox{ otherwise}}$ $\lambda$ $D$ $D M N {знак равно}_{β η} δ (M, N)$ $D\ M\ N =_{\beta\eta} \delta(M,N)$ $M,N\in L'$

Доказательство включает соображения о деревьях Бёма, которые дают довольно сильную характеристику возможных «действий» произвольных лямбда-членов на нормальных формах. В частности, для любого непостоянного замкнутого члена можно найти и такие, что $F$ $n\in\mathbb{N}$ $P_1,\ldots,P_n$

F Икс п_{1} ... п_{N} {знак равно}_{β η} Икс Q_{1} ... Q_{К}

$F\ x\ P_1\ldots P_n =_{\beta\eta} x\ Q_1\ldots Q_k$

Для некоторых , . Это резко ограничивает возможные формы гипотетического который реализует , показывая с небольшой работой, что такой не может существовать. $k$ $Q_1,\ldots,Q_k$ $D$ $\delta$ $D$

Коди
источник