LINUX.ORG.RU

На чем основан алгоритм обнаружения бесконечных вычислений?

 , ,


0

5

Предположим, что у нас алгоритм вычисления того, существует ли предел натурального ряда. Он будет соответствовать индуктивному определению нат ряда Nnext=N+1. Запускаем его, допустим, на МТ. Надо сказать, что интуитивно понятно, что данное вычисление бесконечно. Но это не доказано. На самом деле, этот алгоритм и есть попытка доказательства этого, поскольку, если бы он когда нибудь остановился, мы могли бы сделать вывод, что данное вычисление конечно. То есть, мы получили бы доказательство от противного.

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

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

Ясно, что это лишь частный случай, и существует тьма подобных случаев. Количество которых недетерминированно.

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



Последнее исправление: CYB3R (всего исправлений: 1)

Не знаю как в доказательном программировании, а в суперкомпиляции для этого используется свисток.

buddhist ★★★★★
()

Присоединяюсь к анонимусу выше.

Если записать программу для Машины Тьюринга (ведь она же у тебя МТ), то сразу станет понятно, что машина не достигнет завершающего состояния.

vanzef
()
Ответ на: комментарий от tysonfury2015

Нет.

Это вполне можно формализовать. Как? Построить граф для программы, как это делается при компиляции и посмотреть достижимость состояния. Граф будет несвязным.

vanzef
()
Ответ на: комментарий от vanzef

Программа для МТ по определению конечна.

Не знал, что на лоре такие особи водятся. Переплюнул самого Тьюринга. ЛГБТ негодуе.

anonymous
()

Не для этого ли в математике придумали пределы и признаки сходимости рядов?

blexey ★★★★★
()
Ответ на: комментарий от blexey

То есть, по-вашему, признак сходимости === доказательство завершаемости?

anonymous
()
Ответ на: комментарий от tailgunner

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

anonymous
()

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

anonymous
()

Мы не можем доказать, что это вычисление бесконечно

Пруф в любом известном тебе proof-аssistant'е?

ymn ★★★★★
()
Ответ на: комментарий от anonymous

Анонiмусу надо было в юристы идти, в судах бы слабоумных опускал, судьи бы процессов, как праздника ждали...

Эх... Сраная совковая система образования и отсутствие хоть какой-то профориентации рандомно кидает людей по профессиям, отсюда и дрявая экономика и машины ТАЗ, собираемые алкашами с похмелья и разваливающиеся на ходу и остальные беды этой страны слабоумных.

anonymous
()

Анонiмус открыл для себя проблему останова?

Agda может определять только некоторые случаи, когда остановка точно произойдёт, для этого используются алгоритм, использованный в Foetus. Этот алгоритм очень ограничен, например такой случай он забракует (я уже крепко забыл её синтаксис, так что пусть будет haskell):

f :: Nat -> Nat
f x | x == 0 = 0
    | even x = f $ x + 1
    | True = f $ x - 2

Хотя очевидно, что эта ф-ция завершается, обо

f (f x) | x == 0 = 0
        | even x = f (x + 1 - 2) -> f $ (x - 1)
        | True  = f $ x - 4

(Когда-то я проверял этот пример, вроде не вру)

Был ещё язык MiniAgda, использующий sized-типы (т.е. типы, параметризуемые максимальной глубиной терма). Критерием остановки в этом случае будет просто уменьшающийся размер терма. Вроде сейчас их запилили и в Agda.

Но вообще, я не понимаю, что мешало набрать в поисковике «agda termination checker» и прочитать всё там, не прибегая к помощи лорчан с дырявой памятью.

fmdw
()
Последнее исправление: fmdw (всего исправлений: 1)
Ответ на: комментарий от fmdw

Ну вот, наконец адекватного ответа дождались:). Ясно, спасибо, закрыто.

tysonfury2015
() автор топика
Ответ на: комментарий от anonymous

Говоря «программа конечна», я имел в виду «код программы конечен», что вполне очевидно из контекста (речь шла о графе, вспомнил его название, CFG).

vanzef
()
Ответ на: комментарий от tysonfury2015

В общем случае --- нет, peregrine правильную ссылку дал.

В твоём примере --- имеет.

vanzef
()
Ответ на: комментарий от tysonfury2015

Ты тупой. Из кода выводим CFG, из CFG находим back edges, привязываем к ним induction variables, и если выражения для них достаточно простые - выводим интервалы. В llvm для этого отдельный pass есть.

anonymous
()
Ответ на: комментарий от anonymous

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

Одно другому не мешает.

korvin_ ★★★★★
()

ты реальной тупой, предел массива равен PHP_INT_MAX

Pooping
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.