История изменений
Исправление quasimoto, (текущая версия) :
Но не любая теория
Достаточно выразительная, да. Например, базовые Agda с Coq строго выразительней PA, так что тоже попадают под действие этих теорем (Гёделя, в смысле), хотя проблема останова и разрешима для них.
Если проблема останова разрешима - то, очевидно, и проблема эквивалентности становится тривиально разрешимой.
Но у нас всё равно нет чёрного ящика в который можно будет закидывать fib1 с fib2 (в каком виде вообще?) и за конечное время получать ответы «равны» или «не равны», туда придётся забросить так же и доказательство предполагаемо населяющее утверждение «fib1 = fib2» и получать тогда ответы «подходит» или «нет» — в такого рода языке пруфчек разрешим, да (отсутствие Тьюринг-полноты тут может играть роль), но в смысле Entscheidungsproblem этот частный случай этой проблемы остаётся неразрешим, я считаю, то есть автоматически строить доказательство для «fib1 = fib2» просто получив fib1 с fib2 (опять, в каком виде?) алгоритмически нельзя — можно перечислить все доказательства (считаем, что язык рекурсивно-перечислим), проверка доказательства занимает конечное время, так что _если_ утверждение истинно, то его автоматическое доказательство (чисто теоретически) займёт конечное время, проблема в том, что если оно ложно, то мы зависнем — такая штука не decidable, но semidecidable, что типично для автоматических пруверов (и вообще для процесса поиска доказательств), вообще в RE-complete находятся и проблема останова, Rice, Entscheidungsproblem, 10-ая проблема Гильберта и т.д.
Исходная версия quasimoto, :
Но не любая теория
Достаточно выразительная, да. Например, базовые Agda с Coq строго выразительней PA, так что тоже попадают под действие этих теорем (Гёделя, в смысле), хотя проблема останова и разрешима для них.
Если проблема останова разрешима - то, очевидно, и проблема эквивалентности становится тривиально разрешимой.
Но у нас всё равно нет чёрного ящика в который можно будет закидывать fib1 с fib2 (в каком виде вообще? по идее это числа Гёделя, что не даёт сказать ничего интересного) и за конечное время получать ответы «равны» или «не равны», туда придётся забросить так же и доказательство предполагаемо населяющее утверждение «fib1 = fib2» и получать тогда ответы «подходит» или «нет» — в такого рода языке пруфчек разрешим, да (отсутствие Тьюринг-полноты тут может играть роль), но в смысле Entscheidungsproblem этот частный случай этой проблемы остаётся неразрешим, я считаю, то есть автоматически строить доказательство для «fib1 = fib2» просто получив fib1 с fib2 (опять, в каком виде?) алгоритмически нельзя — можно перечислить все доказательства (считаем, что язык рекурсивно-перечислим), проверка доказательства занимает конечное время, так что _если_ утверждение истинно, то его автоматическое доказательство (чисто теоретически) займёт конечное время, проблема в том, что если оно ложно, то мы зависнем — такая штука не decidable, но semidecidable, что типично для автоматических пруверов (и вообще для процесса поиска доказательств), вообще в RE-complete находятся и проблема останова, Rice, Entscheidungsproblem, 10-ая проблема Гильберта и т.д.