Теория реализуемости: разница в мощности между лямбда-исчислением и машинами Тьюринга

48

У меня есть три связанных подвопроса, которые выделены пунктами ниже (нет, их нельзя разделить, если вам интересно). Андрей Бауэр писал здесь , что некоторые функции реализуются через машину Тьюринга, но не через лямбда-исчисление. Ключевой шаг его рассуждений:

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

  • Я хотел бы видеть объяснение / неофициальное доказательство.

Я не вижу, как применить теорему Райса здесь; это применимо к проблеме «эта машина Тьюринга T и этот лямбда-член L эквивалентны?», потому что применение этого предиката к эквивалентным терминам дает один и тот же результат. Однако требуемая функция может вычислять разные, но эквивалентные ТМ для разных, но эквивалентных лямбда-терминов.

  • Более того, если проблема заключается в самоанализе лямбда-члена, я думаю, что передача кодировки Лямбды-члена Гёделя также была бы приемлемой, не так ли?

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

  • Но поскольку здесь лямбда-исчисление не может решить проблему, связанную с машиной Тьюринга, мне интересно, можно ли определить аналогичную проблему для лямбда-исчисления и доказать, что она не разрешима для машин Тьюринга, или на самом деле существует разница в мощности в пользу Машины Тьюринга (что бы меня удивило).
Blaisorblade
источник

Ответы:

56

У Джона Лонгли есть очень обширная обзорная статья, в которой обсуждаются связанные с этим вопросы «Понятия вычислимости в старших типах» .

NN(NN)N

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

NNn

Стоит отметить, что для более высоких типов, если язык менее выразителен в одном порядке, он более выразителен на один порядок вверх, потому что функции контравариантны. Точно так же есть функции, которые вы можете написать в LC, что вы не можете с кодировкой в ​​стиле ТМ (потому что они основаны на том факте, что вы можете передавать функциональные аргументы и знать, что получатель не может заглянуть внутрь функции, которую вы ему даете) ,

РЕДАКТИРОВАТЬ: Вот пример функции, определяемой в PCF, но не в кодировках TM + Goedel. Я объявлю isAlwaysTrueфункцию

 isAlwaysTrue : ((unit → bool) → bool) → bool

который должен возвращать true, если его аргумент игнорирует свой аргумент и всегда возвращает true, должен возвращать false, если его аргумент возвращает false на любых входах, и входит в цикл, если его аргумент входит в цикл на любых входах. Мы можем довольно легко определить эту функцию следующим образом:

isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)

где вычисление цикла, а также оператор and для логических значений. Это работает, потому что unit → boolв PCF всего три жителя , и поэтому мы можем их полностью перечислить. Однако в модели стилей кодирования ТМ + Геделя pможно было бы проверить, сколько времени потребуется его аргументу, чтобы вернуть ответ, и на основании этого вернуть разные ответы. Таким образом, реализация isAlwaysTrueс ТМ не будет соответствовать спецификации.

Нил Кришнасвами
источник
1
это отличный опрос. спасибо за ссылку!
Суреш Венкат
Я только что понял, что забыл принять ответ, хотя я хотел принять ваш. Сожалею!
Blaisorblade
«Разница в кодировке означает, что вы можете анализировать синтаксис аргумента с помощью кодировки в стиле ТМ, а вы не можете с помощью стандартного представления лямбда-исчисления». Но есть ли у вас представления для композиции функций? Кроме того, то, что вы говорите, предполагает, что HOL - это больше, чем теория типизированного лямбда-исчисления, это нечто большее?
Hibou57
Кроме того, что по этому поводу: cs.virginia.edu/~evans/cs150/classes/class39/lecture39.pdf . Это неправильно в некотором смысле?
Hibou57
Уважаемый Нил, у вас есть пример для функции, которая может быть реализована в модели лямбда-исчисления, но не в модели Тьюринга?
Инго Блехшмидт,
29

Что сказал Нил, а также следующее.

NNλλλ

λNN


λNNλ

NNλappn¯f:NNf(k)appn¯k¯n¯nappλ

Xf:X×NNλtf~:X(NN)λsXNNλff~NNλλNNλ

XNNλXX

Андрей Бауэр
источник
2
все еще жду этого лучшего примера ...
Жак Каретт
1
λ
Я не понимаю, как карри может стать неоспоримым. Вы должны быть в состоянии повторно использовать теорему smn, поскольку ее доказательство создает функцию для данных первого порядка (натуральных чисел). Согласно тезису Черча-Тьюринга, это поведение в натуральном выражении может быть реализовано как лямбда-термин (который использует нативные функции внутри, но я не вижу, как это запрещено). Аналогичным образом можно доказать теорему utm, поэтому по вашему посту мы должны быть готовы. Чего мне не хватает?
Blaisorblade
1
В ответе я объяснил, что означает, что карри становится неисчислимым, а именно то, что предлагаемый объект не является экспоненциальным в категории представляемых множеств.
Андрей Бауэр
Спасибо за объяснение! К сожалению, я не могу снова проголосовать. Я могу следить за большинством технических деталей; Я не знаком с топологическими моделями, но я все равно знаком с «вы не можете проверять функции в функциональном программировании / λ-исчислении». Ваш последний абзац также объясняет, почему я не могу пройти через smn, потому что приведенное smn карринг снова генерирует коды Гёделя, а не стандартные функции, как вам требуется. Я буду медитировать над этим пунктом.
Blaisorblade