Какие функции не может вычислить система F?

28

В этой статье в Википедии о полноте Тьюринга говорится, что:

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

Что является примером полной вычислимой функции, которая не вычислима системой F ?

Кроме того, поскольку Хиндли-Милнер это:

Ограничение Системы F

из-за того что:

проверка типов неразрешима для варианта System F в стиле Curry, то есть для варианта, в котором отсутствуют явные аннотации ввода.

Означает ли это, что лямбда-исчисление, лежащее в основе систем типа Хиндли-Милнера, также недостаточно полно?

Если это действительно так, поскольку haskell явно завершен по Тьюрингу, и мы знаем, что его основой являются лямбда-исчисление и система типов Хиндли-Милнера, какие функции, отсутствующие в лямбда-исчислении, добавлены для того, чтобы завершить тьюринг haskell?

Майк ХР
источник
Примером функции, которая делает полное тестирование Haskell, является интерфейс с собственным кодом.
Трисмегистос
@Cody спасибо за ваш комментарий. Я не знаком с системой T. Прав ли я, предполагая, что система T упоминается здесь ? как система T сравнивается и сравнивается с системой F?
Майк HR
ПРИМЕЧАНИЕ: при поиске в Google system T vs. system Fя нашел кое-что, что отвечает моему последнему подзапросу и перефразируется здесь так: как haskell добавил полноту Тьюринга к Системе F
Майк HR
1
Я думаю, что @Trismegistos поднимает интересную философскую проблему: что такое Хаскель, где его границы?
Мартин Бергер

Ответы:

45

Система довольно выразительна. Как доказано здесь Жираром , функции типа (где определяется как ) являются точно определимыми функциями ( ) во втором порядке арифметики Хейтинга . Обратите внимание, что это то же самое, что и функции, определяемые в арифметике Пеано второго порядка .НН НХ . X ( X X ) X NN H A 2FNNNX. X(XX)XNNHA2

Возможно, вы захотите проверить Proofs и Types как более читабельный справочник. Обратите внимание , что это означает , что много программ могут быть записаны в системе F, от функции Аккермана переводчиков для системы Геделя . Как и для любого общего языка программирования (с некоторыми мягкими условиями), система не может реализовать собственный интерпретатор , то есть функцию которая принимает в качестве входного кода для термина системы и возвращает (код для) нормальную форму дляF e v a l : NN t F tTFeval:NNtFt, Доказательство включает в себя вариант диагонализирующей уловки, используемой для неразрешимости проблемы остановки. Андрей прекрасно объясняет это здесь .

Чтобы ответить на ваши другие вопросы: языки -calculus, лежащие в основе языков Hindley-Milner (HM), также не являются полными по Тьюрингу. На самом деле она значительно слабее , чем система , ближе выразительность просто напечатанная -исчисления.F λλF λ

Haskell действительно завершен по Тьюрингу. Наиболее отличительной чертой, позволяющей это (хотя есть и другие), является наличие неограниченной рекурсии : определение любой программы (функции) может относиться к самой программе. Это похоже на добавление комбинатора, как это делается в определении PCF, которое просто набрано, но сохраняет полноту по Тьюрингу с комбинатором.YYY

Обратите внимание, что существуют другие функции, которые делают Haskell Turing завершенным, но они обычно не считаются частью основного языка, например ссылки на функции, неограниченные типы данных и т. Д.

Коди
источник
1
Вау, это удивительный ответ и отвечает на все отлично. Спасибо!
Майк HR
«Как и для любого общего языка программирования ...» Это не совсем правильно. Есть несколько самоинтерпретаторов для всех языков, которые, по моему пониманию, исключают не завершающиеся программы как плохо напечатанные. Смотрите эту статью
jmite
@jmite, как заявлено, моя заявка верна. Эта статья упоминается в связанном обсуждении, и у Андрея есть несколько последующих замечаний в его блоге: math.andrej.com/2016/01/04/…
cody
11

Несколько вводит в заблуждение утверждение о том, что система печати Хаскелла является «системой типов Хинли-Милнера». Типы Haskell гораздо более мощные, включая, среди прочего, типы с более высоким родом. Действительно, система ввода настолько мощна, что вы можете встраивать языки программирования, полные по Тьюрингу, в систему набора, см. Здесь . Это не единственная причина мощи Хаскелла, сказал Коди о некоторых других.

Мартин Бергер
источник
Спасибо. Мое основное знакомство с Хиндли-Милнером было через Хаскелл, так что, я думаю, я мог предположить, что в его состав входят более высокопородные типы. Хиндли-Милнер просто ссылается на вывод типа (так что, скорее всего, алгоритм W)? или это нечто большее? Я понимаю, что это есть математическая основа в лямбда-исчислении, я просто пытаюсь понять, где логические границы между мощной системой типов haskell и какова будет минимальная реализация системы типов Хиндли-Милнера.
Майк HR
NB. Если кого-то интересует мощь системы типов haskell, я бы порекомендовал видеофильм Эдварда Кметта о hask , который (глубоко) углубляется в теорию категорий с использованием системы типов haskell.
Майк HR
1
@ MikeH-R Обычно мы имеем в виду, что Хиндли – Милнер является системой типирования или, точнее, типизированным -calculus, тогда как алгоритм является алгоритмом вывода типов для системы Хиндли – Милнера. Что примечательно в системе Хиндли-Милнера, так это то, что она сочетает параметрический полиморфизм со способностью выводить наиболее общий тип любой заданной программы без аннотаций типов. Статья Википедии стоит читать. ВтλW
Мартин Бергер