dmitgu

5.1. Язык LS, пункты 1-5.

к Оглавлению

Теперь осталось на базе языка LA из класса сложности NF построить язык LS из класса NP и доказать на его примере неравенство NP ≠ P по аналогии с доказательством неравенства NF ≠ F.

Слова для языка LS имеют вид:

t, S, s

Части слова должны иметь определённое содержание, иначе слово отвергается сразу и не принадлежит языку LA как не корректное. В корректном случае содержание этих частей такое:

1.1. Часть t – как и в языке LA – это утверждение, для которого требуется наличие логического доказательства и соблюдение некоторых условий, изложенных далее, чтобы слово принадлежало языку.

По сравнению с языком LA у слова языка LS появились 2 новые части.

1.2. S (заглавная) – параметр числовой длины доказательства, записанный в позиционном (десятичном, например) виде;

1.3. s (прописная) – параметр строковой длины доказательства,, размер |s| которого равен S, состоящий только из символов «1». Например, для S = 10 корректным будет s = «1111111111». В данном случае для обозначения использована прописная буква потому, что в программировании подобные строковые аргументы и функции часто начинаются с прописной буквы «s». 

Логическое доказательство для утверждения t может быть признано доказательством в смысле языка LS лишь в том случае, если предельный (максимальный) размер сертификата, частью которого является доказательство, не превышает полиномиального ограничения от размера |s| и этот предел равен (условимся) q_S(|s|), что равно q_S(S) при корректном слове. 

Соотношение q_S(|s|) делает наш язык принадлежащим классу NP, так как помимо полиномиально быстрого относительно размера своих аргументов алгоритма проверки (рассмотренного далее) есть и полиномиальное ограничение размера сертификата относительно размера слова. 

1.4. Наличие двух параметров для длины доказательства в слове связано с двумя ограничивающими алгоритмами на время работы алгоритма проверки – для обычных и «специальных» случаев, которые будут построены на базе теоремы о неопределимости – подобно тому, как это было сделано в языке LA. 

«Специальными» утверждениями – если сравнивать с 1-й прикладной ролью языка LA – в языке LS будут уже не утверждения вида AntiSol, а утверждения вида AntiSol_S, так как данное утверждение будет особым уже не в отношении алгоритма-решения Sol(…), но в отношении одновременно алгоритма-решения Sol(…, …, …) и параметра числовой длины доказательства S. 

2. Про сертификаты для 1-ой прикладной роли языка LS можно сказать всё то же самое, что было сказано про сертификаты в начале раздела «Язык логики LA». Перенесём сюда вид сертификата:

a, y

и уточним, что алгоритм-решение, программный код которого представлен частью a сертификата имеет теперь вид Sol(…, …, …), так как алгоритм-решение в обычном случае зависит от аргументов таким образом: Sol(t, S, s). 

Алгоритм проверки:

Ls(t, S, a, s, y) – работает как Lc(t, y), за исключением того, что: 

3.1. В начале работы он проверяет аргументы t, S, a на совпадение с шаблоном:

«AntiSol_S», S, «Sol(…, …, …)»

и если совпадение выявлено, то возвращает 0. Ниже поясню нюансы;

3.2. После 1-го этапа проверяет соответствие между S, s, y. Если соответствия нет, то возвращает 0. А соответствия нет в случаях: Аргумент s состоит не только из символов «1»; И/или его длина не равна числу S; И/или размер |a| + |y| превышает полином 1000*S^n, например, где n – фиксированное натуральное число);

Кстати, из пункта 1.3 получается в этом случае, что q_S(|s|) = 1000*S^n; 

3.3. После 2-го этапа проверяет, чтобы аргумент a соответствовал шаблону: либо «-», либо «Sol(…, …, …)». Если не соответствует, то возвращает 0;

3.4. После этапов 1-3 – если они не закончили работу – переходит к исполнению Lc(t, y) и возвращает то, что вернёт Lc(t, y);

Пояснение к пункту 3.1:

