Что может сделать Идрис, отказавшись от полноты Тьюринга?

35

Я знаю, что у Идриса есть зависимые типы, но он не завершен. Что он не может сделать, отказавшись от полноты Тьюринга, и связано ли это с наличием зависимых типов?

Я предполагаю, что это довольно специфический вопрос, но я не знаю много о зависимых типах и связанных системах типов.

Squidly
источник
2
Я полагаю, вы ищете конкретный пример? Я не знаком с Idris, но в Isabelle / HOL вы не можете писать (или, скорее, компилировать) функции, которые не всегда завершаются (что еще хуже, вам нужно предоставить подтверждение завершения ).
Рафаэль
Что-то в этом роде, да - я не был полностью уверен, будет ли что-то совершенно нишевое, например, вы не можете кодировать язык с определенными свойствами в системе типов, или это будет немного более общим (например, как вы сказали) все функции должны быть завершены)
Squidly
1
Думаю, это ошибочное предположение исходит от Эдвина Брэди, который говорит, что Идрис "Pacman complete". Я думаю, что его основной смысл, сказав «Pacman complete» вместо «Turing complete», заключается в том, что он хочет подчеркнуть важность того, чтобы языки легко компилировались человеческим мозгом, а не только машинами! .. глупые языки, такие как BrainFuck, безусловно Тьюринг завершен, но человеческому мозгу может потребоваться довольно много времени, чтобы понять код, написанный на BrainFuck, и, таким образом, разработать и, что еще более важно, поддержать программу Pacman на BrainFuck, которая требует больших усилий ..
Мишелрандаль
@ Митж Не совсем. Я думаю, это потому, что я неправильно понял что-то, что я слышал, как он говорил в разговоре.
Squidly

Ответы:

50

Идрис завершен! Он проверяет целостность (завершение при программировании с данными, производительность при программировании с использованием codata), но не требует, чтобы все было полным.

Интересно, что для моделирования полноты Тьюринга достаточно иметь данные и кодаты, поскольку вы можете написать монаду для частичных функций. Я сделал это много лет назад в Coq - сейчас, вероятно, это не очень хорошо, но здесь все же: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v .

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

Idris не будет сокращать частичные функции на уровне типов, чтобы проверка разрешалась. Кроме того, только тотальные программы могут обоснованно считаться доказательствами.

Эдвин Брейди
источник
4
Сам человек. Что такое производительность в этом контексте?
Squidly
5
Двойственный к завершению: в то время как индуктивное определение должно завершаться (потребляя все его данные), коиндуктивное определение должно быть продуктивным - на практике это означает, кратко, что рекурсивный вызов должен быть защищен конструктором. Я нашел это объяснение, чтобы быть самым ясным (ymmv): adam.chlipala.net/cpdt/html/Coinductive.html
Эдвин Брэди
14

Во-первых, я предполагаю, что вы уже слышали о тезисе Черча-Тьюринга , в котором говорится, что все, что мы называем «вычислением», - это то, что можно сделать с помощью машины Тьюринга (или любой из множества других эквивалентных моделей). Таким образом, полный по Тьюрингу язык - это язык, на котором можно выразить любое вычисление. И наоборот, неполным по Тьюрингу языком является тот, в котором есть некоторые вычисления, которые не могут быть выражены.

Хорошо, это было не очень информативно. Позвольте мне привести пример. Есть одна вещь, которую вы не можете сделать на любом неполном по Тьюрингу языке: вы не можете написать симулятор машины Тьюринга (в противном случае вы можете кодировать любые вычисления на моделируемой машине Тьюринга).

Хорошо, это все еще не было очень информативным. реальный вопрос в том, что полезная программа не может быть написана на неполном по Тьюрингу языке? Ну, никто не придумал определение «полезной программы», которое включает в себя все программы, которые кто-то где-то написал для полезной цели, и не включает в себя все вычисления машины Тьюринга. Поэтому разработка неполного по Тьюрингу языка, на котором вы можете написать все полезные программы, по-прежнему является долгосрочной исследовательской целью.

Сейчас есть несколько очень разных видов неполных по Тьюрингу языков, и они отличаются тем, что они не могут сделать. Однако есть общая тема: языки, полные тьюринга, должны включать в себя некоторый способ условного завершения или продолжения работы в течение времени, не ограниченного размером программы, и способ для программы использовать объем памяти, который зависит от ввода. , Конкретно, большинство императивных языков программирования предоставляют эти возможности через циклы while и динамическое распределение памяти соответственно. Большинство функциональных языков программирования предоставляют эти возможности через рекурсию и вложение структуры данных.

