Здравствуйте, kochetkov.vladimir, Вы писали:

KV>>>Если isFermaTheoremCorrect частично рекурсивна -- это не "несколько сложнее", а невозможно доказать в принципе.
KV>·>Доказать возможно (и теорема Ферма была доказана!)
KV>Я вообще не про доказательство теоремы, это не имеет никакого значения Моё замечание про доказательство того, по какой именно ветке пойдёт предложенный тобой алгоритм с if'ом, т.е. того, реализует ли данный алгоритм первоначальную функцию. Это теорема Райса в чистом виде.
Эта теорема говорит об алгоритмической неразрешимости, а не то, что "невозможно доказать в принципе". Не путай! Это очень разные понятия.

KV>·>Алгебра используется для построения доказательства функции.
KV>В результате которого мы получаем уже другую (эквивалентную исходной) функцию. В данном конкретном примере принципиальной разницы между "эквивалентна" и "является" нет, если допустить, что x принадлежит счётному множеству, на котором всюду определены используемые в функции арифметические операции (что в общем случае совершенно необязательно).
Ок, согласен. Надо уточнить что эти функции эквивалентны если они имеют одну и ту же область определения (что, вообще говоря, часто неявно подразумевается).

KV>·>Ок. Верно. Давай рассмотрим алгоритм "print 42". Он по обоим твоим пунктам удовлетворяет для функции f(x) = 42 + x — x. Так? Значит он корректно работает. Так?
KV>Пока ты не определил, какому множеству принадлежит x
Области определения функции. Например, пусть будет множество натуральных чисел, для определённости.

KV> и какие отношения определены на этом множестве
??

KV> -- нет, не "так", а "хз как". Но он удовлетворяет функции f(x) = 42 без этой оговорки.
Ок. Пойдём далее. Этот алгоритм корректно работает?