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

StackOverflow https://stackoverflow.com/questions/3492188

Вопрос

Поскольку существуют языки, не являющиеся полными по Тьюрингу, и, учитывая, что я не изучал компьютерные науки в университете, может ли кто-нибудь объяснить что-то, что неполный по Тьюрингу язык (например Coq) не можешь сделать?

Или это полнота /неполнота какого-либо реального практичный интерес (т.е.разве это не имеет большого значения на практике)?

Редактировать - Я ищу ответ в следующем роде вы не можете создать хэш-таблицу на языке, не являющемся полным по Тьюрингу, из-за X, или что-то в этом роде!

Это было полезно?

Решение

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

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

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

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

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

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

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

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

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

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

Кстати, Douglas Hofstadter написал несколько очень интересных научно-популярных книг о вычислениях, в частности Gödel, Escher, Bach:вечная Золотая Коса.Я не помню, обсуждает ли он явно ограничения неполноты по Тьюрингу, но чтение его книг определенно поможет вам понять больше технического материала.

Другие советы

Наиболее прямым ответом является: машина / язык, который не завершен Turing, не может использоваться для реализации / моделирования Turging Machines. Это исходит из основного определения полноты Turging: машина / язык предназначен для заполнения, если она может реализовать / симулировать Turging Machines.

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

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

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

Итак, функция, которая отсутствует, которая классифицирует язык, чтобы быть завершенным завершенным, - это то, что практически ограничивает полезность языка. Таким образом, ответ в том, что зависит: что делает языком не завершенным?

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

function collatz(n)
  while n > 1
    if n is odd then
      set n = 3n + 1
    else
      set n = n / 2
    endif
 endwhile

Это ограничение приводит к тому, чтобы выразить такие проблемы менее естественным образом в CoQ.

Вы не можете написать функцию, которая имитирует Turging Machine. Вы можете написать функцию, которая имитирует Turging Machine для 2^128 (или 2^2^2^2^128 Шаги) и сообщает, принимается ли Turging Machine, отклоненная или пробежала дольше, чем допустимое количество шагов.

Поскольку «на практике» вы будете давно договориться до того, как ваш компьютер сможет имитировать Turging Machine для 2^128 Шаги, справедливо сказать, что Turging неполнота не имеет большого значения «на практике».

Лицензировано под: CC-BY-SA с атрибуция
Не связан с StackOverflow
scroll top