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


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

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

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

4 54

4 ответа:

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

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

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

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

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

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

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

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

самый прямой ответ: машина / язык, который не является полным Тьюрингом, не может использоваться для реализации/моделирования машин Тьюринга. Это происходит из основного определения полноты Тьюринга: машина/язык является полным Тьюрингом, если он может реализовать/имитировать машины Тьюринга.

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

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

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

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

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

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

это ограничение приводит к необходимости выражать такие проблемы менее естественным образом.

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

Так как "на практике" вы будете давно ушли, прежде чем ваш компьютер может имитировать машину Тьюринга для 2^128 шаги, справедливо сказать, что незавершенность Тьюринга не имеет большого значения "в практика."