Идрис сильно вдохновлен Агда . Agda - это язык, разработанный для доказательства теорем . Теперь доказательство теорем и выполнение программ очень тесно связаны , поэтому вы можете писать программы в Agda так же, как доказываете теорему. Интуитивно, доказательство теоремы «A подразумевает B» - это функция, которая принимает доказательство теоремы A в качестве аргумента и возвращает доказательство теоремы B.

Поскольку целью системы является доказательство теорем, вы не можете позволить программисту писать произвольные функции. Представьте, что язык позволил вам написать глупую рекурсивную функцию, которая просто вызывала себя:

oops : A -> B
oops x = oops x

Вы не можете позволить существованию такой функции убедить вас, что A подразумевает B, иначе вы сможете доказать что угодно, а не только истинные теоремы! Таким образом, Агда (и аналогичные доказатели теорем) запрещают произвольную рекурсию. Когда вы пишете рекурсивную функцию, вы должны доказать, что она всегда завершается , так что всякий раз, когда вы запускаете ее для доказательства теоремы A, вы знаете, что она построит доказательство теоремы B.

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

В настоящее время проводится много исследований, посвященных тому, чтобы сделать системы доказательства более похожими на язык программирования, не ставя под угрозу их гарантию того, что если у вас есть функция от A до B, это так же хорошо, как математическое доказательство того, что A подразумевает B. Расширение системы для принятия большего числа завершающие функции - одна из тем исследования. Другие направления расширения включают в себя решение таких «реальных» задач, как ввод / вывод и параллелизм. Другая проблема заключается в том, чтобы сделать эти системы доступными для простых смертных (или, возможно, убедить простых смертных в том, что они действительно доступны).

Я не знаком с Идрисом. Это решение проблем, о которых я только что говорил. Насколько я понял из беглого взгляда на препринт 2013 , Идрис является Тьюринг-полной, но включает в себя совокупность шашку. Средство проверки целостности проверяет, что каждая функция, снабженная ключевым словом, totalзавершается. Фрагмент языка, который содержит только программы Idris, в которых каждая функция является полной, по выразительной силе похож на Arda (вероятно, не точное совпадение из-за различий в теории типов, но достаточно близко, чтобы вы не заметили, если не попытались умышленно).

Другие примеры языков, которые не являются полными по Тьюрингу по-разному, см. Каковы практические ограничения нетурингового полного языка, такого как Coq? (от которого этот ответ в значительной степени взят).

Жиль "ТАК - прекрати быть злым"
источник
3
"какая полезная программа не может быть написана на неполном по Тьюрингу языке?" Виртуальная машина Java.
Дэвид Ричерби
@DavidRicherby Разве ты не можешь? Действительно ли JVM завершена по Тьюрингу? Существует ограничение на размер отдельного объекта. Можете ли вы выделить неограниченное количество объектов и получить к ним доступ? Например, в C ответ кажется «нет», потому что существует только конечное число значений указателя.
Жиль "ТАК - перестать быть злым"
Для читателей, интересующихся этой частью, у нас есть еще один пост о том, почему не может быть языка программирования для точно всегда заканчивающихся языков.
Рафаэль
3
@ Жиль, я понимаю твою точку зрения, но разве это не более или менее эквивалентно тому, чтобы сказать, что ни один из существующих языков программирования не является полным по Тьюрингу? В конце концов, любая реализация столкнется с барьерами, о которых вы упомянули. Похоже, в комнате довольно большой слон, учитывая то, что Идрис теряет из-за неполной по Тьюрингу. Например, теряет ли он больше, чем любой другой язык? Если вы запрещаете неограниченное внешнее хранилище (например, программа перестает говорить «пожалуйста, вставьте следующий / предыдущий диск»), тогда любой язык тривиально неполон по Тьюрингу, поэтому любой вопрос по этому случаю является пустым.
Дэвид Ричерби
3
@DavidRicherby Мои комментарии (но не мой ответ) в режиме гика теории языка программирования. Если вы возьмете формальную спецификацию SML (например), можно спроектировать (но, конечно, не реализовать в физическом мире) реализацию языка, которая может моделировать все вычислимые программы. Это не так в C, потому что конечность памяти встроена в язык ( sizeof(void*)). В своем ответе я отношусь к языкам идеализированным образом, поэтому SML или C будут считаться завершенными по Тьюрингу.
Жиль "ТАК - перестань быть злым"