Во-первых, я предполагаю, что вы уже слышали о тезисе Черч-Тьюринга , в котором говорится, что все, что мы называем «вычислением», - это то, что можно сделать с помощью машины Тьюринга (или любой из множества другие эквивалентные модели). Таким образом, полный по Тьюрингу язык - это язык, на котором можно выразить любое вычисление. И наоборот, неполным по Тьюрингу языком является тот, в котором есть некоторые вычисления, которые не могут быть выражены.
Хорошо, это было не очень информативно. Позвольте мне привести пример. Есть одна вещь, которую вы не можете сделать на любом неполном по Тьюрингу языке: вы не можете написать симулятор машины Тьюринга (в противном случае вы можете кодировать любые вычисления на моделируемой машине Тьюринга).
Хорошо, это все еще не было очень информативным. реальный вопрос в том, что полезная программа не может быть написана на неполном по Тьюрингу языке? Ну, никто не придумал определение «полезной программы», которое включает в себя все программы, которые кто-то где-то написал для полезной цели, и не включает в себя все вычисления машины Тьюринга. Поэтому разработка неполного по Тьюрингу языка, на котором вы можете написать все полезные программы, по-прежнему является очень долгосрочной исследовательской целью.
Теперь есть несколько очень разных видов неполных по Тьюрингу языков, и они отличаются тем, что они не могут сделать. Однако есть общая тема. Если вы разрабатываете язык, есть два основных способа гарантировать, что язык будет полным по Тьюрингу:
требует, чтобы язык имел произвольные циклы (while) и динамическое выделение памяти (malloc)
требует, чтобы язык поддерживал произвольные рекурсивные функции
Давайте рассмотрим несколько примеров полнотекстов Тьюринга, которые некоторые люди, тем не менее, могут называть языками программирования.
Ранние версии 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. Расширение системы принять больше завершающих функций является одной из тем исследования. Другие направления расширения включают в себя решение таких «реальных» задач, как ввод / вывод и параллелизм. Другая проблема заключается в том, чтобы сделать эти системы доступными для простых смертных (или, возможно, убедить простых смертных в том, что они действительно доступны).
Синхронные языки программирования - это языки, предназначенные для программирования систем реального времени, то есть систем, в которых программа должна реагировать менее чем за n тактовых циклов. Они в основном используются для критически важных систем, таких как управление транспортным средством или сигнализация. Эти языки дают надежные гарантии того, сколько времени займет выполнение программы и сколько памяти она может выделить.
Конечно, аналог таких сильных гарантий заключается в том, что вы не можете писать программы, потребление памяти и время работы которых вы не можете предсказать заранее. В частности, вы не можете написать программу, чье потребление памяти или время работы зависят от входных данных.
Есть много специализированных языков, которые даже не пытаются быть языками программирования и поэтому могут оставаться далеко от полноты Тьюринга: регулярные выражения, языки данных, большинство языков разметки, ...
Кстати, Дуглас Хофштадтер написал несколько очень интересных научно-популярных книг о вычислениях, в частности Гёдель, Эшер, Бах: вечная золотая коса . Я не помню, обсуждает ли он явно ограничения неполноты Тьюринга, но чтение его книг определенно поможет вам понять больше технических материалов.