Типовые металогические предикаты

Металогические предикаты

Лекция №7

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

Металогические предикаты помогут решить две проблемы, связанные с использованием переменных в предыдущих главах. Первая проблема относится к поведению переменных в системных предикатах. Например, вычисление арифметического выражения, содержащего переменную, приводит к ошибке. То же происходит при обращении к типовому предикату, аргумент которого – переменная. Все это приводит к уникальности программ на Прологе в отличие от эквивалентных логических программ.

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

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

Основным типовым металогическим предикатом является предикат var (Term), проверяющий, представляет ли собой терм Term переменную с неопределенным значением. Поведение этого предиката аналогично поведению типовых предикатов. Решение вопроса var (Term) успешно, если терм Term –- переменная, и безуспешно, если терм Term отличен от переменной. Например, var (X) выполнено, а решение обоих вопросов var (а)? и var ([X|Xs])? безуспешно.

Предикат var является расширением для программ на чистом Прологе. Для задания имен всех переменных таблицу использовать невозможно. Дело в том, что факт var (X) означает, что все примеры Х являются переменными, а не то, что буква “X” обозначает переменную. Возможность работы с именами переменных находится вне логики первого порядка вообще и вне чистого Пролога в частности.

Значение предиката nonvar (Term) противоположно значению предиката var. Цель nonvar (Term) выполнена, если Term не переменная, и приводит к безуспешному вычислению, если Term переменная.

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

Рассмотрим отношение plus (X,Y,Z). Программа 10.1 является версией plus. которая может быть использована и для сложения, и для вычитания. Идея состоит в проверке, какие установлены аргументы, до обращения к арифметическому вычислителю. Например, второе правило гласит, что если первый и третий аргументы, Х иZ, не переменные, то второй аргумент Y может быть определен как их разность. Заметим, что если аргументы – не целые числа, то вычисление, как и требуется, будет безуспешным.

Работа программы 10.1 подобна работе программы 3.3 – логической программы plus. В частности, она не приводит к ошибкам. И все же программе 10.1 не в полной мере присуща гибкость рекурсивной логической программы – она не может быть, например, использована для разбиения числа на два меньших числа. Разбиение числа использует порождение чисел, а для этого нужна другая программа. Данная задача сформулирована в виде упражнения в конце раздела.

plus(X,Y,Z)¬

суммачисел X и У равна Z.

plus(X,Y,Z)¬ nonvar(X), nonvar{Y), Z:- X + Y.

plus(X,Y,Z)¬ nonvar(X), nonvar(Z), Y:= Z-Y.

plus(X,Y,Z)¬ nonvar(Y), nonvar(Z), X:= Z-Y.

Программа 10.1. Программа plus. допускающая различные использования.

Металогические цели, расположенные в начале тела предложения для определения, какое предложение процедуры следует выполнять, называются металогическими тестами. Приведенная выше программа plus управляется металогическими тестами. Такие тесты относятся к текущему состоянию вычисления. Для понимания работы тестов требуется знание операционной семантики Пролога.

Многие версии Пролога фактически содержат типовые предикаты с металогическими свойствами. Так, в Edinburgh-Прологе цель integer(X) приводит, если Х – переменная, к безуспешным вычислениям, а не к ошибке. Это позволяет использовать в правилах программы 10.1 предикат integer вместо предиката nonvar, например:

plus (X,Y,Z)¬integer (X), integer (Y), Z: = X + Y.

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

Другим отношением, призванным восстановить универсальность программ на Прологе, является отношение length (Xs, N) – определение длины N списка Xs. Ранее для определения длины данного списка и для порождения произвольного списка данной длины потребовалось ввести две отдельные программы на Прологе (8.10 и 8.11), хотя обе функции выполняет одна логическая программа (3.17). Программа 10.2 использует металогические тесты для определения единого отношения length. Ее дополнительное преимущество перед программами 8.10 и 8.11 состоит в невозможности незавершающихся вычислений, присущих обеим программам, когда оба аргумента не определены.

length (Xs.N) ¬

список Xs имеет длину N.

length(Xs,N)¬ nonvar(Xs), lengthl (Xs,N).

length(Xs,N)¬ var(Xs), nonvar(N), length2(Xs,N).

length l(Xs,N)¬См. программу 8.11.

