Метод вычислений в параллельном логическом выводе

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Метод вычислений в параллельном логическом выводе

Д.А. Страбыкин (strabykin@mail.ru)

М.М. Шихов (kafevm@mail.ru)

Вятский государственный университет, Киров

Введение

В работе предлагается метод вычислений для параллельного логического вывода на знаниях, представленных формулами исчисления предикатов первого порядка. Описывается модификация формальной системы. Предлагается организация вычислений на подстановках с учетом параллельности логического вывода. Приводится пример вычислений, и дается оценка недостатков и преимуществ подхода.

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

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

1. Модификация формальной системы IP с целью введения вычислений

За основу был взят обобщенный метод параллельного дедуктивного вывода, представленный в работе [Страбыкин, 1998], в котором отсутствует возможность вычислений. Метод использует вводимую в той же работе формальную систему IP, которая подвергается незначительной модификации. Значениями будем называть специально вводимые символы, например, числа, строки, матрицы и т.д.

Изменяется определение терма.

Всякая предметная переменная (x_i^N), значение или функциональный символ (a_j^N) есть терм (будем обозначать либо просто t, либо t^N, когда необходимо. Множество значений функциональных символов также будем называть множеством предметных констант).

Если t^N, t₁,…,t_N - термы, то t^N(t₁,…,t_N) - также терм.

Если t - терм, то e(t) - терм. Здесь e - специальный символ, обозначающий вычислитель.

Других правил образования термов нет.

Вводятся дополнительные аксиомы. При этом мы полагаем, что в обозначении A[…,t,…] атом A имеет вхождения терма t в своем составе.

Аксиома вычисления предметной константы:

A[…,e(a_i),…]> A[…,a_i,…].

Аксиома вычисления функции с константными аргументами:

A[…,e(a₀^N(a₁,…,a_N)),…]>A[…,a^M,…],

где a^M есть результат отображения a₀^N:(a₁,…,a_N) > a^M. При этом все аргументы функции a₀^N в левой части формулы являются предметными константами.

Обобщенная аксиома вычисления функции:

A[…,e(t₀^N(t₁,…,t_N)),…]>A[…,e(e(t₀^N)(e(t₁),…, e(t_N))),…].

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

2. Реализация вычислений на подстановках

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

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

