Почему лямбда-исчисление не может представлять некоторые комбинаторы?

18

Эта статья предполагает, что есть комбинаторы (представляющие символические вычисления), которые не могут быть представлены лямбда-исчислением (если я правильно понимаю вещи):

Hawkeye
источник

Ответы:

20

Есть несколько вещей, которые можно захотеть сделать на практике, и которые нельзя прямо выразить в лямбда-исчислении.

Исчисление SF является примером. Его выразительная сила не новость; интересная часть статьи (не показанная на слайдах) - это теория категорий. Исчисление SF аналогично реализации lisp, где вы позволяете функциям проверять представление своих аргументов, поэтому вы можете писать такие вещи, как (print (lambda (x) (+ x 2)))"(lambda (x) (+ x 2))".

Другой важный пример - параллель Плоткина или . Интуитивно понятно, что есть общий результат, в котором говорится, что лямбда-исчисление является последовательным: функция, которая принимает два аргумента, должна сначала выбрать один, чтобы оценить. Невозможно написать лямбда-термин, orтакой что ( or⊤ ⊥) ⟹ , ( or⊥ ⊤) ⊤ ⊤ и or⊥ ⊥ ⟹ ⊥ (где ⊥ - не заканчивающийся термин, а ⊤ - завершающий термин). Это известно как «параллельный или», потому что параллельная реализация может делать один шаг каждого сокращения и останавливаться всякий раз, когда один из аргументов завершается.

Еще одна вещь, которую вы не можете сделать в лямбда-исчислении - это ввод / вывод. Вы должны были бы добавить дополнительные примитивы для этого.

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

Жиль "ТАК - перестань быть злым"
источник
11

Ответ на ваш вопрос зависит от того, как вы определяете «вычисления» и «представленные». Нить на LTU , что sclv упоминается , с другой стороны, состоит в основном из людей , говорящих мимо друга вследствие Разрегулированных определения различных терминов.

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

В любом случае, проводится различие между чем-то вроде:

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

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

Это очень неформальное описание, но основная идея может быть сформулирована более точно. В вышеупомянутом потоке LtU можно найти пару ссылок на существующие работы в том же духе.


И комбинаторная логика Шенфинкеля, и λ-исчисление Чёрча изначально были разработаны как дистиллированные абстракции логических рассуждений, и, как таковая, их структура очень четко отображает логические рассуждения и наоборот. Они также несут предположение о расширении , такое как описано правилом eta-сокращения: λx. f xгде xне происходит f, эквивалентно только fодному.

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

SF-исчисление - это модифицированное исчисление комбинаторов, которое предоставляет в качестве примитивной операции ограниченную форму интенсионального анализа: возможность деконструировать частично примененные выражения, но не примитивные значения или ненормализованные выражения. Это происходит в соответствии с идеями, такими как сопоставление с образцом, которое можно найти в языках программирования в стиле ML или макросах, как в Лиспсе, но не может быть описано в исчислении SK или λ без эффективной реализации интерпретатора для оценки «интенсиональных» терминов.

Итак, в заключение: SF-исчисление не может быть представлено непосредственно в λ-исчислении в том смысле, что наилучшее возможное представление наиболее вероятно включает в себя реализацию интерпретатора SF-исчисления, и причина этого заключается в фундаментальном семантическом различии: имеют ли выражения внутренние структура, или они определяются исключительно своим внешним поведением?

CA Макканн
источник
Что вы имеете в виду, что существуют разные взгляды на представление вычислений на машине Тьюринга?
Соколиный глаз
5

Исчисление SF Барри Джея может изучить структуру терминов, к которым он применяется, и которые не являются функциональными. Лямбда-исчисление и традиционная комбинаторная логика являются чисто функциональными, и поэтому не могут этого сделать.

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

Чарльз Стюарт
источник
2
См. Также расширенную дискуссию / дебаты в Lambda the Ultimate: lambda-the-ultimate.org/node/3993
sclv