Каковы практические ограничения полный язык Тьюринга, такой как Coq?

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

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

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

Сейчас существует несколько очень разных видов языков, неполных по Тьюрингу, и они отличаются тем, что не могут делать. Однако есть и общая тема. Если вы разрабатываете язык, есть два основных способа гарантировать, что язык будет Тьюринг-полным:

• потребовать, чтобы в языке были произвольные циклы (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 тактов. Они в основном используются для критически важных систем, таких как системы управления транспортными средствами или сигнализации. Эти языки дают твердые гарантии того, сколько времени потребуется программе для выполнения и сколько памяти она может выделить.

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

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

Кстати, Дуглас Хофштадтер написал несколько очень интересных научно-популярных книг о вычислениях, в частности Гёдель, Эшер, Бах: вечная золотая коса. Я не помню, обсуждает ли он в явном виде ограничения Тьюринга-неполноты, но чтение его книг определенно поможет вам понять более технический материал.