Подстановку л удобно определить как объединение двух непересекающихся множеств: л= л_v л_e. Множество л_e составляют замены вида e(t)/x, где t - терм, x - переменная исчисления, e(t) - вычислитель. Оставшиеся элементы t/x составляют множество л_v. В заменах t/x л_v не может быть вхождений вычислителя e(t'). Это достигается за счет того, что t[…,e(t'),…]/x преобразуется в t[…,y,…]/x, а к множеству л_e добавляется замена e(t')/y. Здесь y - фиктивная новая переменная предметной области. Причины такого подхода - минимизация объемов вычислений и упрощение описания алгоритмов. Также введем ряд дополнительных обозначений. Подстановку, не содержащую ни одной замены, будем обозначать . Подстановку, в которой присутствуют замены, конфликтующие по одной и той же переменной, причем термы-значения этих переменных не могут никакими заменами переменных в их составе сведены к одному значению, будем называть несогласованной и обозначать .

Результат работы вычислителя зависит от ограничений, накладываемых на область определения функций в составе его аргумента, и влияет на ход алгоритма согласованного объединения подстановок. Внутри системы вычислитель удобно рассматривать в виде процедуры, определенной следующим образом: e=<t, v, s>, где t - исходный терм; v - результат вычисления; s - признак окончания вычислений. Признак окончания s может принимать следующие значения: 0 - вычисления прошли без ошибок и v - константа предметной области; 1 - вычисления прошли без ошибок, но v - не является константой; 2 - в ходе вычислений возникли ошибки, делающие дальнейшее согласование подстановок невозможным. Алгоритм процедуры задается следующим образом.

1. Если терм принадлежит множеству констант предметной области, то v=t, s=0. Переход к пункту 10.

2. Если терм принадлежит множеству переменных, то v=e(t), s=1. Переход к пункту 10.

3. Если t=e(t'), то выполняется e<t',v,s>. Переход к пункту 10.

4. Иначе терм t есть функция t₀(t₁, …, t_n). Для каждого t_i (0 i n) рекурсивно выполняется e<t_i, v_i, s_i>.

5. Если max(s_1,…,s_n)=2, то v=e(t), s=2. Переход к пункту 10.

6. Иначе, если max(s_1,…,s_n)=1, то v = e(v'₀(v'₁, …, v'_n)), s=1. Где v'_i = t'_i, если v'_i=e(t'_i), и v'_i=v_i иначе. Переход к пункту 10.

7. Осуществляется проверка принадлежности кортежа (v₁,…,v_n) области определения функции v₀.

8. Если значения (v₁,…,v_n) не принадлежат области определения, то v=e(v₀(v₁,…,v_n)), s=2. переход к пункту 9.

9. Иначе, если значения (v₁,…,v_n) принадлежат области определения, то выполняется отображение v₀:(v₁,…,v_n) v. Фиксируется s=0.

10. Конец процедуры e.

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

вычисление параллельный логический вывод

3. Определение наименьшего общего унификатора

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

Рассмотрим все варианты возможных унификаций термов. Результатом унификации t₀(t₁,…,t_n) и t'₀(t'₁,…,t'_m) будет согласованное объединение подстановок {t₀/y₀,t₁/y₁,…,t_n/y_n} и {t'₀/y₀,t'₁/y₁,…,t'_m/y_m}. Особенностью специальных вспомогательных переменных y_i (1 i max(m, n)) является то, что сравнение x<y_i всегда истина для любой x из предметной области. Из результата согласованного объединения подстановок все элементы вида t/y_i могут быть исключены. Результатом унификации t₀(t₁,…,t_n) и предметной константы a всегда будет . Результатом унификации t₀(t₁,…,t_n) и переменной x будет либо , если t₀(t₁,…,t_n) содержит вхождения x, либо подстановка {t₀(t₁,…,t_n)/x}. Результатом унификации t₀(t₁,…,t_n) и вычислителя e(t) всегда будет . Результатом унификации констант a и a' будет либо (если a?a'), либо (если a=a'). Результатом унификации константы a и переменной x всегда будет подстановка {a/x}. Результатом унификации константы a и вычислителя e(t) будет подстановка {a/y, e(t)/y}, где y - фиктивная переменная (x<y всегда истина для любой x из предметной области). В дальнейшем если e(t) будет вычислен и окажется равным a, замены с фиктивной переменной можно удалить из результата. Результатом унификации двух переменных x и x' будет либо (если x=x'), либо {x/x'} (если x<x'), либо {x'/x} (если x'<x). Результатом унификации переменной x и вычислителя e(t) всегда будет подстановка {e(t)/x}. Результатом унификации двух вычислителей e(t) и e(t') будет либо (если t=t'), либо {e(t)/y, e(t')/y} (если t?t'). Здесь y - фиктивная переменная (x<y всегда истина, и в случае вычисления e(t)=e(t'), замены с y можно исключить).

Алгоритм двуместной операции согласованного объединения подстановок ' " следующий.

1. Если ' = , то ="; переход к пункту 17.

2. Иначе, если " = , то ='; переход к пункту 17.

3. Иначе, если '= или "=, то =; переход к пункту 17.

4. Иначе выполняется ='".

5. Множество разделяется на константную и вычислимую части =_ve; _ve=.

6. Выполняются замены переменных в составе термов t; t/x, соответствующими значениями из множества _v.

7. Для всех e(t_i); e(t_i)/x_ie множества выполняются процедуры e<t_i, v_i, s_i>.

8. Если хоть один s_i=2 то фиксируется =. Переход к пункту 17.

9. Иначе все e(t_i)/x_ie в составе преобразуются в v_i/x_i и, если имеются s_i=0, то переход к пункту 5.

10. Фиксируется одно из множеств всех значений некоторой переменной x: {t₁,…,t_n}; t_i/x_v, (1 i n). Причем n 2.

11. Если ни для какой переменной такое множество сформировать не удается, то выполняется переход к пункту 17.

12. Иначе устанавливается t'=t₁, j=2. Из множества исключается замена t₁/x.

13. В соответствии с изложенными выше правилами унификации находится _t как результат унификации терма t' и терма t_j.

14. Если _t=, то фиксируется = и выполняется переход к пункту 17.

15. Иначе из множества исключается замена t_i/x, выполняется j=j+1, t'=_tt', =_t.

16. Если j>n, то выполняется ={t'/x} и переход к пункту 5, иначе переход к пункту 13.

17. В качестве результата операции фиксируется .

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

4. Пример вычислений

Выполнить согласованное объединение подстановок: '={1/X, f(Y)/M, e(sin(Y))/Z} и "={f(0)/M, e(add(Z,X))/K}, которое предполагает вычисление элементарной функции sin(Y) и выполнение суммирования add(Z,X).

Процесс выполнения алгоритма с указанием шагов следующий.

1: 2: 3: 4: ='" ={1/X, f(Y)/M, e(sin(Y))/Z, f(0)/M, e(add(Z, X))/K}.

5: =_ve={1/X, f(Y)/M, f(0)/M}{e(sin(Y))/Z, e(add(Z, X))/K}.

6: =_ve= {1/X, f(Y)/M, f(0)/M}{e(sin(Y))/Z, e(add(Z, 1))/K}.

7: =_ve= {1/X, f(Y)/M, f(0)/M}{e(sin(Y))/Z, e(add(Z, 1))/K}.

8: 9: 10: {f(Y), f(0)} для переменной M.

11: 12: t'= f(Y); ={1/X, f(0)/M}{e(sin(Y))/Z, e(add(Z, 1))/K}; j=2.

13: результатом унификации t' и t₂, т.е. f(Y) и f(0) являетя _t={0/Y}.

14: 15: ={1/X}{e(sin(Y))/Z, e(add(Z, 1))/K}; j=3; t'=f(0); ={1/X} {e(sin(Y))/Z, e(add(Z, 1))/K}{0/Y}.

16: ={t'/x}={1/X}{e(sin(Y))/Z, e(add(Z, 1))/K}{0/Y}{f(0)/M}.

5: =_ve={1/X, 0/Y, f(0)/M}{e(sin(Y))/Z, e(add(Z, 1))/K}.

6: ={1/X, 0/Y, f(0)/M}{e(sin(0))/Z, e(add(Z, 1))/K.}

7: 8: 9: ={1/X, 0/Y, f(0)/M, 0/Z, e(add(Z, 1))/K} есть s_i=0 для получившейся 0/Z.

5: =_ve={1/X, 0/Y, f(0)/M, 0/Z}{e(add(Z, 1))/K}.

6: ={1/X, 0/Y, f(0)/M, 0/Z}{e(add(0, 1))/K}.

7: 8: 9: ={1/X, 0/Y, f(0)/M, 0/Z, 1/K} есть s_i=0 для получившейся 1/K.

5: =_ve={1/X, 0/Y, f(0)/M, 0/Z, 1/K}.

6: 7: 8: 9: 10: 11: 17: результат: {1/X, 0/Y, f(0)/M, 0/Z, 1/K}.

Таким образом, в процессе согласованного объединения подстановок выполнены вычисления: sin(Y)=0 (в замене sin(Y))/Z при Y=0) и add(Z,X)=1 (в замене add(Z,X))/K) при Z=0, X=1).

