Pull to refresh
5
0
Send message
Да, конечно.

1. Заметим, что если умеем решать проблему остановки на пустом входе, то умеем решать на любом входе. В самом деле: пусть мы хотим узнать останавливается ли А на входе х. Рассмотрим композицию двух алгоритмов — один берет пустой вход и выдает х, а второй наш алгоритм А (который читает выход первого алгоритма и выдает то, что считает нужным выдать). Это композиция останавливается тогда и только тогда, когда останавливается А на входе х.
2. Построим диагональную всюду определенную функцию. f(A) = 1, если A не останавливается на входе А и f(A) = A(A) + 1, если останавливается.
Это какая-то вычислимая функция (если проблема остановки разрешима). Посмотрим на f(f) — это какое-то значение (так как функция всюду определенная), но если f(f) определено, то f(f) = f(f) + 1, а так не бывает.
У теоремы Геделя есть и семантическая версия: для любой эффективной аксиоматизации натуральных чисел есть формула, истинная в стандартной модели натуральных чисел, но не выводимая в этой аксиоматизации.
А так как мы получили самоотрицающее выражение, то доказали, что приведённые выше 3 утверждения противоречивы и требуют корректировки.


Мы же вот здесь договорились, что после замены на 11 все стало хорошо и ни одно из утверждений не является рефлексивным (а значит все три истины): habr.com/en/post/512518/?reply_to=21899626#comment_21899464

«Если 2 + 2 = 4, то среди утверждений длины не более 11 слов есть истинные» (16 слов, не саморефлексия).


Ну и, очевидно, это ложь, так как из одного не следует другого.


Это, очевидно, не ложь. Для того, чтобы импликация была ложью, необходимо, чтобы посылка была истина а следствие ложью. Максимум мы можем сказать, что это выражение целиком не имеет смысла (семантически некорректно), но уже не понятно почему — оно про себя точно ничего не утверждает.

Утверждение «если 2+2 = 4, то 3+3 = 6» — тоже истинное.
И даже «если 2+2 = 5, то 3+3 = 6» истина.
Да, хорошо, напишем 11.

Тогда у нас есть:
1. «Среди утверждений длинны не более 5 слов есть истинные.»
2. «Множество утверждений длины не более 5 слов является подмножеством множества утверждений длины не более 11 слов.»
3. «Если истинное утверждение содержится в подмножестве некоторого множества, то истинное утверждение содержится и в самом множестве.»

И все три мы считаем истинными.
Но тогда синтаксически (см. «modus ponens» или «силлогизм», что ближе) мы должны согласиться и с утверждением, которое из них троих следует:
«Среди утверждений длины не более 11 слов есть истинные.»

Я тут подумал, что можно даже проще получить то же самое:
1. «2 + 2 = 4»
2. «Если 2 + 2 = 4, то среди утверждений длины не более 11 слов есть истинные» (16 слов, не саморефлексия).
Каким образом первое самореферентное?
Оно само длинное, а утверждает что-то только про короткие утверждения.

Каким образом второе самореферентное?
Оно вообще про конкретные множества, а не про само утверждение или свою истинность. Или смущает, что оно само входит во второе из множеств, о которых утверждает? Давайте заменим 1000 на 11. Тогда оно уже слишком длинное, чтобы входить в него.

Откуда саморферентность в третьем? Оно опять про какие-то множества и подмножества и общее определение истинности.
То есть мы не признаем оригинальное утверждение истинным?

Тогда у нас есть проблема.
Рассмотрим следующие три утверждения:
1. «Среди утверждений длинны не более 5 слов есть истинные.»
2. «Множество утверждений длины не более 5 слов является подмножеством множества утверждений длины не более 1000 слов.»
3. «Если истинное утверждение содержится в подмножестве некоторого множества, то истинное утверждение содержится и в самом множестве.»

Какое из трех не является истинным?

Если мы все три объявляем истинными, то мы обязаны объявить истинным и утверждение «среди утверждений длинны не более 1000 слов есть истинные» (это просто синтаксическое следствие предыдущих трех).
Так не работает.

Давайте начнем с чего-нибудь простого: «утверждение 2+2 = 4 — истино» — это семантически корректное утверждение или нет?

А утверждение «среди утверждений длинны не более 5 слов есть ложные»?
Или утверждение «среди утверждений длинны не более 1000 слов есть истинные»

Прошу обратить внимание, что последнее утверждение — оно не выглядит саморефлексией, но, неожиданно, может рассматриваться как самоподтверждение.
Если система достаточно богатая, то это можно сформулировать формально.

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

