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

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

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

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

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

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

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

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

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

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

Сейчас есть несколько очень разных видов неполных по Тьюрингу языков, и они отличаются тем, что они не могут сделать. Однако есть общая тема: языки, полные тьюринга, должны включать в себя некоторый способ условного завершения или продолжения работы в течение времени, не ограниченного размером программы, и способ для программы использовать объем памяти, который зависит от ввода. , Конкретно, большинство императивных языков программирования предоставляют эти возможности через циклы 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? (от которого этот ответ в значительной степени взят).