Может ли зависимо типизированный язык быть полным по Тьюрингу?
Кажется, что зависимо типизированные языки часто не являются полными по Тьюрингу. Почему мы не можем позволить каждой функции иметь общую рекурсию (что сделало бы язык Тьюринга полным), вместо того, чтобы разрешить только более ограниченную форму рекурсии?
Что-то мешает создателям зависимо типизированных языков разрешить всем функциям возможность общей рекурсии?
Например:
@AntC «Тьюринг завершен» не означает «может решить проблему остановки».
@AntC, да? Это полная противоположность реальности. Каждый язык программирования является полным по Тьюрингу, как и множество вещей, на которые нужно очень сильно прищуриться, чтобы увидеть, что они могут выполнять вычисления.
Ик, спасибо, ребята. Мозг-о. Должно быть, я путаю с «решить проблему остановки».
Я немного поработал над формулировкой вопроса и названием. Это все еще соответствует вопросу, который вы хотите задать? Я включил деталь, которую, по моему мнению, упустили из виду. Эта конкретная деталь, я считаю, до сих пор приводит к путанице. Сделав это явным, мы сможем более эффективно решить этот вопрос. Надеюсь, это поможет, и дайте мне знать, если это не соответствует тому, что вы хотите спросить!
На случай, если он не будет открыт повторно, вот ответ: есть что-то, что мешает многим создателям зависимо типизированных языков сделать его полным по Тьюрингу «очевидным» способом (путем разрешения общей рекурсии повсюду). Мы можем рассматривать систему типов как соответствующую своего рода логике. С этой точки зрения мы можем писать программы, соответствующие доказательствам теорем. Но разрешение каждой функции выполнять общую рекурсию приводит к противоречивой логике. Однако мы все равно можем получить полноту по Тьюрингу другим способом, проявив немного большую осторожность. См. ответ @gallais для хорошего обзора этого.
Ответы 1
То, что вы прочитали, является дезинформацией.
Например, в IO.Base вы можете увидеть, что стандартная библиотека Agda поставляется с
комбинатор под названием forever, который успешно выполняет действие IO до тех пор, пока
конец времен (или, что более вероятно, действие IO в конечном итоге решает
вызвать либо exitSuccess, либо exitFailure):
forever : IO {a} ⊤ → IO {a} ⊤
Функции вы конечно не найдете fix : (A → A) → A но это так
потому что тип должен быть честен в отношении возможности незавершения
(точно так же, как типы в Haskell должны честно говорить о возможности
мутация, или ввод-вывод, или сбой). Чтобы инкапсулировать такие эффекты, вы
обычно используют монады. Выше мы использовали монаду IO, но есть и другие
монады, улавливающие идею незавершенности, ср. Полнота Тьюринга Макбрайда совершенно бесплатно
Ух ты. ХОРОШО. Это отличный ответ - спасибо. Но почему в различных местах сообщается, что agda не является полной по Тьюрингу? Откуда это вообще взялось?
Именно здесь полезно рассматривать Agda как неполный по Тьюрингу DSL, который производит полные по Тьюрингу действия ввода-вывода.
Я чувствую, что это несколько обманчиво избегает истины. Мотивация использования этих языков в качестве систем доказательства и плохое взаимодействие этой идеи с самореференцией полностью утрачены.
Я думаю, что ответ дает некоторую полезную информацию, которая часто теряется, но в то же время я согласен с @DanielWagner. Полностью неограниченная общая рекурсия приводит к противоречивости, если рассматривать язык как логику. Чтобы избежать этого, вам придется тщательно ограничить его.
@DanielWagner, не могли бы вы рассказать мне об этом подробнее? Спасибо :)
🤷 нет ничего обманчивого в том, что типы должны честно говорить о нерасторжении. И это не какой-то загадочный выход: используя бисимуляции, вы можете доказать свойства этих потенциально незавершаемых программ!
Меня смущает вопрос: ни один язык программирования не является полным по Тьюрингу. Это, скорее, была точка зрения Тьюринга (и Гёделя). Не просто «часто», а всегда. Тогда что вы конкретно спрашиваете о языках с зависимой типизацией?