Например, натуральные числа только с нулем и операцией +1, если я правильно помню, ровно такие.
Проблема не в том, что условие выходит за рамки системы.

Наоборот, для достаточно богатой системы утверждение «это система непротиворечива» можно сформулировать внутри системы. И вторая теорема Геделя о неполноте как раз о том, что вот это самое утверждение либо недоказуемо, либо ложно.
Есть такое объяснение (не совпадающее с оригинальным, если где-то нужно чуть подробнее описать — не стесняйтесь):
1. Задача остановки не разрешима. То есть нету алгоритма, который берет на вход описание алгоритма и отвечает на вопрос остановится он на пустом входе или нет. В самом деле, если бы такой алгоритм существовал, то можно было бы построить «диагональную» функцию, которая с i-ой отличается на входе i.
2. Утверждение «алгоритм останавливается» формализуется в любой достаточно богатой системе (и это самая технически сложная часть, если использовать «минимальный необходимый» формализм, но если взять чуть более богатый, чем необходимый минимум, то это довольно просто).
3. Если есть перечислимая система аксиом, в которой были бы доказуемы все истинные утверждения этой модели, то проблема останова была бы разрешима. В самом деле — либо «эта программа останавливается на пустом входе», либо «эта программа не останавливается на пустом входе» — истинное утверждение. Если для любой программы доказуемо ровно одно из них — мы решили проблему остановки.

PS forany.xyz/a-227 — еще один достаточно хороший материал, лекция для старших школьников (кроме другой ссылки на Успенского, которую я дал ниже по дискуссии)
Не столько основанная, сколько содержащая.
Есть очень хорошее объяснение (почти на пальцах) от В.А. Успенского почему теорема Геделя о неполноте — это следствие неразрешимости проблемы остановки: www.mathnet.ru/links/81edd102bbff2a65a53c6dd27f387678/rm4322.pdf

Если упустить технические детали (в статье они есть), то идея примерно такая: если язык достаточно богатый (а стандартная арифметика — богатая), то можно сформулировать утверждение «алгоритм (в статье используется ассоциативное исчисление, но можно абсолютно так же использовать, например, машины Тьюринга) за один шаг может перейти из состояния А в состояние B.»

После этого можно сформулировать утверждение «Машина Тьюринга может (за несколько шагов) дойти до заключительного состояния (=остановиться), начиная с состояния А» (В этом месте появляется квантор по логу исполнения).

Ну и, наконец, осталось заметить, что если бы все истинные утверждения были бы доказуемы, то проблема остановки была бы разрешима — достаточно просто подождать, пока появится доказательство остановки или доказательство отрицания остановки.

А вот алгоритмическая неразрешимость проблема остановки — это уже диагональный метод в чистом виде.
На примере чуть выше habr.com/en/post/512494/#comment_21888832 — видно, что она добавляет много деталей реализации, которых не было в постановке.
В описании не было ничего про переменную balance внутри state, например.

Ту же самую функциональность можно получить, например, заменив balance на my_balance. Соответствие высокоуровневой спецификации останется, а значит какой-то выбор сеть делает. При этом консистентный по всему коду.
Согласен, переменные строго динамически типизированные.
А вот функции — уже не строго типизированные (на чем и игра в этом примере).
Ну не совсем.

Пока в nums нет дупликатов и found — это просто про умножение (а не про, например, взятие по модулю) это свойство (не больше одного совпадения во внутреннем цикле) не зависит от констант (и их можно произвольно менять).

Но да, если оставлять так, то нужно внимательно следить за условием (для произвольного условия good(num, i, 25) этот код не подходит).
Формально, можно и так оставить: может быть не больше одного совпадения во внутреннем цикле, а после первого внутреннего цикла, изменившего значение, нас выкинет из внешнего.

Что не отменяет того, что так писать, конечно, не стоит.
Так концептуально не получится — питон же не строго типизированный.
Например следующую функцию перенести в язык, где нету option/maybe (в каком-нибудь виде) невозможно по концептуальным причинам.
def f (x):
     if x > 2:
         return x
     else:
         return None
Для любой пары упорядоченных типов, пара состоящая из них, — тоже упорядочена.

Например: (1, 10) < (2, 5) < (2, 7)
play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=10eceaf01064d7be6f37194093bf93d2
Дело не в stable_sort, можно вызывать ustable, ничего не изменится в результате.

Фокус в вот этой имплементации: doc.rust-lang.org/std/cmp/trait.Ord.html#impl-Ord-61
Если есть порядок на первом и втором элементе пары, то появляется порядок на парах (по которому я и сортирую).

Information

Rating
10,007-th
Registered
Activity