5. Свойства операции согласованного объединения подстановок

Согласование с пустой подстановкой не влияет на исходный операнд: ==. Согласование с несогласованной подстановкой в результате дает несогласованную подстановку: ==. Операция коммутативна: '='. И ассоциативна: '"=(')"=('").

Последние два свойства следуют из правил унификации терма и константы, а также терма и переменной, к которым в конечном итоге рекурсивно сводится операция согласованного объединения подстановок.

6. Достоинства и недостатки подхода

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

Введение вычислений на уровне термов дает большую гибкость и полностью покрывает возможности введения вычислений на уровне атомов, например, правила: ADD(A, B, e(add(A, B))), ADD(A, e(sub(C, A)), C), ADD(e(sub(C, B)), B, C) позволяют организовать «вычислимый» предикат, позволяющий находить числа, состоящие в отношении A+B=C.

Вычисления сосредоточены в рамках одной операции.

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

Также необходимо отметить, что приведенные алгоритмы имеют высокий ресурс распараллеливания как на уровне узла, выполняющего согласованное объединение подстановок, так и на более высоком уровне согласования решений [Страбыкин, 1998].

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

Список литературы

1. [Вагин и др., 2004] Вагин, В.Н. Достоверный и правдоподобный вывод в интеллектуальных системах [Текст] / В. Н. Вагин, Е. Ю. Головина, А. А. Загорянская, М. В. Фомина; под ред. В. Н. Вагина, Д. А. Поспелова. - М.: Физматлит, 2004.

2. [Страбыкин, 1998] Страбыкин, Д.А. Логический вывод в системах обработки знаний [Текст] / Д. А. Страбыкин; под ред. Д. В. Пузанкова. - СПб.: СПбГЭТУ, 1998.

3. [Страбыкин, 2008] Логический вывод с обобщением функциональных символов в формулах посылок и заключений [текст] / Д.А. Страбыкин, М.М. Шихов, Р.С. Петров // КИИ-2008 Одиннадцатая национальная конференция по искусственному интеллекту с международным участием (28 сентября - 3 октября 2008 г., Дубна, Россия). - М.: Физматлит, 2008, в 3-х т. - Т.1.

Размещено на Allbest.ru