понятие вычислимой/невычислимой функции

[epros]

(Оффтоп)

arseniiv в сообщении #1513764 писал(а):

Просто фундаментальную или ещё и с «регулятором сходимости»?

Э-ээ, зачем? По-моему, любая фундаментальная последовательность рациональных чисел "куда-нибудь" да сходится.

-- Сб апр 10, 2021 17:00:22 --

svv в сообщении #1513766 писал(а):

У дилетанта тогда сразу возникает вопрос: что, и $\operatorname{sign}(x)$ невычислима?

Ну, дык, выше об этом и было написано.

[manul91]

epros в сообщении #1513748 писал(а):

Мы предположили, что алгоритм правильно разрешает вопрос остановки по любому предъявленному ему коду алгоритма. Нет никакого разумного способа отделить "неправильные" случаи работы разрешающего алгоритма от "правильных". Либо весь алгоритм в целом правильный, либо мы не можем полагаться на выдаваемые им результаты. Дописывать к разрешающему алгоритму какие-то проверки того, не предъявлен ли ему "его собственный" код, очевидно бессмысленно. Потому что если разрешающий алгоритм существует, то он должен как-то анализировать логику "зацикливания", независимо от того, чей это код - его собственный или нет. Отказ анализировать какие-то конкретные коды просто ничего не даст.

Все-таки интересно, можно ли говорить про "достаточно" и "недостаточно" хороших разрешашающих алгоритмов насчет вопроса останова, и насколько это будет осмысленно?
Доказательство невозможности универсального разрешающего алгоритма ничего об этом не говорит.
Вот например с практической точки зрения понятно что если даны два "частично разрешающих" алгоритма $A_1$ и $A_2$; и $A_1$ правильно решает вопроса остановки на подмножества $G_{A_1}$ программ (из всех программ $G$) и лажает на остальных; а $A_2$ правильно решает вопроса остановки на подмножества $G_{A_2}$ (из всех программ $G$) - и если при этом $G_{A_1} \subset G_{A_2}$ - то во вполне понятном смысле $A_2$ тогда является "лучшим разрешателем останова" чем $A_1$.
В какой степени это можно улучшить, и можно ли сформулировать разумных требований к "частично разрешающего проблему останова" алгоритма $A$, чтобы он ошибался "настолько редко насколько возможно"?

Еще вот (в связи с "изолированности контекста гипервизора и гостя на аппаратном уровне"....: )
В наивной теории множеств избегали подобного "парадокса лжеца", путем присваивания статус "класса" неких множеств с наложения соответных ограничений... Притом там из-за бесконечностей множеств похоже, похоже тоже нельзя дать вычислимые алгоритмы сравнения.
Нельзя ли подобным образом поделить алгоритмы на классы, задавая им необходимые свойства/ограничения - чисто декларативно (рукомахательством)? Типа $A$ должен уметь разрешать проблему остановки для всех алгоритмов $B$ которые "ниже классом" чем $A$ (не реализируют и не используют внутри у себя "сути" $A$)?

-- 10.04.2021, 17:24 --

epros в сообщении #1513748 писал(а):

С синусом всё, как ни странно, проще. Это аналитическая функция. Просто берём разложение синуса в степенной ряд около нуля и для любого аргумента (который сам по себе является некой фундаментальной последовательностью рациональных чисел) находим фундаментальную последовательность рациональных чисел, которая сходится к значению функции.

При этом найти $sign(\sin x)$ в общем случае, тоже нельзя ...

[epros]

manul91 в сообщении #1513769 писал(а):

Нельзя ли подобным образом поделить алгоритмы на классы, задавая им необходимые свойства/ограничения - чисто декларативно (рукомахательством)?

Почему бы и нет? Очевидно, что некие простые случаи зацикливания посредством автоматического анализа кода обнаружить вполне можно. Путём добавления кода, анализирующего более сложные случаи зацикливания, мы сможем расширить класс правильно разрешаемых случаев. Но всегда будут оставаться зацикливающиеся алгоритмы, на анализе которых разрешающий алгоритм тоже зациклится (хотя по правилам "не должен"). Очевидно, что при таком подходе, как бы мы ни наращивали сложность разрешающего алгоритма, на анализе собственного кода он всё равно зациклится.

[manul91]

epros в сообщении #1513772 писал(а):

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

