Проблема алгоритмической разрешимости и полуразрешимости  формальных систем и её решение

с использованием  квантового  генератора тестов

П.А. Правильщиков,
 в.н.с, к.т.н, с.н.с, pavelp@ipu.ru
ИПУ РАН, г. Москва

Показано, что одной из проблем теории алгоритмов является формальное доказательство алгоритмической разрешимости или неразрешимости задач. В случае логики первого порядка и, в частности, в случае исчисления высказывания для решения проблемы разрешимости или неразрешимости предложено использовать квантовые D-алго-ритмы (QD-алгоритмы), «заточенные» под архитектуру квантового ускорителя (КвУ). Вычислительной моделью такого ускорителя является не машина Тьюринга, а идеальный квантовый генератор тестов (КГТ). Приводится описание КГТ и описание квантовых D-алгоритмов. Утверждается, что с появлением квантовых компьютеров (КК), КвУ и QD-алгоритмов теория алгоритмов вынуждена стать ещё более междисциплинарной наукой, в основе которой лежат не только математика и computer science, но и линейная алгебра, и квантовая механика.

 

It is shown that one of problems of the theory of algorithms is the formal proof of algorithmic resolvability or unsolvability of problems. In a case of the first-order logic and, in particular, in case of propositional calculation for the decision of a problem of resolvability or unsolvability it is offered to use the quantum D-algorithms adapt to architecture of the quantum accelerator . Computing model of such accelerator is not Turing machine, but it is the ideal quantum tests generator (QTG). Description QTG and the description of quantum D-algorithms is resulted. Affirms that with the advent of quantum computers, quantum accelerator and quantum algorithms the theory of algorithms is compelled to become even more interdisciplinary science, in basis of which are not situated only mathematics and computer science, but also linear algebra and the quantum mechanics.

Введение

Известно, что теория алгоритмов является междисциплинарной наукой, которая находится на стыке математики и computer science и изучает общие свойства и закономерности алгоритмов. До появления КК и теории квантовых вычислений утверждалось, что теория алгоритмов вместе с математической логикой образует теоретическую основу вычислительных наук. Но в наше время происходит квантовая революция в вычислительной технике (ВТ). Поэтому можно утверждать, что теоретическую основу вычислительных наук образует не только математическая логика и
теория алгоритмов, но также линейная алгебра и квантовая механика. Следовательно, теория алгоритмов стала ещё более междисциплинарной наукой. Одной из задач теории алгоритмов является задача формального доказательства алгоритмической разрешимости или неразрешимости задач. Под алгоритмической разрешимостью понимается свойство формальной теории обладать алгоритмом, который по данной формуле определяет: выводима она из множества аксиом теории или нет, не выводима. Теория называется разрешимой, если такой алгоритм существует, и неразрешимой в противном случае. Вопрос о выводимости в формальной теории является частным, но вместе с  тем важнейшим случаем общей проблемы разрешимости. Метод решения проблемы разрешимости, представленный в форме алгоритма, называется разрешающей процедурой для этой проблемы. Проблема разрешимости, для которой существует разрешающая процедура, называется разрешимой.

