Так как есть не-Тьюринговые полные языки, и, учитывая, что я не изучал Comp Sci в университете, может кто-то объяснить что-то, что Turing-неполный язык (например, Coq) не может?
Или это полнота/неполнота, не представляющая практического интереса (т.е. не имеет большого значения на практике)?
РЕДАКТИРОВАТЬ. Я ищу ответ в соответствии с тем, что вы не можете создать хеш-таблицу на не-Тьюринговом полном языке из-за X или что-то в этом роде!
Во-первых, я полагаю, вы уже слышали о тесте Church-Turing, в котором говорится, что все, что мы называем "вычислением", является тем, что может быть выполнено с помощью машины Тьюринга (или любой из многих других эквивалентных моделей). Таким образом, язык Turing-complete - это тот, в котором могут быть выражены любые вычисления. Наоборот, язык Turing-неполный - это тот, в котором есть некоторые вычисления, которые не могут быть выражены.
Хорошо, это было не очень информативно. Позвольте мне привести пример. Есть одна вещь, которую вы не можете сделать ни на одном языке Turing-неполного: вы не можете написать симулятор машины Тьюринга (иначе вы могли бы кодировать любые вычисления на моделируемой машине Тьюринга).
Хорошо, это все еще не очень информативно. реальный вопрос: какая полезная программа не может быть написана на языке Тьюринга? Ну, никто не придумал определение "полезной программы", которое включает в себя все программы, которые кто-то где-то написал для полезной цели, и это не включает все машинные вычисления Тьюринга. Поэтому разработка Turing-неполного языка, в котором вы можете написать все полезные программы, по-прежнему является очень долгосрочной исследовательской целью.
Теперь существует несколько очень разных типов Turing-неполных языков, и они отличаются тем, чего они не могут сделать. Однако есть общая тема. Если вы разрабатываете язык, существуют два основных способа гарантировать, что язык будет заполнен Тьюрингом:
требуют, чтобы язык имел произвольные циклы (while) и распределение динамической памяти (malloc)
требуют, чтобы язык поддерживал произвольные рекурсивные функции
Посмотрите на несколько примеров полных языков, отличных от Turing, которые некоторые люди могут, тем не менее, вызывать языки программирования.
Ранние версии FORTRAN не имели динамического распределения памяти. Вам нужно было заранее выяснить, сколько памяти потребует ваше вычисление и распределить это. Несмотря на это, FORTRAN когда-то был самым широко используемым языком программирования.
Очевидным практическим ограничением является то, что перед запуском программы необходимо предугадать требования к памяти вашей программы. Это может быть трудным и может быть невозможным, если размер входных данных не ограничен заранее. В то время человек, который кормил входные данные, часто был человеком, который написал программу, поэтому это было не так уж и важно. Но это не так для большинства программ, написанных сегодня.
Coq - это язык, разработанный для теорем доказывания. Теперь теоремы доказывания и запущенные программы очень тесно связаны, поэтому вы можете писать программы в Coq так же, как вы доказываете теорему. Интуитивно доказательство теоремы "A означает, что B" является функцией, которая берет доказательство теоремы A как аргумент и возвращает доказательство теоремы B.
Поскольку цель системы - доказать теоремы, вы не можете позволить программисту писать произвольные функции. Представьте, что язык позволил вам написать глупую рекурсивную функцию, которая только что называлась (выберите линию, которая использует ваш любимый язык):
theorem_B boom (theorem_A a) { return boom(a); }
let rec boom (a : theorem_A) : theorem_B = boom (a)
def boom(a): boom(a)
(define (boom a) (boom a))
Вы не можете позволить существованию такой функции убедить вас, что A подразумевает B, иначе вы сможете доказать что-либо, а не только истинные теоремы! Таким образом, Coq (и аналогичные теоретические теоремы) запрещают произвольную рекурсию. Когда вы пишете рекурсивную функцию, вы должны доказать, что она всегда заканчивается, так что всякий раз, когда вы запускаете ее на доказательстве теоремы A, вы знаете, что она построит доказательство теоремы B.
Немедленное практическое ограничение Coq заключается в том, что вы не можете писать произвольные рекурсивные функции. Поскольку система должна иметь возможность отклонить все функции, не связанные с завершением, неразрешимость проблемы остановки (или, в более общем смысле, Теорема Риса) гарантирует, что есть также прекращающие функции, которые также отвергаются. Дополнительной практической трудностью является то, что вы должны помочь системе доказать, что ваша функция завершается.
В настоящее время проводится много исследований, направленных на то, чтобы сделать защищенные системы более похожими на язык программирования, не ставя под угрозу их гарантию, что если у вас есть функция от A до B, это не хуже математического доказательства того, что A подразумевает B. Расширение системы принимать больше завершающих функций является одной из тем исследований. Другие направления распространения включают в себя решение таких проблем "реального мира", как ввод/вывод и concurrency. Другая задача состоит в том, чтобы сделать эти системы доступными для простых смертных (или, возможно, убедить простых смертных, что они действительно доступны).
Языки синхронного программирования - это языки, предназначенные для программирования систем реального времени, то есть систем, в которых программа должна отвечать меньше, чем n тактов. Они в основном используются для критически важных систем, таких как управление транспортным средством или сигнализация. Эти языки предоставляют надежные гарантии того, сколько времени потребуется программе для выполнения и сколько памяти она может выделить.
Конечно, аналогию таких сильных гарантий является то, что вы не можете писать программы, потребление памяти и время работы которых вы не можете предсказать заранее. В частности, вы не можете записать программу, потребление или время которой зависит от входных данных.
Существует много специализированных языков, которые даже не пытаются программировать языки и поэтому могут оставаться вдалеке от полноты Тьюринга: регулярные выражения, языки данных, большинство языков разметки,...
Кстати, Дуглас Хофстадтер написал несколько очень интересных научно-популярных книг об вычислениях, в частности Гёдель, Эшер, Бах: Вечная золотая оплетка. Я не помню, явно ли он обсуждает ограничения Тьюринга-неполноты, но чтение его книг определенно поможет вам понять больше технических материалов.
Самый прямой ответ: машина/язык, который не является Тьюрингом, не может использоваться для реализации/моделирования машин Тьюринга. Это происходит из базового определения полноты Тьюринга: машина/язык завершается полным, если он может реализовать/моделировать машины Тьюринга.
Итак, каковы практические последствия? Ну, есть доказательство того, что все, что может показаться полным, может решить все вычислимые проблемы. Что по определению означает, что все, что не является совершенным, имеет гандикап, что есть некоторые вычислимые проблемы, которые он не может решить. Эти проблемы зависят от того, какие функции отсутствуют, что делает систему без Тьюринга полной.
Например, если язык не поддерживает петлю или рекурсию или неявные циклы, невозможно завершить Тьюринг, потому что машины Тьюринга могут быть запрограммированы на запуск навсегда. Следовательно, язык не может решить проблемы, требующие циклов.
Другим примером является то, что язык не поддерживает списки или массивы (или позволяет ими имитировать их, например, используя файловую систему), тогда он не может реализовать машину Тьюринга, поскольку машины Тьюринга требуют произвольного произвольного доступа к памяти. Следовательно, язык не может решить проблемы, требующие произвольного произвольного доступа к памяти.
Таким образом, отсутствующая функция, которая классифицирует язык, который не содержит Тьюринга, - это то, что практически ограничивает полезность языка. Итак, ответ: зависит от того, что делает язык не Тьюринга полным?
Важным классом проблем, которые плохо подходят для таких языков, как Coq, являются те, чье завершение предположительно или трудно доказать. Вы можете найти множество примеров в теории чисел, возможно, самым известным является гипотеза Коллатца
function collatz(n)
while n > 1
if n is odd then
set n = 3n + 1
else
set n = n / 2
endif
endwhile
Это ограничение приводит к тому, что в Coq приходится выражать такие проблемы менее естественным образом.
Вы не можете написать функцию, имитирующую машину Тьюринга. Вы можете написать функцию, которая имитирует машину Тьюринга для шагов 2^128 (или 2^2^2^2^128) и сообщает, что машина Тьюринга принята, отклонена или запущена дольше, чем допустимое количество шагов.
Поскольку "на практике" вам уже давно не удастся, прежде чем ваш компьютер сможет имитировать машину Тьюринга для шагов 2^128, справедливо сказать, что неполнота Тьюринга не имеет большого значения "на практике".