Почему стратегия оценки по стоимости не является полной по Тьюрингу?

Question

Я читаю статью о различных стратегиях оценки (я связал статью в вики, но я читаю другую, не на английском). И это говорит о том, что в отличие от стратегий call-by-name и call-by-need, стратегия call-by-value является , а не Тьюринг завершен .

Кто-нибудь может объяснить, пожалуйста, почему это так? Если это возможно, добавьте пример, пожалуйста.

Answer 1

Я оспариваю претензию в статье, которую вы читаете. (Мне не платят за это, поэтому я приведу аргументирующий аргумент, а не доказательство.)

Хорошо известно, что, по крайней мере, при уменьшении нормального порядка (он же называется по имени) чистое лямбда-исчисление является тьюрингово-полным. Но если мы посмотрим на основополагающую статью Джона Рейнольдса Определение интерпретаторов для языков программирования высшего порядка , мы увидим, что Рейнольдс подробно обсуждает разницу между вызовом по имени и вызовом по значению. Критическая часть аргумента состоит в том, что для того, чтобы провести правильное различие, мы можем преобразовать программу в стиль продолжения . Преобразование CPS отличается для вызова по необходимости и вызова по значению, но результирующие преобразованные термины могут быть оценены в любом стиле.

Итак, вот вам аргумент: напишите программу лямбда-исчисления, которая имитирует машину Тьюринга, затем преобразует CPS, используя преобразование CBN, и вы можете оценить полученный код, используя стратегию сокращения CBV. Взрыв! Тьюринг.

На практике могу поспорить, что вы можете написать программу CBV для эмуляции машины Тьюринга; вероятно, достаточно выбрать подходящий комбинатор с фиксированной запятой, такой как & Theta; например. (Более известный Y-комбинатор работает только в рамках стратегии сокращения по имени, то есть сокращения в обычном порядке.)

Отказ от ответственности: Я давно не изучал лямбда-исчисление, и я уверен, что в приведенном выше аргументе есть несколько неправильных деталей. Но я уверен в сути. Это был не первый раз, когда я обнаружил что-то явно неправильное в онлайн-ресурсах о теории языка программирования.

Answer 2

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

Существование комбинатора с фиксированной запятой по значению (т. Е. "Y комбинатор") для нетипизированного лямбда-исчисления, по-видимому, опровергает основное утверждение (см .: Фиксированный запор ). Существование такого комбинатора нарушает строгую нормализацию, что говорит о том, что есть по крайней мере один язык, который завершается по Тьюрингу, который использует стратегию оценки по стоимости.

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