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

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

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

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

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

• требуется, чтобы язык имел произвольные циклы (while) и динамическое выделение памяти (malloc)

• требуется, чтобы язык поддерживал произвольные рекурсивные функции

давайте рассмотрим несколько примеров не-Тьюринговых полных языков, которые некоторые люди могут тем не менее называть языками программирования.

• ранние версии FORTRAN не имели динамики выделение памяти. Вы должны были заранее выяснить, сколько памяти потребуется вашему вычислению, и выделить ее. Несмотря на это, Фортран когда-то был наиболее широко используемым языком программирования.

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

• Coq-это язык, предназначенный для доказательства теорем. Сейчас доказывание теорем и запуск программ очень тесно связаны, так что вы можете писать программы в Coq так же, как вы доказать теорему. Интуитивно, доказательство теоремы "a подразумевает B" - это функция, которая принимает доказательство теоремы A в качестве аргумента и возвращает доказательство теорема Б.

  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, иначе вы могли бы доказать что угодно, а не только истинные теоремы! Так Кок (и аналогичных программ для доказательства теорем) запретить произвольная рекурсия. Когда вы пишете рекурсивную функцию, вы должны докажите, что он всегда заканчивается, так что всякий раз, когда вы запускаете его на доказательство теоремы A, вы знаете, что он построит доказательство теоремы B.

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

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

• синхронные языки программирования это языки, предназначенные для программирования систем реального времени, то есть систем, в которых программа должна реагировать в меньше чем n тактов. Они главным образом использованы для mission-critical систем как управления корабля или signaling. Эти языки обеспечивают надежные гарантии того, как долго программа будет работать и сколько памяти она может выделить.

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

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

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