length2 (Xs, N)¬ См. программу 8.10.

Программа 10.2. Программа length, допускающая различные использования.

Металогические тестыможно также использовать для выбора наилучшего порядка целей в предложениях программы. В разд. 3.7 обсуждалось определение отношения дедушка_или_бабушка:

дедушка_или_бабушка (X, Z) ¬ родитель (X, Y), родитель (Y, Z).

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

Используя основные типовые металогические предикаты, можно определять более сложные металогические процедуры. Рассмотрим отношение ground (Term), истинное, если терм Term основной. Программа 10.4 определяет это отношение.

дедушка_или_бабушка(X,Y)¬

Z – внук X.

дедушка_или_бабушка (X,Z)¬ nonvar(X), родитель (X,Y), родитель (Y,Z). дедушка_или_бабушка(Х,Z) ¬ nonvar(Z), родитель(У,Z), родитель (X,Y).

Программа 10.3 – Более эффективная версия программы дедушка_или бабушка.

ground (Term) ¬

терм Term основной.

ground (Term)¬

nonvar(Tenn), constant (Term).

ground (Term)¬

nonvar(Term),

compound (Term),

functor(Term,F, N),

ground (N, Term),

ground (N, Term)¬

N>0,

arg(N,Term,Arg)

ground (A rg),

N1:= N-1,

ground(NI, Term). ground(0,Term).

Программа 10.4. Проверка, является ли терм основным.

Программа написана в стиле программ разд. 9.2, анализировавших структуры, в частности, в стиле программы 9.3, определяющей отношение substitute. Два предложения процедуры ground/1 достаточно очевидны. В обоих предложениях используется металогический тест, позволяющий избежать возникновения ошибочных ситуаций. Первое предложение утверждает, что константа является основным термом. Во втором предложении рассматриваются структуры. В нем происходит обращение к вспомогательному предикату ground/2, который итерационно проверяет, что все аргументы структуры – основные термы.

Рассмотрим более искусное применение типовых металогических предикатов на примере программирования алгоритма унификации. Необходимость в Прологе унификации для сопоставления цели и заголовка предложения означает доступность явного определения унификации. Исходная унификация Пролога может быть задана тривиальным определением

unify (Х,Х),

что совпадает с определением системного предиката = /2, задаваемого фактом Х=Х.

Заметим, что данное определение зависит от используемого в Прологе алгоритма унификации и, следовательно, не влияет на наличие проверки на вхождение.

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

В программе 10.5 приводится явное определение унификации. Отношение unify (Term1, Term2) истинно, если терм Term1 унифицирован с термом Term2. Предложения программы unify описывают возможные случаи. Первое предложение программы утверждает, что две переменные унифицируемы. Следующее предложение является записью правила унификации, утверждающего, что если Х переменная, то Х унифицируемо с Y.

ипifу (Term1, Term2) ¬

Term1 и Теrт2 унифицируемы без проверки на вхождение.

unify (X,Y)¬

var(X), var(Y), X = Y

unify (X,Y)¬

var(X), nonvar(Y), X = Y

unify (X,Y)¬

var(Y), nonvar(X), Y = X.

unify (X,Y)¬

nonvar(X), nonvar(Y), constant(X), constant(Y), X = Y

unify (X,Y)¬

nonvar(X), nonvar(Y), compound(X),

compound (Y), term_unify(X,Y).

term_unify(X,Y)¬

functor(X,F, N), functor(Y,F, N), unify_args(N, X, Y).

unify_args(N,X,Y)¬

N > 0,unify_arg(N,X,Y),Nl:= N - 1, unify_args(Nl,X,Y)

unify _args(0,X,Y),

unify_arg(N,X,Y)¬

arg(N, X, ArgX), arg(N, Y, ArgY), unify (ArgX, ArgY).

Программа 10.5. Алгоритм унификации.

Другой случай, являющийся предметом рассмотрения программы 10.5, состоит в унификации двух составных термов, как это описано предикатом term_unify (X, Y). В данном предикате проверяется, имеют ли два терма Х и У одинаковые главный функтор и арность, а затем проверяется, что все аргументы попарно унифицируемы. В этой процедуре предикат unify_ arg используется примерно так, как в рассмотренных ранее программах анализа структуры.

Дата добавления: 2014-01-07