Это понятно

epros в сообщении #1513772 писал(а):

Почему бы и нет? Очевидно, что некие простые случаи зацикливания посредством автоматического анализа кода обнаружить вполне можно. Путём добавления кода, анализирующего более сложные случаи зацикливания, мы сможем расширить класс правильно разрешаемых случаев.

Беспокоит например то, что похожим образом "в лоб" можно ввести только частичный порядок "хорошести".
Например, для двух "частично разрешающих" алгоритмов $A_1$ и $A_2$; если $A_1$ правильно решает вопроса остановки на подмножества $G_{A_1}$ программ (из всех программ $G$) и лажает на остальных; а $A_2$ правильно решает вопроса остановки на подмножества $G_{A_2}$ (из всех программ $G$) - и если при этом $G_{A_1} \subset G_{A_2}$ - то ясно что можно говорить, что $A_2$ является "лучшим разрешателем останова" чем $A_1$.
Но что если $G_{A_1} \not\subset G_{A_2}$, а например они только как-то пересекаются (или даже, вообще не имеют общих программ-элементов)? Тогда $A_1$ и $A_2$ не удастся просто сравнить; неизвестно кто "лучше" ("сравнить мощности" $G_{A_1}$ и $G_{A_2}$ может оказаться невозможным - если обе счетной мощности).

-- 10.04.2021, 18:04 --

arseniiv в сообщении #1513760 писал(а):

Диэдр во сне сказал. В общем не помню, но картина мира согласованнее с этим. Если бы гёделевское утверждение было таким особенным, это должно было бы давать кучу фантастических следствий, которых я не вижу и в данный момент ясно не представлю в голове, но кто-нибудь наверно даст ссылку на рассмотрение свойств множества всех недоказуемых утверждений для теории достаточной силы.

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

[epros]

manul91 в сообщении #1513776 писал(а):

Беспокоит например то, что похожим образом "в лоб" можно ввести только частичный порядок "хорошести".
Например, для двух "частично разрешающих" алгоритмов $A_1$ и $A_2$; если $A_1$ правильно решает вопроса остановки на подмножества $G_{A_1}$ программ (из всех программ $G$) и лажает на остальных; а $A_2$ правильно решает вопроса остановки на подмножества $G_{A_2}$ (из всех программ $G$) - и если при этом $G_{A_1} \subset G_{A_2}$ - то ясно что можно говорить, что $A_2$ является "лучшим разрешателем останова" чем $A_1$.
Но что если $G_{A_1} \not\subset G_{A_2}$, а например они только как-то пересекаются (или даже, вообще не имеют общих программ-элементов)? Тогда $A_1$ и $A_2$ не удастся просто сравнить; неизвестно кто "лучше" ("сравнить мощности" $G_{A_1}$ и $G_{A_2}$ может оказаться невозможным - если обе счетной мощности).

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

О, сорри, без Оракулов не обойдётся уже арифметическая иерархия. См. Turing reduction.

-- Сб апр 10, 2021 18:53:09 --

Хм. А может правильнее будет смотреть в направлении Ordinal analysis. Там суть в том, что "сила" каждой формальной теории характеризуется неким счётным ординалом. Если считать, что "частично разрешающий" алгоритм реализует проверку "зацикливаемости" в соответствии с некоторой аксиоматикой, то эти алгоритмы можно сравнить по соответствующим ординалам.

[Someone]

manul91 в сообщении #1513709 писал(а):

arseniiv в сообщении #1513706 писал(а):

arseniiv в сообщении #1513706 писал(а):

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