Формальное исчисление, например, исчисление высказываний или D-исчисление [1] в общем случае должно определять язык, правила построения термов и формул, а также аксиомы и правила вывода. Таким образом, для каждой теоремы T, всегда можно построить цепочку A1, A2, … , An = T, где каждая формула Ai  либо является аксиомой, либо выводима из предыдущих формул, по одному из правил вывода. Алгоритмическая разрешимость означает, что существует алгоритм, который для каждого правильно построенного предложения T, за конечное время выдаёт однозначный ответ: да, данное предложение выводимо в рамках  исчисления или нет — оно не выводимо. Очевидно, что противоречивая теория разрешима, так как любая формула будет выводимой.  Алгоритмическая разрешимость — очень сильное свойство, и большинство используемых на практике теорий им не обладают. В связи с этим было введено более слабое понятие полуразрешимости. Полуразрешимость означает наличие алгоритма, который за конечное время всегда подтвердит, что предложение истинно, если это действительно так, но если нет — может работать бесконечно. По сути, это означает, что существует алгоритм, который может эффективно доказать истинность, а значит и вывести любую правильно построенною теорему в данной формальной теории. Но доказать истинность в некоторых случаях можно и не используя аналитический подход с выводом одной формулы из другой. Здесь мы будем использовать именно такой альтернативный подход к определению истинности T  без аналитического вывода. Тут уместно подчеркнуть, что эффективные полуразрешающие процедуры для логики первого порядка имеют большое теоретическое значение. В прикладном плане, например, в задачах формальной верификации БИС, в доказательстве корректности программ они позволяют автоматически доказывать формализованные утверждения очень широкого класса.

Потребность в построении полуразрешающих процедур и автоматическом доказательстве теорем особенно 
обострилась в последние 30-35 лет в теории и практике программирования в целях создания программ, к надёжности которых предъявляются повышенные требования, а также в теории и инженерной практике проектирования БИС [2-5]. Так, проблема формальной верификации проектов БИС состоит в доказательстве того, что разработанная схема комбинационного устройства (КУ), верно реализует записанное на некотором языке задание на проектирование схемы. Доказательство некоторых положений в науке вообще и теперь доказательство теорем уже в информационных технологиях и САПР, имеет большое значение, особенно в постиндустриальной технологии, основанной на знаниях, так как сама наука, если её рассматривать как знание ― это истина, взятая с её обоснованием [6]. Под обоснованием некоторого научного, в частности, математического положения (тезиса) обычно понимается некоторое доказательство. В самом широком смысле доказательство есть некоторое рассуждение, имеющее целью обосновать истинность (или ложность) какого-либо утверждения, которое называется тезисом. Суждения, на которые опирается доказательство и из которых логически следует тезис, называются аргументами  (осно­ваниями) доказательства. Корректное доказательство, т.е. доказательство, не содержащее ошибок и устанавливающее истинность тезиса, называют просто доказательством, а корректное доказательство, устанавливающее ложность тезиса, называется опровержением. Доказательство, содержащее ошибку, называют несостоятельным.

Впервые проблема автоматического доказательства теорем и в более широком контексте проблема разрешимости стала обсуждаться ещё в 60-х годах в литературе в области кибернетики. Тогда же наметились и подходы к автоматизации доказательства теорем. Одной из первых попыток осуществить автоматическое доказательство теорем является известная попытка А. Ньюэлла, Дж. Шоу  и  Г. Саймона использовать в этих целях созданную ими программу «Общий решатель задач» (GPS) [7]. Подход, использованный ими для доказательства теорем, состоит в доказательстве или опровержении формул исчисления высказываний вида:

,                                                           (1)

где f1(x1, x2, …, xn)  и  f2(x1, x2, …, xn) — сложные высказывания. Эти высказывания записаны в символическом виде с применением операций отрицание, конъюнкция, дизъюнкция и других. Идея подхода GPS, состоит в том, чтобы при доказательстве равенства (1), либо его опровержении, найти цепь элементарных преобразований формул. Такая
цепочка преобразований формулы f1(x1, x2, …, xn) преобразует её в f2(x1, x2, …, xn), или же f2 (x1, x2, …, xn) преобразует в f1(x1, x2, …, xn), либо приводит путем преобразований f1(x1, x2, …, xn)  и  f2 (x1, x2, …, xn) к одной и той же формуле f3(x1, x2, …, xn). Если программа GPS убеждается, что равен­ства достичь невозможно, то принимается утверждение:
                                      .                                (2)

По сути, выражение (2) является опровержением (1), то есть тезис теоремы не верен.

