Эта статья предполагает, что есть комбинаторы (представляющие символические вычисления), которые не могут быть представлены лямбда-исчислением (если я правильно понимаю вещи):
Есть несколько вещей, которые можно захотеть сделать на практике, и которые нельзя прямо выразить в лямбда-исчислении.
Исчисление SF является примером. Его выразительная сила не новость; интересная часть статьи (не показанная на слайдах) - это теория категорий. Исчисление SF аналогично реализации lisp, где вы позволяете функциям проверять представление своих аргументов, поэтому вы можете писать такие вещи, как (print (lambda (x) (+ x 2)))⟹ "(lambda (x) (+ x 2))".
Другой важный пример - параллель Плоткина или . Интуитивно понятно, что есть общий результат, в котором говорится, что лямбда-исчисление является последовательным: функция, которая принимает два аргумента, должна сначала выбрать один, чтобы оценить. Невозможно написать лямбда-термин, orтакой что ( or⊤ ⊥) ⟹ ⊤, ( or⊥ ⊤) ⊤ ⊤ и or⊥ ⊥ ⟹ ⊥ (где ⊥ - не заканчивающийся термин, а ⊤ - завершающий термин). Это известно как «параллельный или», потому что параллельная реализация может делать один шаг каждого сокращения и останавливаться всякий раз, когда один из аргументов завершается.
Еще одна вещь, которую вы не можете сделать в лямбда-исчислении - это ввод / вывод. Вы должны были бы добавить дополнительные примитивы для этого.
Конечно, все эти примеры можно представить в лямбда-исчислении, добавив один уровень косвенности, по существу, представляя лямбда-термины в качестве данных. Но тогда модель становится менее интересной - вы теряете связь между функциями в смоделированном языке и лямбда-абстракциями.
Ответ на ваш вопрос зависит от того, как вы определяете «вычисления» и «представленные». Нить на LTU , что sclv упоминается , с другой стороны, состоит в основном из людей , говорящих мимо друга вследствие Разрегулированных определения различных терминов.
Различие, конечно, не в вычислительной мощи - каждая рассматриваемая система эквивалентна по Тьюрингу. Вопрос в том, что простая эквивалентность по Тьюрингу ничего не говорит о структуре или семантике выражения. В этом отношении, в чрезвычайно минималистской модели вычислений, требующую сложные кодировки или нетривиальные начальные состояния, он может быть даже неясно , будет ли система является способной универсальным вычислением, или иллюзия универсальности создаются чьей - то интерпретация системы , Например, посмотрите это обсуждение списка рассылки, касающееся машины Тьюринга с двумя символами, состоящей из двух состояний, в частности проблем, поднятых Воганом Праттом.
В любом случае, проводится различие между чем-то вроде:
Эквивалентность по Тьюрингу подразумевает только то, что система удовлетворяет третьему критерию для любой вычислимой функции, тогда как чаще всего это первый критерий, который нас интересует, либо в формальной системе логики, либо в языке программирования (в какой-то степени они действительно различаются).
Это очень неформальное описание, но основная идея может быть сформулирована более точно. В вышеупомянутом потоке LtU можно найти пару ссылок на существующие работы в том же духе.
И комбинаторная логика Шенфинкеля, и λ-исчисление Чёрча изначально были разработаны как дистиллированные абстракции логических рассуждений, и, как таковая, их структура очень четко отображает логические рассуждения и наоборот. Они также несут предположение о расширении , такое как описано правилом eta-сокращения: λx. f xгде xне происходит f, эквивалентно только fодному.
На практике очень строгое понятие экстенсиональности может быть слишком ограничивающим, в то время как безудержная интенциональность делает локальные рассуждения о подвыражениях трудными или невозможными.
SF-исчисление - это модифицированное исчисление комбинаторов, которое предоставляет в качестве примитивной операции ограниченную форму интенсионального анализа: возможность деконструировать частично примененные выражения, но не примитивные значения или ненормализованные выражения. Это происходит в соответствии с идеями, такими как сопоставление с образцом, которое можно найти в языках программирования в стиле ML или макросах, как в Лиспсе, но не может быть описано в исчислении SK или λ без эффективной реализации интерпретатора для оценки «интенсиональных» терминов.
Итак, в заключение: SF-исчисление не может быть представлено непосредственно в λ-исчислении в том смысле, что наилучшее возможное представление наиболее вероятно включает в себя реализацию интерпретатора SF-исчисления, и причина этого заключается в фундаментальном семантическом различии: имеют ли выражения внутренние структура, или они определяются исключительно своим внешним поведением?
Исчисление SF Барри Джея может изучить структуру терминов, к которым он применяется, и которые не являются функциональными. Лямбда-исчисление и традиционная комбинаторная логика являются чисто функциональными, и поэтому не могут этого сделать.
Есть много расширений лямбда-исчисления, которые делают вещи, которые нарушают чистоту, большинство из которых требуют некоторой корректировки стратегии перезаписи, например, добавление состояния, элементов управления (например, через продолжения) или логических переменных.
источник