Если не помните, откуда знаете что не единственный? Мне кажется, он по сути единственный (если возможны вариации - то только косметические, не меняющие "суть" - иначе как придем к противоречию?

О какой конкретно теории идёт речь? Если, например, о теории множеств ZFC или NBG, то там таких неразрешимых (и очень интересных для теории множеств и топологии) утверждений полно. Если же говорить об арифметике Пеано, то в ней тоже есть вполне содержательные с человеческой точки зрения утверждения, которые невозможно ни доказать, ни опровергнуть средствами арифметики Пеано. Наиболее известным примером является, видимо, теорема Гудстейна. Другим аналогичным примером является усиленная финитная теорема Рамсея. Есть ещё какие-то примеры, но, поскольку это не моя область, я не знаю деталей. Ссылки можно найти в англоязычной википедии.
Кстати, теорема Гудстейна даёт пример общерекурсивной функции, общерекурсивность которой нельзя доказать средствами арифметики Пеано. В теории множеств (ZFC или NBG) теорема Гудстейна доказывается.

[arseniiv]

epros в сообщении #1513768 писал(а):

По-моему, любая фундаментальная последовательность рациональных чисел "куда-нибудь" да сходится.

Сходится-то сходится, разумеется, но мы не знаем насколько быстро, потому те «неотдекорированные» фундаментальные последовательности не дают некоторых хороших результатов.

manul91 в сообщении #1513776 писал(а):

Само построение геделевского утверждения (как кстати, и "опровергающего примера" для универсального разрешателя проблема остановки) - уже по факту своего способа построения определяет какой-то "класс" недоказуемых утверждений (программ на которых "разрешатель" будет лажать) относно данной теории (разрешателя остановки $A$).
Казалось бы, обозвать весь этот класс утверждений (исследуемых программ) "хитрыми" относно теории (разрешателя остановки $A$) - доказуемости (правильности работы) над этим классом не требовать - а для "всех остальных" - требовать - и вуаля, получаем определение "теории настолько полной насколько можно" (то же для разрешателя остановки).

В общем я просто ещё раз повторю, что на этом пути ничего полезного не нашли.

manul91 в сообщении #1513776 писал(а):

Для определенности, можно еще ограничиться размером кода $A$

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

[manul91]

Someone в сообщении #1513818 писал(а):

Кстати, теорема Гудстейна даёт пример общерекурсивной функции, общерекурсивность которой нельзя доказать средствами арифметики Пеано

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

Someone в сообщении #1513818 писал(а):

О какой конкретно теории идёт речь? Если, например, о теории множеств ZFC или NBG, то там таких неразрешимых (и очень интересных для теории множеств и топологии) утверждений полно.

Про "любой" (достаточно мощной/выразительной, чтобы в ней можно было бы сформулировать утверждения типа геделевских)... Существуют ли недоказуемые утверждения (средствами теории Х) для которых точно известно (доказано), что они НЕ сводятся (не эквивалентны, не являются "кодировками" каким-нибудь способом) непротиворечивости теории Х?
-- 11.04.2021, 03:04 --

manul91 в сообщении #1513822 писал(а):

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

Если ищется ущербность, то мы например можем кодировать чисел унарно, соответным количеством черточек.
Но мы же наоборот - ищем оптимальность; зачем вообще учитывать заведомо неудачных алгоритмических кодировок которые при переводе "раздуваются ассимптотически экспоненциально"?

[home-mik]

У меня тут глупый вопрос возник по теме: вычислимость функции ведь не должна зависеть от того, дождались мы ответа от алгоритма ее вычисляющего останова и результата или нет.

Просто по определению того же Шеня:

Цитата:

Функция $f$ с натуральными аргументами и значениями называется вычислимой, если существует алгоритм, ее вычисляющий, то есть такой алгоритм $A$, что

1) если $f(n)$ определено для некоторого натурального $n$, то алгоритм $A$ останавливается на входе $n$ и печатает $f(n)$;

2) если $f(n)$ не определено, то алгоритм $A$ не останавливается на входе $n$

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

[epros]

manul91 в сообщении #1513822 писал(а):

Существуют ли недоказуемые утверждения (средствами теории Х) для которых точно известно (доказано), что они НЕ сводятся (не эквивалентны, не являются "кодировками" каким-нибудь способом) непротиворечивости теории Х?

Конечно. Есть недоказуемые в теории X утверждения, которые сильнее утверждения о непротиворечивости теории X. Например, упомянутая теорема Гудстейна недоказуема не только в арифметике Пеано, но и в примитивно рекурсивной арифметике. Но утверждение о непротиворечивости примитивно рекурсивной арифметики слабее теоремы Гудстейна, в том смысле, что из него теорема Гудстейна не следует.

По этому поводу советую посмотреть упомянутую выше статью про Ordinal analysis.

home-mik в сообщении #1513835 писал(а):

У меня тут глупый вопрос возник по теме: вычислимость функции ведь не должна зависеть от того, дождались мы ответа от алгоритма ее вычисляющего останова и результата или нет.

Разумеется.

home-mik в сообщении #1513835 писал(а):

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