На каждом шаге преобразований (1) в процессе доказательства левая и правая части равенства сравниваются между собой. Если между ними нет различия, то теорема доказана. Если же различие есть, то выясняется его характер. Дальнейшие нюансы подхода к доказательству в программе GPS здесь опущены. Здесь важно лишь то, что этот
подход работает с аналитическим заданием логических функций в виде формул. Существенно и то, что при использовании этого подхода к доказательству теорем две функции в (1) считаются равными, если они при любых значениях входящих в них атомарных формул  одинаково  интерпретируются с точки зрения истинности и ложности.

Другой подход к доказательству теорем использует широко известное в математике доказательство по индукции. Такой подход применяется в целях автоматизации доказательства корректности некоторых программ [3]. Другие подходы используются в алгоритмах формальной верификации БИС [5], и хотя они более похожи на подход А. Ньюэлла, Дж. Шоу и Г. Саймона, хотя бы в постановке задачи автоматического доказательства теорем, они всё-таки сильно различаются. Теперь рассмотрим два таких высказывания: «Человек не может быть одно­временно лгуном и человеком, всегда говорящим правду» и «Че­ловек или не лгун, или не всегда говорит правду». Эти два высказывания являются примерами, известных доказуемых дополнений к знаменитому парадоксу лжеца: «Я лгу»[1]. Ин­туиция подсказывает нам, что два приведённых высказывания  одинаково интерпретируются с точки зрения истинно­сти и ложности. Но как доказать это?

1. Постановка задачи и обоснование подхода к её решению

Часто в подобной ситуации более удобно от словесных формулировок высказы­ваний, приведённых выше, перейти к их символической записи. Если x1 и x2 суть элементарные высказывания «Человек лгун» и «Человек всегда
говорит правду», то приведённое вы­ше сложное высказывание «Человек не может быть одно­временно лгуном и человеком, всегда говорящим правду» можно записать в виде логической формулы:

.                                                                                    (3)

Сложное высказывание «Че­ловек или не лгун, или не всегда говорит правду» состоит из двух атомарных высказываний x¢1 и x¢2 :  «Че­ловек не лгун» и «Человек не всегда говорит правду», что можно записать в виде формулы:

.                                                                                     (4)

Если в соответствии с (1) на основе нашей интуиции объединить формулы (3) и (4), то получим следующее выражение:

  .                                                                            (5)

Можно заметить, что выражение (5) представляет собой одну из формулировок теоремы Де Моргана[2], которую словесно можно записать в следующем виде.
     Теорема 1. Отрицание конъюнкции двух переменных, т.е. , равно дизъюнкции отрицаний тех же двух переменных, т.е. .

Проанализируем и докажем эту теорему с помощью такой модели вычислений как КГТ, который является теоретическим аналогом квантовых ускорителей (КвУ). КвУ «заточен» или «подогнан» под выполнение квантовых D-алгоритмов, выполняющих полный упорядоченный перебор ¾ см. [9-11]. Заметим, что подход, использующий
полный упорядоченный перебор, в последнее время часто называют «методом грубой силы» (в эвристическом
варианте хакеры используют этот метод для взлома паролей с помощью традиционных классических компьютеров[3]).

Однако использование полного упорядоченного перебора с помощью классических компьютеров (классических
суперкомпьютеров) или классических процессоров-ускорителей [5,9] требует либо экспоненциально большого времени, либо экспоненциально большого объёма ОП [7-11]. И только использование КК и КвУ позволит эффективно решать многие труднорешаемые задачи, в частности, проблему алгоритмической разрешимости или неразрешимости формальных систем с полиномиальным временем решения и полиномиальными объёмами ОП. Но для этого сначала мы должны свести решение проблемы разрешимости или неразрешимости к эффективному решению проблемы автоматического доказательства в рамках логики первого порядка, в частности, в рамках исчисления высказываний или булевой логики, что и было показано выше. После этого проблему решения автоматического доказательства теорем можно будет свести к эффективному решению логических уравнений [10-11]. См. также [12].
Сведение логических уравнений в целях доказательства теорем показано ниже. Важно повторить, что к проблеме алгоритмической разрешимости и автоматическому доказательству теорем сводятся не только теоретические проблемы математики и теории алгоритмов, но и многие прикладные, практически  значимые задачи, например, та же проблема верификации проектов БИС [4, 5].