Очень важно исполнить этот этап до обращения к потенциально огромным аргументам s и y. Дело в том, что утверждение «AntiSol_S» строится на базе того опровергающего алгоритма ContrSol(S), который с «правильным» аргументом s, соответствующим алгоритму S, запускает алгоритм:

Sol(«AntiSol_S», S, s), где s = ss(S).

И – важное замечание! – потенциально огромная строка s вовсе не генерируется перед запуском данного алгоритма. Ведь этот запуск – лишь эмуляция работы данного алгоритма и при обращении к любому символу строки s наш опровергающий алгоритм ContrSol(S), который эмулирует работу данного алгоритма, возвращает «1» запущенному внутри него алгоритму. И длина строки s в этой эмуляции работы алгоритма имеет длину S. То есть, работа запущенного алгоритма ничем не отличается от случая, в котором у данного алгоритма есть корректный и готовый аргумент s. Но при этом генерировать данную строку не приходится. 

Поэтому количество шагов, которое сделает алгоритм ContrSol(S), никак не зависит от длины строки s, а зависит (полиномиально) от времени работы запущенного алгоритма (запущенного при как бы уже готовом аргументе s) , зависит (полиномиально) от размера алгоритма |Sol(…, …, …)| и от размера аргумента |S|. 

И если этот запущенный алгоритм остановится с каким-то результатом, то опровергающий алгоритм ContrSol(S) выдаст то, что «условно» опровергнет результат работы запущенного алгоритма.

А опровергнет «условно» только потому, что есть ограничения на размер доказательства, а без такого ограничения опровержение было бы буквальным, а именно:

4.1. Если результат будет Sol(«AntiSol_S», S, ss(S)) = 1, то опровергающий алгоритм вернёт 0, что будет соответствовать отрицанию «AntiSol_S» и в этом случае опровержение – буквальное (а не условное) и не зависит от размеров доказательства, так как подходящего доказательства нет вообще.

4.2. Если результат будет Sol(«AntiSol_S», S, ss(S)) = 0, то опровергающий алгоритм вернёт 1, что будет соответствовать утверждению «AntiSol_S» и в этом случае работа алгоритма Sol(«AntiSol_S», S, s) = 0 будет опровергнута только тогда, когда результат работы опровергающего алгоритма (который действительно имеет место быть) можно доказать доказательством длиной до q_S(S) - |a|. То есть – доказательство состоявшегося факта работы алгоритма заведомо есть, но вопрос только в том, чтобы оно было не слишком длинное.

Но в любом случае алгоритм Sol(«AntiSol_S», S, …) не может подтвердить доказуемость «AntiSol_S» и об этом сообщает алгоритм проверки

Ls(«AntiSol_S», S, «Sol(…, …, …)», …, …) = 0

4.3. При этом не имеет значения, какие там аргументы s и y – потому что недоказуемость имеет место быть даже при корректных значениях s и y, а при некорректных значениях – проверка заведомо даст негативный результат. 

И этот результат получается очень быстро – неполиномиально быстро относительно размеров аргументов |s| и |y|, потому что от них данный результат зависит не больше, чем зависит размер |S| от размера правильного (соответствующего числу S) |s|, а это неполиномиально малая (логарифмическая) зависимость.

Построенный алгоритм Ls(t, S, a, s, y) для языка LS со словами вида:

t, S, s 

будем считать первой прикладной ролью языка LS и за счёт этого мы можем отнести язык LS к классу NP. Действительно, алгоритм Ls(t, S, a, s, y) работает в пределах полиномиального количества шагов относительно размера своих аргументов и размер сертификата (доказательства) полиномиально ограничен относительно размера слова, так как |y| ≤ q_S(|s|) - |a|.

5.1. А как же получается, что для слова типа t, S, s при утверждении t = «AntiSol_S» и сертификате a = «Sol(… , … , …)» проверка работает неполиномиально быстро относительно размера слова? 

Ответ будет неожиданным для «классического» подхода. Проверка, когда она работает неполиномиально быстро в сравнении с «обычной» скоростью, работает вовсе не для слова