Общего способа установить справедливость пункта 2 не существует. Чтобы установить справедливость пункта 1 нужно дождаться останова алгоритма.

-- Вс апр 11, 2021 10:56:52 --

arseniiv в сообщении #1513819 писал(а):

Сходится-то сходится, разумеется, но мы не знаем насколько быстро, потому те «неотдекорированные» фундаментальные последовательности не дают некоторых хороших результатов.

Ну, можно придумать примеры, когда фундаментальная последовательность сходится настолько плохо, что оказывается трудно доказать её фундаментальность. Но ведь если мы знаем, что последовательность фундаментальная, то знаем, что она сходится.

[home-mik]

epros в сообщении #1513842 писал(а):

manul91 в
[quote="home-mik в сообщении #1513835 писал(а):

У меня тут глупый вопрос возник по теме: вычислимость функции ведь не должна зависеть от того, дождались мы ответа от алгоритма ее вычисляющего останова и результата или нет.

Разумеется.

Хорошо. Тогда такой пример:
$f(n) = \begin{cases} 1,&\text{если $x^n + y^n = z^n$ разрешимо в целых числах;}\\ 0,&\text{в противном случае.} \end{cases}$
Допустим, мы не знаем про доказательство теоремы Ферма. Тогда функция $f(n)$ вычислима, но не определена для $n > 2$, я правильно понимаю?

[epros]

home-mik в сообщении #1513871 писал(а):

Допустим, мы не знаем про доказательство теоремы Ферма. Тогда функция $f(n)$ вычислима, но не определена для $n > 2$, я правильно понимаю?

Вычислимость и определённость функции не зависит от нашего знания. Но значения функции мы имеем право не знать.

[arseniiv]

manul91 в сообщении #1513822 писал(а):

Но мы же наоборот - ищем оптимальность; зачем вообще учитывать заведомо неудачных алгоритмических кодировок которые при переводе "раздуваются ассимптотически экспоненциально"?

Нет, вы не поняли, я не про кодировки формул, а про различные формализмы вычислимости. В каждом из них в конечном счёте алгоритм является строкой над каким-то более-менее натурально определяемом алфавите (а $\mathbb N$ — это естественным образом $\{1\}^*$, помянутая вами унарная запись), и сами формализмы сами по себе не плохи и не хороши. Одни может быть позволяют выразить что-то одно компактнее, другие другое. И переводы между ними могут оказываться сложными безотносительно к тому, «неэффективный» формализм или нет.

А говоря об отбрасывании неэффективных чего-нибудь, вы забываете, что полно случаев, когда эффективность не ограничена сверху. Например вы очень кстати упомянули унарную кодировку натуральных чисел: известно, что если мы ограничиваемся одним и тем же алфавитом, типа $\{0, 1\}$, и ищем префиксный и «монотонный»* код для записи произаольных натуральных чисел, то мы не найдём оптимального, если нас не интересуют достаточно маленькие числа; см. ну хотя бы ту же статью Кнута, как она там называлась, где в начале он отвлекался на мириады, а потом стал заниматься уже кодированием.

* Если $n_1 < n_2$, то $\text{код}(n_1) < \text{код}(n_2)$, где порядок на строках естественный, лексикографический.

epros в сообщении #1513842 писал(а):

Но ведь если мы знаем, что последовательность фундаментальная, то знаем, что она сходится.

Это разумеется, но в конструктивном анализе нужно вроде гораздо больше, чтобы каша сварилась повкуснее. Someone рекомендовал в разных темах какую-то конкретную книгу по конструктивному анализу, где разбирались те три или четыре варианта конструктивных вещественных чисел, и утверждения там делаются часто, кажется, для двух самых приятных видов (из рассматриваемых). Не помню её автора.

home-mik
Учитывайте, что когда мы используем классическую логику, и с помощью неё рассматриваем конструктивные ээ… конструкции, то мы обязательно будем натыкаться на беспокоящие вас (кажется) случаи типа «я не знаю, но оно есть», ведь классическая логика совершенно не против такого, но не во всех областях это так заметно. Их можно избежать, если сразу погрузиться в конструктивный/интуиционистский контекст (это значит, в частности, что для выводов о вещах нам достаточно только тех из них, которые мы можем явно построить; NB это не обязательно влечёт то, что других вещей нет, хотя поначалу можно думать и так) и перестать использовать классическую логику (не навсегда, конечно) и в нём уже рассматривать эти вещи, хотя там тоже что-то будет. Но с куда более разумно выглядящими аргументами.

[home-mik]

epros в сообщении #1513872 писал(а):

home-mik в сообщении #1513871 писал(а):

Допустим, мы не знаем про доказательство теоремы Ферма. Тогда функция $f(n)$ вычислима, но не определена для $n > 2$, я правильно понимаю?

Вычислимость и определённость функции не зависит от нашего знания. Но значения функции мы имеем право не знать.

Но как тогда объективно, т.е. независимо от нашего знания, установить, определена функция на данном аргументе или нет?

Взять хотя бы то же определение вычислимой функции Шеня. Там в каждом пункте - "если функция определена/не определена для аргумента". Если попробовать подставить в это определение ту же функцию Busy Beaver $BB(n)$, то непонятно даже как подставлять: ее подсчитали для $N = 1,2,3,4$, даже алгоритм общий есть - перебирать все возможные машины Тьюринга и отбирать из них ту, которая дальше зайдет. Эти четыре значения по сути так и подсчитали.

А дальше, для $N > 4$ значений никто не знает. И какой вывод? Она там, дальше не определена или невычислима? Никто же не мешает и дальше использовать алгоритм перебора всех машин Тьюринга и сидеть неопределенно долго в ожидание значений для $N > 4$.

-- 11.04.2021, 19:26 --

arseniiv в сообщении #1513898 писал(а):

home-mik
Учитывайте, что когда мы используем классическую логику, и с помощью неё рассматриваем конструктивные ээ… конструкции, то мы обязательно будем натыкаться на беспокоящие вас (кажется) случаи типа «я не знаю, но оно есть», ведь классическая логика совершенно не против такого, но не во всех областях это так заметно. Их можно избежать, если сразу погрузиться в конструктивный/интуиционистский контекст (это значит, в частности, что для выводов о вещах нам достаточно только тех из них, которые мы можем явно построить; NB это не обязательно влечёт то, что других вещей нет, хотя поначалу можно думать и так) и перестать использовать классическую логику (не навсегда, конечно) и в нём уже рассматривать эти вещи, хотя там тоже что-то будет. Но с куда более разумно выглядящими аргументами.

Я как-то "заходил" к конструктивным математикам, ужаснулся, и вышел - читал статьи Маркова. В общем понял я еще меньше, чем в классической, поэтому решил придерживаться последней. Хотя поначалу да, у меня как у программиста, прикладника надежды на конструктивизм были большие.

[arseniiv]

home-mik в сообщении #1513902 писал(а):

Но как тогда объективно, т.е. независимо от нашего знания, установить, определена функция на данном аргументе или нет?

В общем случае никак. Привет от классической логики и несчётных множеств.

home-mik в сообщении #1513902 писал(а):

читал статьи Маркова

Можно почитать что-то из области теории типов. Там может быть понятнее (или наоборот, кому как). В каждой теории типов у нас вместо конструктивных объектов разные термы, каждый из которых имеет свой тип; высказываниям соответствуют тоже типы, элементы которых понимаются как всевозможные доказательства такого высказывания (когда их нет, тип пустой, и в непротиворечивой теории один специальный тип 0 (или он вводится аксиоматически, или он может быть выразим как например $\Lambda t. \; t$ в System F и других теориях с полиморфизмом) пустой по построению).

Когда начинают строить конструктивные вещественные числа и что-то такое, то это приводит к некоторым сложностям, потому что это очень непохоже на прикладные численные методы, так как у них совершенно разные цели — численным методам почти всегда плевать на абсолютную точность представления, они сразу довольствуются конечной, хотя может быть заранее и не ограниченной, и интересуются приближением к классическим результатам. Изучение конструктивных оснований же интересуется построением как можно большего куска математики, используя только тот или иной репертуар средств, принятых конструктивными (есть несколько разных, например одни включают принцип Маркова и другие стараются его не использовать — тут ничего особенного, подобная же ситуация есть с аксиомой выбора). То есть книги по «конструктивизму вообще» — примерно того же рода, что книги по теории множеств и построению обычных классических вещественных чисел на их основе — такие же детальные и во многих ситуациях не те, которые стоило бы почитать.

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