Для доказательства теоремы 1, используя правила логики и операцию «равнозначность», которая будет обозначаться символом ««», выражение (5) можно переписать в виде булевых уравнений (6) и (7):

                        (6)
                                 (7)

Рис. 1. Логическая сеть комбинационного устройства, реализующая левую часть уравнения (6)

Использование D-алгоритмов для решения уравнений (6) и (7) позволяет найти набор Xi из n значений (в нашем случае n = 2  и искомый набор Xi  = ), на котором выполняются эти уравнения. Если с помощью D-алгорит-мов такой набор  Xi  не найден, то решения для (6) и (7) не существует. Если не существует набор Xi, при котором левая часть уравнения (6) равна 0, либо левая часть уравнения (7) равна 1, то теорема 1 будет доказана: выражение (5) будет выполняться. Подчеркнём, что рассматриваемые здесь QD-алгоритмы так же, как и классические D-алго-ритмы, являются полными, т.е. всегда найдут решение, если оно существует, и это строго доказано. В качестве примера для демонстрации доказательства методом грубой силы, т.е. с помощью QD-алгоритмов выберем уравнение (7). Этот выбор можно объяснить тем, что (7) представляет собой классическую формулировку проблемы выполнимости логических уравнений (SAT-проблемы). Далее, чтобы более наглядно продемонстрировать QD-алгоритмы в случае решения уравнения (7), представим его левую часть в виде КУ ¾ см. рис. 1. Следует также подготовить другие исходные данные, необходимые для доказательства путём выполнения QD-алгоритма. Эти исходные данные связаны со структурой КУ и, прежде всего с числом R рангов КУ. На рис. 1 показаны 3 ранга (R = 3). Следовательно, в соответствии с законом сохранения перебора [9] временнáя сложность (т.е. время решения уравнения (7) или время доказательства теоремы 1) определяется выражением:

 вдеп.                                                                                           (8)

Здесь вдеп ¾ временнáя дискретная единица перебора. Содержательно вдеп представляет собой время выполнения элементарной операции ag пересечения. Операция ag является основной операцией исчисления кубических комплексов (D-исчисления)[1]. Правила выполнения операции ag приведены ниже в табл. 6, в табл. 1-5 приведены таблицы истинности логических элементов КУ на рис. 1.

     В табл. 1-5 символ sr,k,l  обозначает строку справа в таблице; индекс r ¾ ранг КУ; k ¾ индекс, обозначающий номер логического элемента в множестве элементов, отнесённых к данному рангу, l ¾ номер строки в табл. 1-5. Повторим: операция ag является основной операцией классического  D-исчисления [1]. Правила покоординатного выполнения операции ag приведены в табл. 6. В таблице 6 символ cj,q обозначает значение в координате j куба Cq при выполнении шага q QD-алгоритма. Символ qj обозначает значение в координате j конкатенации Kr. Далее во второй части работы будут приведены все конкатенации строк табл. 1-5. Из табл. 6 также можно сделать вывод, что используемый в классическом исчислении алфавит A = {0, 1, ~, Æ}, mA = . Символ «~» ¾ символ неопределённого состояния; символ «Æ»¾ символ пустого пересечения.

2. Описание квантового генератора тестов (КГТ)

   КГТ «подогнан» (или «заточен») для выполнения QD-алгоритмов, основанных на D-исчислении. Для описания выполнения той же операции ag  при использовании QD-алгоритмов используется унитарная матрица U†R, которую автор назвал матрицей Рота, в честь Дж.П. Рота, создавшего классическое  D-исчисление [1]. Матрица Рота имеет вид:

       U†R   =                                                         (9)

