Почему стратегия оценки вызова по значению не полна по Тьюрингу?
Я читаю статью о различных стратегиях оценки (я связал статью в Wiki, но я читаю другой не на английском языке). И это говорит это, в отличие от этого, call-by-name и call-by-need стратегии, call-by-value стратегия не полна по Тьюрингу.
Кто-либо может объяснить, почему это так? Если это возможно, добавьте пример.
2 ответа
Я оспариваю претензию в статье, которую вы читаете. (Мне за это не платят, поэтому я собираюсь привести убедительный аргумент, а не доказательство.)
Хорошо известно, что, по крайней мере, при редукции в нормальном порядке (также известной как вызов по имени), чистое лямбда-исчисление полно по Тьюрингу.Но если мы посмотрим на основополагающую статью Джона Рейнольдса Определительные интерпретаторы для языков программирования высшего порядка , мы увидим, что Рейнольдс подробно обсуждает разницу между вызовом по имени и вызовом по значению. Важнейшая часть аргументации состоит в том, что для того, чтобы правильно различать, мы можем преобразовать программу в стиль передачи продолжения . Преобразование CPS отличается для вызова по необходимости и вызова по значению, но полученные преобразованные термины можно оценивать в любом стиле.
Итак, вот аргумент: напишите программу лямбда-исчисления, которая имитирует машину Тьюринга, затем CPS преобразует ее с помощью преобразования CBN, и вы можете оценить полученный код, используя стратегию сокращения CBV. Хлопнуть! Полный по Тьюрингу.
На практике я уверен, что вы можете написать программу CBV для эмуляции машины Тьюринга; вероятно, достаточно выбрать подходящий комбинатор с фиксированной точкой, например. (Более известный комбинатор Y работает только в рамках стратегии сокращения вызова по имени, т. Е. Сокращения в нормальном порядке.)
Заявление об ограничении ответственности: Я давно не изучал лямбда-исчисление, и я уверен в этом. в приведенном выше аргументе неверно несколько деталей. Но я уверен в сути. Это не первый раз, когда я обнаруживаю что-то явно неправильное в онлайн-ресурсах по теории языков программирования.
Ваш вопрос не имеет большого смысла без ссылки на какой-то конкретный язык, но я постараюсь изо всех сил ответить в отношении нетипизированного лямбда-исчисления.
Существование комбинатора с фиксированной точкой вызова по значению (т. Е. "Y комбинатора") для нетипизированного лямбда-исчисления, кажется, опровергает основное утверждение (см .: Комбинатор с фиксированной точкой ). Существование такого комбинатора нарушает строгую нормализацию, которая предполагает, что существует по крайней мере один язык, полный по Тьюрингу, который использует стратегию оценки по значению.
Гораздо более вероятно, что на полноту по Тьюрингу в языке повлияет наличие (или отсутствие) системы типов. Например, лямбда-исчисление с простой типизацией не может кодировать комбинатор с фиксированной точкой и является строго нормализующим (т.е. все хорошо типизированные термины сводятся к значению), однако это верно независимо от используемой стратегии оценки. Скорее, это следствие системы типов.