Практические языки, не содержащие Тьюринга?

Ответ 1

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

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

Еще одна система, которая более полно решает эту концепцию расслоения, Hume. Отчет дает полное описание системы и ее пяти уровней постепенно более полных и постепенно менее безопасных языков.

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

Ответ 2

BlooP (сокращение от B выделенного цикла) является интересным, -Турговый язык. Это, по существу, язык, содержащий Turing, с одним (основным) предупреждением: каждый цикл должен содержать оценку количества итераций. Бесконечные петли не допускаются. В результате проблема Halting может быть решена для программ BlooP.

Ответ 3

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

function confusion()
{
    if( halts( confusion ) )
    {
        while True:
            no-op
    }
    else
        return;
}

Любой язык, который не может выполнять рекурсию или циклы, на самом деле не будет "универсальным".

Регулярные выражения и машины с конечным состоянием - одно и то же! Лексинг и соответствие строк - одно и то же! Причина остановки FSM заключается в том, что они никогда не зацикливаются; они просто передают вход char -by- char и выходят.

EDIT:

Для многих алгоритмов очевидно, будут ли они останавливаться.

например:

function nonhalting()
{
    while 1:
        no-op
}

Эта функция, очевидно, никогда не останавливается.

И эта функция, очевидно, останавливается:

function simple_halting_function()
{
    return 1;
}

Итак, нижняя строка: вы можете гарантировать, что ваш алгоритм остановится, просто спроектируйте его так, чтобы он это делал.

Если вы не уверены, что алгоритм остановится все время; то вы, вероятно, не сможете реализовать его на любом языке, который гарантирует "остановку".

Ответ 4

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

Ответ 5

Оказывается, это довольно легко завершить. Например, вам нужны только 8 инструкций ala BrainF ** k, и более того, вам действительно нужно только одна инструкция.

Сердцем этого языка является конструкция цикла, и как только у вас есть неограниченные циклы, у вас есть неотъемлемая проблема с остановкой. Когда цикл завершится? Даже в не-Тьюрингском полном языке, который поддерживал неограниченные циклы, вы могли по-прежнему иметь проблему с остановкой в ​​практика.

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

Ответ 6

"устранить необходимость теоретически бесконечной памяти". -- Ну, да. Любой физический компьютер ограничен энтропией вселенной и, даже до этого, скоростью света (== максимальная скорость распространения информации).

Еще проще, на физически реализуемом компьютере, просто контролировать потребление ресурсов и накладывать на него определенные ограничения. (то есть, когда память или потребление времени > MY_LIMIT, убейте процесс).

Если вы просите чисто математическое/теоретическое решение, как вы определяете "общую цель"?

Ответ 7

Правильный способ сделать это, ИМХО, состоит в том, чтобы иметь язык, который является Тьюрингом полным, но предоставить систему для формулировки семантики, поддающейся обработке с помощью проверки проверки.

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

Как и в моем производственном компиляторе, у меня есть рекурсии, которые, как я знаю, наверняка не остановятся на некоторых входах. Я использую неприятный взломать, чтобы остановить это: счетчик с "разумным" пределом. FYI, фактический код связан с мономорфизацией полиморфного кода, а бесконечное расширение происходит при использовании полиморфной рекурсии. Haskell ловит это, мой компилятор для Felix не делает (что ошибка в компиляторе я не знаю, как исправить).

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

Возможно, это заслуживает другого вопроса.

Ответ 8

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