История изменений

я понимал естественно совсем НЕ саму функцию, но _определение_ функции

То есть

• У алгоритмически вычислимой функции может быть определение в виде алгоритма.

Только ещё есть варианты:

• У алгоритмически вычислимой функции может не быть (быть неизвестно) определение в виде алгоритма.
• Функция может быть невычислима. Каким определением-алгоритмом она задаётся?
• Функция может быть вычислимой или нет, но задаваться косвенно (ДУ, например). И график функции (который строит алгоритм) может быть не интересен, могут быть нужны только свойства функции (которые не получаются прямым алгоритмическим перебором).

Я правда не вполне понимаю, как можно узнать завис, или не завис недетерминированный алгоритм?

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

И я не понимаю, какой вообще смысл в этой вашей задаче?

Отлавливать опечатки и логические ошибки приводящие к зависаниям в циклах и stack overflow в рекурсии (в том числе между разными функциями) во время набора кода.

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

Никакой «логики математики» и «самой себя» нету. Математика вообще это одно, а теоремы Гёделя (_теоремы_, что характерно) утверждают определённые свойства формальных систем. Именно, если язык теории не достаточно богат, то в такой теории (возможно) всякая правда будет настоящей правдой (sound => consistent), а всякая настоящая правда найдёт своё (доказуемое) отражение в такой теории (complete). Примеры таких теорий - аксиоматика Тарского для Евклидовой геометрии и арифметика Пресбургера (которая слабее PA). Такие теории не попадают под действие (первой) теоремы о неполноте.

Теоремы о неполноте отвечают на вопрос о том что будет когда аксиоматическая система станет достаточно богатой, так что в ней станет возможна рефлексия - она тут же станет универсальной системой годной для того чтобы служить основанием для самой себя и для всей математики вообще, или так и останется просто одной из формальных дедуктивных систем? В такой богатой системе будет возможно построить высказывания вроде «это утверждение недоказуемо» и «данная система непротиворечива». Такая богатая теория не сможет быть одновременно complete & (sound | consistent) (для простоты - достаточно рассмотреть «парадокс лжеца»). Если теория полагает что она непротиворечива - она противоречива. Теория может считать, что она противоречива и при этом быть непротиворечивой (outside). Что обычно нужно это непротиворечивость (outside, но не допущение таковой inside) и, как следствие, неполная теория которая не может рассуждать о самой себе, но при этом вполне справляется с доказательством всех остальных теорем для формализации которых эта теория и создавалась. То есть вот есть теория, она используется по назначению, но рассуждать о свойствах этой теории нужно не в самой теории, а во внешнем «фреймворке для выявления общезначимости», то есть в метатеории (например, рассуждать о PA можно в видоизменённой PA или в ZFC).

[...] it's a simple matter, this theorem. It says that Parliament cannot grant itself an amnesty by the vote of one of its sub-committees, nor by itself: it must at least bring in some members from the outside. Isn't that just common sense? Or, alternatively, that you can't fix your glasses while keeping them on your nose.

(c) J.Y.Girard.

Правда, чтобы рассуждать о «фреймворке» нужен «фреймворк для фреймворка» и далее turtles all the way down (PA -> PA' + transfinite induction -> ZFC -> ZFC + Grothendieck Universe -> ?).

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

Что будет если вычислитель станет Тьюринг-полным? Будет существовать программа способная решить завершается ли любая данная программа или нет?

я понимал естественно совсем НЕ саму функцию, но _определение_ функции

То есть

• У алгоритмически вычислимой функции может быть определение в виде алгоритма.

Только ещё есть варианты:

• У алгоритмически вычислимой функции может не быть (быть неизвестно) определение в виде алгоритма.
• Функция может быть невычислима. Каким определением-алгоритмом она задаётся?
• Функция может быть вычислимой или нет, но задаваться косвенно (ДУ, например). И график функции (который строит алгоритм) может быть не интересен, могут быть нужны только свойства функции (которые не получаются прямым алгоритмическим перебором).

Я правда не вполне понимаю, как можно узнать завис, или не завис недетерминированный алгоритм?

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

И я не понимаю, какой вообще смысл в этой вашей задаче?

Отлавливать опечатки и логические ошибки приводящие к зависаниям в циклах и stack overflow в рекурсии (в том числе между разными функциями) во время набора кода.

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

Никакой «логики математики» и «самой себя» нету. Математика вообще это одно, а теоремы Гёделя (_теоремы_, что характерно) утверждают определённые свойства формальных систем. Именно, если язык теории не достаточно богат, то в такой теории (возможно) всякая правда будет настоящей правдой (sound => consistent), а всякая настоящая правда найдёт своё (доказуемое) отражение в такой теории (complete). Примеры таких теорий - аксиоматика Тарского для Евклидовой геометрии и арифметика Пресбургера (которая слабее PA). Такие теории не попадают под действие (первой) теоремы о неполноте.

Теоремы о неполноте отвечают на вопрос о том что будет когда аксиоматическая система станет достаточно богатой, так что в ней станет возможна рефлексия - она тут же станет универсальной системой годной для того чтобы служить основанием для самой себя и для всей математики вообще, или так и останется просто одной из формальных дедуктивных систем? В такой богатой системе будет возможно построить высказывания вроде «это утверждение недоказуемо» и «данная система непротиворечива». Такая богатая теория не сможет быть одновременно complete & (sound | consistent) (для простоты - достаточно рассмотреть «парадокс лжеца»). Если теория полагает что она непротиворечива - она противоречива. Теория может считать, что она противоречива и при этом быть непротиворечивой (outside). Что обычно нужно это непротиворечивость (outside, но не допущение таковой inside) и, как следствие, неполная теория которая не может рассуждать о самой себе, но при этом вполне справляется с доказательством всех остальных теорем для формализации которых эта теория и создавалась. То есть вот есть теория, она используется по назначению, но рассуждать о свойствах этой теории нужно не в самой теории, а во внешнем «фреймворке для выявления общезначимости», то есть в метатеории (например, рассуждать о PA можно в видоизменённой PA или в ZFC).

[...] it's a simple matter, this theorem. It says that Parliament cannot grant itself an amnesty by the vote of one of its sub-committees, nor by itself: it must at least bring in some members from the outside. Isn't that just common sense? Or, alternatively, that you can't fix your glasses while keeping them on your nose.

(c) J.Y.Girard.

Правда, чтобы рассуждать о «фреймворке» нужен «фреймворк для фреймворка» и далее turtles all the way down (PA -> PA' + transfinite induction -> ZFC -> ZFC + Grothendieck Universe -> ?).

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

Что будет если вычислитель станет Тьюринг-полным? Будет существовать программа способная решить завершается ли любая данная программа или нет?