Матрица U†R используется в новом матричном D-исчисления [10-12] в качестве подматрицы-блока (или блока) U†R в блочно-диагональной матрице URБ-Д,n   (U†R = , j = ).  Здесь n = dim H; H ¾ гильбертово пространство одного квантового разряда КГТ, который называется кунитом. Унитарная блочно-диагональная матрица URБ-Д,n  имеет вид:

URБ-Д,n  =                                                             (10)

 

В классическом ускорителе, моделью которого является идеальный генератор тестов (ИГТ), операция ag  реализуется аппаратно в виде классического блока пересечений (блока Bj ). Блок Bj  реализует ag, у которой функции определены табл. 6 [9]. В квантовом ускорителе, моделью которого является КГТ [10-12], функции  одной операции ag  определяются матрицей U†R = . Однако в КГТ n  операций ag  определяются матрицей URБ-Д,n , которая также реализована аппаратно в виде одного квантового блока пересечений ¾ блока QBj. В отличие от блока Bj, реализующего одну операцию ag, блок QBj параллельно реализует n  операций ag. Следует подчеркнуть, что логические основы в виде множества некоторых постулатов и некоторые доказательства здесь не приводятся. Их можно прочитать в [10-12] и в других наших работах. Теперь можно привести блок-схему КГТ ¾ см. рис. 2.

Как показано на рис. 2, КГТ состоит из двух квантовых регистров QR1 и QR2 . Он управляется классическим компьютером или суперкомпьютером, которые здесь не показаны. Число L квантовых разрядов в QR1 и QR2 одинаково: L1= =L2 = L.  Каждый разряд QR1 и QR2 является кунитом с одинаковой размерностью Dim H = n. Это означает, что в одном куните могут храниться n чисел или символов. В трёх кунитах  (L = 3) ¾ n3 чисел. Если L = 3 и n = 2 (это означает, что рассматривается кубит), то в трёх кубитах может одновременно храниться 23 = 8 чисел. Если L = 3 и n = 10, то в трёх кунитах может одновременно храниться 103 = 1000 чисел (1000 >> 8).  В L кунитах может хранится nL чисел  или символов, в L кубитах ¾ 2L  чисел. Теоретически число L, как и число n, могут быть больше любого наперёд заданного числа . Поэтому не случайно говорят, что «в гильбертовом пространстве много места». Отсюда в одном куните можно разместить куб Сq, который используется на шаге q QD-алгоритма. В другом куните можно разместить конкатенацию Kr соответствующих строк таблиц истинности (см. табл. 1-5). Это позволяет выполнить покоординатное пересечение (Сq Ç Kr), используя блоки пересечения QBj.

Рис. 2. Блок-схема КГТ

Примеры выполнения такого пересечения будут приведены во второй части нашей работы. В результате пересечения (Сq Ç Kr) можно получить один или несколько пустых или непустых кубов Сq+1. Пустой куб Сq+1 ¾ это куб, у которого в результате пересечения (Сq Ç Kr) хотя бы в одной координате появился символ Æ. Пустые кубы должны быть отбракованы схемами фильтрации, пролиферации и измерения, которые показаны на рис.2 ¾  см. также  [1,
8-11]. Полученные непустые кубы  записываются в первый кунит, благо, что «в гильбертовом пространстве много места». Если не удалось получить ни одного непустого куба, то работа QD-алгоритма завершена. В результате этого можно сделать вывод, что ни одного решения нашей задачи в виде набора Xi  не существует. В нашем случае это означает, что теорема 1, которую удалось свести к уравнению (7) будет доказана ¾ см. вторую часть данной работы: Правильщиков Проблема алгоритмической разрешимости (полуразрешимости) формальных систем и квантовые D-алгоритмы. Вторая часть приведена в докладе на этой же конференции. В этой второй части приведён также пример решения уравнения (7) с использованием  QD-алгоритма.

Литература