t, S, s при утверждении t = «AntiSol_S» 

и сертификате

a = «Sol(… , … , …)», y,

а для слова:

t, S, a при утверждении t = «AntiSol_S» и a = «Sol(… , … , …)» 

и сертификатах

s, y. 

5.2. Дело ведь не в том, каким образом мы выбрали аргументы и в каком порядке расставили их, разделив запятыми. Дело в логике работы алгоритма проверки – он может брать 5 кусков из 1-го аргумента и использовать их как сертификат, а остальное из первого аргумента использовать как слово, добавив к нему ещё частей из второго аргумента. Я для удобства разбил информацию, получаемую алгоритмом проверки на те аргументы, которые написаны. 

Но даже по смыслу у нас алгоритм проверки описывает 2 языка. Первый – язык логики Пеано (с ограничениями на размер доказательств), второй – язык доказуемости утверждения не просто в логике Пеано (с ограничениями на размер доказательств), но в логике, сокращённой на некоторые заведомо недоступные доказательства для данного алгоритма-решения. 

Можно считать эти 2 языка одним: Где в «первой части» решается вопрос о доказуемости данного утверждения доказательствами допустимого размера «вообще». А во «второй части» – о доказуемости данного утверждения с учётом (помимо размера доказательств) некоторых ограниченных возможностей у заданного алгоритма-решения. 

Если для «первой» части у нас такие слово и сертификат из её первой роли:

Слово вида 1: t, S, s; Сертификат вида 1: a, y,

То для «второй части» языка у нас такие слово и сертифика из её первой роли:

Слово вида 2: t, S, a, s; Сертификат вида 2: y.

Но даже это отличается от того, что было выше при утверждении t = «AntiSol_S» и a = «Sol(… , … , …)»:

Слово спец. вида: t, S, a; Сертификат спец. вида: s, y.

5.3. Да, отличается, но слово в последнем варианте и не принадлежит языку LS, как не принадлежит ему и никакое другое слово вида 2 при утверждении t = «AntiSol_S» и a = «Sol(… , … , …)»:

Слово вида 2: t, S, a, s; Сертификат вида 2: y. 

Почему же в «слове спец. вида» часть s «перепрыгнула» в «сертификат спец. вида»? Потому что она даже не рассматривается алгоритмом проверки в данном специальном случае – 

при t = «AntiSol_S» и a = «Sol(… , … , …)». Слово оказывается отвергнутым алгоритмом проверки без рассмотрения аргументов s, y. 

А что при «классическом» подходе к алгоритму проверки отвергается без рассмотрения? Избыточная часть слишком длинного сертификата. Вот с этой точки зрения часть s в данном случае и оказывается «слишком длинной частью сертификата» - вместе с y. 

И вообще – видна условность деления на «часть слова» и «часть сертификата». То, что является в обычном случае частью слова (речь о части s-малое) в специальном случае вообще не рассматривается алгоритмом проверки. И в специальном случае слово отвергается (без рассмотрения s в качестве его части) независимо от того – «корректный» ли s = ss(S) (это требование для корректности слова в обычном случае), либо часть s содержит вообще «не пойми что». С одной стороны, можно считать, что в специальном случае s – является частью слова, которая отвергается так же, как слишком длинный сертификат – без рассмотрения. А с другой стороны, можно считать, что являющийся в обычном случае частью слова s превращается в специальном случае из части слова в часть сертификата. Разницы как считать – нет, ведь часть s в специальном случае вообще не используется алгоритмом проверки.

5.4. Но, если про часть s можно решить в отношении возможной принадлежности к сертификату и так и эдак когда она не используется, то часть a заведомо используется и оказывается иногда частью слова, а иногда – сертификата. Но ведь аргументы у алгоритма-решения содержат именно информацию о слове, а не сертификате. Как же в этом случае быть с частью a? 

А никак. Часть a дана алгоритму-решению не в составе переданных ему аргументов, а в качестве его собственного программного кода. 

Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.