УДК 519.68:510

   В работе дано определение T-оптимизируемой системы логического программирования, где T - некоторое множество преобразований программ. В качестве иллюстрации общего подхода выбраны интерпретатор системы PROLOG и множество преобразований, которые переставляют и удаляют предложения программ, переставляют атомы в телах правил программ. Для ряда систем логического программирования получены результаты относительно их T-оптимизируемости.
   1. Определения и обозначения. Зафиксируем три непересекающихся счетных множества Ф, П и Х. Ф - множество функциональных символов с приписанной каждому символу местностью, причем для любого n > 0 Ф содержит счетное число символов местности n. Х - множество предметных переменных. Из элементов множеств Ф и Х строятся термы.
   1. Каждый 0-местный символ из Ф есть терм.
   2. Каждая переменная из Х есть терм.
   3. Если t₁, t₂, ..., t_n (n > 0) - термы и f - n - местный символ из Ф, то f(t₁,ј,t_n) есть терм.
   4. Других термов нет.
   Множество всех термов, не использующих предметных переменных, обозначим через M. Множество M называется универсумом Эрбрана.
   П=П₁ИП₂, где П₁ - множество предикатных символов с приписанной каждому символу местностью, причем для любого n > 0 П₁ содержит счетное число символов местности n; П₂ - некоторое множество интерпретированных предикатных символов (встроенных предикатов), каждый k-местный (k > 0) встроенный предикат представляет собой вычислимое отображение M^k®{true, false}.
   Атом определяется традиционным образом:
   1. Каждый 0-местный символ из П₁ есть атом.
   2. Если  t₁, ј, t_n  (n > 0) - термы  и  p - n-местный  символ  из  П₁,  то p (t₁,ј,t_n) есть атом.
   3. Других атомов нет.
   Атом, использующий предикатный символ из П₁, назовем предикатным термом. Атом, использующий встроенный предикат из П₂, назовем условием. Множество всех переменных атома A обозначим через Var(A).
   Традиционным образом определяется формула логики предикатов первого порядка, использующая логические операции Ш,&, Ъ, Й и кванторы $, " (см.[1]).
   Опишем рассматриваемые нами интерпретации. Предметным множеством рассматриваемых интерпретаций будет множество M. Функциональные символы интерпретируются следующим образом: каждому 0-местному символу из Ф сопоставляется он сам, каждому n-местному (n > 0) символу f О Ф сопоставляем отображение Mⁿ ® M, которое n-ке (t₁,ј,t_n) О Mⁿ, где t_i О M, i = 1,ј,n, ставит в соответствие терм f(t₁,ј,t_n). Каждому 0-местному символу из П₁ сопоставляется один из элементов множества {true, false}, а каждому n-местному (n > 0) символу из П₁ сопоставляется некоторое отображение Mⁿ ® { true, false}. Обозначим описанное множество интерпретаций через H. Заметим, что интерпретации из H могут отличаться одна от другой лишь отображениями, сопоставляемыми символам множества П₁.
   Пусть F - замкнутая формула и I - интерпретация из H. Значение формулы F на интерпретации I определяется традиционным образом. Формула называется тождественно истинной, если она принимает значение true на любой интерпретации из H. Пусть F и Fў - замкнутые формулы. Мы будем говорить, что формула Fў является логическим следствием формулы F, и обозначать это F|=Fў, если формула F Й Fў является тождественно истинной.
   Логическая программа P (далее просто программа) есть последовательность предложений D₁,ј,D_n, n > 0. Предложение D О {D₁,ј,D_n} является либо фактом A, либо правилом A:-B₁,ј,B_m, которое является импликацией B₁&ј&B_m Й A, где A - предикатный терм, а каждое из B₁,ј,B_m либо предикатный терм, либо условие, m > 0. Атом A называется головой предложения D, а последовательность B₁,ј,B_m - его телом.
   Программе P сопоставляется формула

"x1ј"xv(D1&ј& Dn) ,

где x₁,ј, x_v - переменные, использованные в предложениях D₁,ј, D_n, v і 0.
   Запрос Q имеет вид ?-C₁,ј,C_k, где C_i - либо предикатный терм, либо условие, i = 1,ј,k, k > 0. Запросу Q сопоставляется формула

$y1 ј$ys(C1& ј& Ck) ,