1.  Roth J.P.  Diagnosis of automata failures: a calculus and method.  // IBM Journal of Research and Development. 1966.  № 7 (July). P. 18-32.

2.  Пархоменко П.П., Правильщиков П.А.  Диагностирование программного обеспечения. // Автоматика и телемеханика. 1980. № 1, Стр. 103-121.

3.  Андерсон Р. Доказательство правильности программ: Пер. с англ. - М.: Мир, 1982. – 168

4.  Pixley C. Formal  Verification of Commercial Integrated Circuits. //IEEE Design & Test of Computer,
vol. 18, № 4 (July-August), 2001, pp. 4-5.

5.  Правильщиков П.А. Проблема верификации БИС и её решение путём использования " вычислительного решета" на основе закона сохранения перебора. //ж. "Оборонный  комплекс ― научно-техническому прогрессу России", М.: НТЦ "Информтехника", 2002. № 4 (стр. 45-61).

6.  Ильин В. В. Критерии научности знания.  М.: Высш. шк., 1989, ― 128 с.

7.  Ньюэлл А., Саймон Г., Шоу Дж.  GPS - программа, моделирующая процесс человеческого  мышления. В кн. "Вычислительные машины и мышление" // Под ред. Фейгенбаума Э. и  Фельдмана Дж., М.: "МИР", 1967, 464 с.

8.  Правильщиков П.А. Закон сохранения перебора и естественный параллелизм D-алгоритмов  для построения тестов и моделирования в технической диагностике. // Автоматика и телемеханика. 2004. № 7, Стр. 156-199.

9.  Правильщиков П.А. Квантовый параллелизм и новая модель вычислений. / Труды 12-го Всеросийского совещания по проблемам управления - ВСПУ-2014. М.: Институт проблем управления им. Трапезникова РАН. 2014. 9616 с. Стр. 7319-7334. ISBN 978-5-91450-151-5. № госрегистрации: 0321401153.

10.  Правильщиков П.А. Квантовый параллелизм и решение уравнений в задачах управления  на базе новой модели вычислений. / Труды 12-го Всеросийского совещания по проблемам управления ¾ ВСПУ-12. М.: Институт проблем управления им. Трапезникова РАН. 2014.  9616 с. Стр. 7335-7351. ISBN 978-5-91450-151-5.  № госрегистрации:  0321401153.

11.  Правильщиков П.А. Доказательство теорем с помощью квантового генератора тестов. // Информационные технологии в проектировании и производстве. 2015. № 3. С. 77-87.

 

 

 

 

 


[1] Утверждение, составляющее парадокс лжеца, в формальной логике рассматривается как не доказуемое и не опровержимое, и поэтому считается, что данное высказывание вообще не является логическим утверждением. Древнегреческий поэт, грамматик и критик Филит Косский умер от бессонницы, пытаясь разрешить парадокс лжеца.  Современные попытки разрешить парадокс приводят к обобщениям классической логики.
Примером может служить тройственная логика Я. Лукасевича. Также известны такие обобщения как комплексная логика или паранепротиворечивая (англ. Paraconsistent) логика Ф. М. Кесадо (Francisco Miró Quesada).  См. кн.:  Черепанов  С. К.  «Лгу, следовательно, высказываюсь» / Современная логика: проблемы теории, истории и применения в науке. — СПб., 2000. — С. 546—549. — ISBN 5-288-02703-X.

[2] Иногда выражение (5) называют также одним из двух логических правил Де Моргана, а иногда и одним из двух логических законов Де Моргана.

[3] С появлением полноценных квантовых компьютеров (КК), у которых квантовый регистр содержит 1000 кубитов, процесс выполнения алгоритма факторизации П. Шора, являющегося, по сути, один из вариантов алгоритма полного упорядоченного перебора, будет достаточно коротким. Тогда любой современный пароль может быть взломан приблизительно за 80 секунд. Не случайно алгоритм Шора так взволновал банковское сообщество и сообщество спецслужб.