где  y₁, ј, y_s  -  переменные,  использованные  в  атомах  C₁,ј, C_k,  s і 0 (см. [2, 3]).
   2. Постановка задачи. Система логического программирования (кратко LPS) определяется заданием тройки < Prog, Quer, U > , где Prog - некоторое множество программ, Quer - некоторое множество запросов, U - интерпретатор, представляющий собой алгоритм, который для каждой программы P О Prog и запроса Q О Quer либо останавливается с положительным ответом (yes), либо с отрицательным ответом (no), либо с неопределенным ответом, либо функционирует бесконечно. Результат применения U к P и Q обозначим U(P,Q). Если U(P,Q) есть yes или no, то будем говорить, что U(P,Q) - определено. Интерпретатор U должен обладать свойством логической корректности:
             если U(P,Q) = yes, то P| = Q;
             если U(P,Q) = no, то P| № Q.
   Пусть P О Prog и Yes(P) = {Q | Q О Quer и P| = Q}.
   Будем говорить, что программы P₁,P₂ О Prog эквивалентны (обозначим P₁ ~ P₂), если Yes(P₁)=Yes(P₂).
   Под преобразованием множества программ Prog мы будем понимать пару (P,Pў), где P ~ Pў, P,Pў О Prog. Пусть T - некоторое множество преобразований программ Prog, причем для любой программы P О Prog пара (P,P) О T. Будем говорить, что программа P О Prog T-преобразуема в программу Pў О Prog, если существует такая последовательность преобразований (P₁, P₂), ј,(P_n-1,P_n), принадлежащих T, что P₁=P,  P_n=Pў, n > 1 (см. [4]).
   Пусть V - алгоритм, который, получив на вход программу P О Prog, T-преобразует её в программу Pў О Prog (т.е. посредством преобразований множества T преобразует программу P в программу Pў). Обозначим через W множество всех таких алгоритмов.
   Будем говорить, что система логического программирования (LPS) T-оптимизируема, если существует такой алгоритм V₀ О W, что для любого алгоритма V О W, для любой программы P О Prog и для любого запроса Q О Quer имеем:

U(V(P),Q) -  определено Ю  U(V0(P),Q) -  определено.

   3. Полученные результаты. Для каждого множества программ Prog определим множество преобразований T, которые переставляют и удаляют предложения программ, переставляют атомы в телах правил программ (см. [4]).
   Пусть U - интерпретатор системы PROLOG (см. [3, 5]).
   LPS, программы и запросы которой не содержат встроенных предикатов, назовем чистой LPS.
   Tеорема 1. Чистая LPS (чистый PROLOG) не является T-оптимизируемой.
   Доказательство. Пусть a,b, - 0-местные функциональные символы из Ф, p, q, r - 1-местные предикатные символы из П₁, x - переменная из Х. Рассмотрим следующую программу P и запросы Q и Qў.
   Программа P:
   q(a).
   r(b).
   q(x) : - p(x).
   r(x) : - p(x).
   p(x) : - q(x).
   p(x) : - r(x).
   Запрос Q : ? - p(a).
   Запрос Qў: ? - p(b).
   Легко видеть, что P|=Q, P|=Qў и для любой собственной подпоследовательности P¢¢ программы P имеем: P¢¢ не эквивалентна P. Легко также заметить, что интерпретатор U остановится с положительным ответом (yes) для программы P и запроса Q и будет функционировать бесконечно для программы P и запроса Qў.
   Преобразуем программу P, переставив местами её последние два предложения p(x) : - q(x) и p(x) : - r(x). Получим программу Pў. Очевидно, что P ~ Pў и интерпретатор U остановится с положительным ответом (yes) для программы Pў и запроса Qў и будет функционировать бесконечно для программы Pў и запроса Q.
   Теорема 1 доказана.
   Tеорема 2. Чистая LPS, программы и запросы которой не используют переменных, T-оптимизируема.
   Доказательство следует из результатов работы [4].
   Будем говорить, что программа P содержит повторяющийся предикатный символ q, если число предложений прграммы P, головы которых используют сивол q, больше 1.
   Tеорема 3. Чистая LPS, программы которой не содержат повторяющихся предикатных символов, T-оптимизируема.
   Доказательство следует из результатов работы [4].
   LPS, которая использует только 0-местные функциональные символы, 0-местные и 1-местные предикатные символы и встроенные предикаты < , > ,=, называется простой LPS.
   Tеорема 4. Чистая простая LPS, не является T-оптимизируемой.
   Справедливость теоремы 4 следует из доказательства теоремы 1.
   Tеорема 5. Простая LPS программы которой не используют повторяющихся предикатных символов не является T-оптимизируемой.
   Доказательство. Пусть q - 0-местный, p,r,s - 1-местные предикатные символы из П₁, x - переменная из Х. Рассмотрим следующую программу P и запросы Q и Qў.
   Программа P:
   q : - x > 0.
   r(x) : - x > 3,  q.
   s(x) : - x < 7,  q.
   p(x) : - r(x),  s(x).
   Запрос Q : ? - p(2).
   Запрос Qў: ? - p(8).
   Легко видеть, что P| № Q, P| № Qў и для любой собственной подпоследовательности P¢¢ программы P имеем: P¢¢ не эквивалентна P. Легко также заметить, что интерпретатор U остановится с отрицательным ответом (no) для программы P и запроса Q и остановится с неопределённым ответом для программы P и запроса Qў.
   Преобразуем программу P, переставив местами атомы в теле её последнего предложения, т. е. последнее предложение теперь стало иметь p(x) : -  s(x),  r(x). Получим программу Pў. Очевидно, что P ~ Pў и интерпретатор U остановится с отрицательным ответом (no) для программы Pў и запроса Qў и остановится с неопределённым ответом для программы Pў и запроса Q.
   Теорема 5 доказана.
   Правило A : - B₁,ј,B_m (m > 0) назовем a-правилом, если Var(B₁)И ј ИVar(B_m) Л Var(A).
   Tеорема 6. Простая LPS, программы которой не содержат a-правил и повторяющихся предикатных символов, T-оптимизируема.