<<
>>

3.2.Унификация

Введем основные определения, следуя [Чень и Ли].

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

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

Определение 3.2.1.Подстановка - это конечное множество вида {α1∕t1, ., αn∕tn}, где

1. каждая αi - неабсолютная переменная,

2. каждый ti - терм, отличный от αi,

3. все αi различны.

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

Свойство 2 исключает подстановку неабсолютной переменной вместо ее самой.

Свойство 3 исключает различные варианты подстановки для одной и той же неабсолютной переменной.

Пусть θ = {α1∕t1, ., αn∕tn} - подстановка и А - формула. Тогда АО - формула, полученная из А заменой одновременно всех вхождений αi (1 ≤ i ≤ n) в А на ti.

Пусть θ = {α1∕t1, ., αn∕tn} и λ = {β1∕t*1, ., βm∕t*m} - две подстановки. Тогда композицияθ и λ есть подстановка (θ°λ), которая получается из множества {α1∕t1λ, ., αn∕tnλ, β1∕t*1, ., βm∕t*m} вычеркиванием (1) всех элементов αj∕tjλ, для которых tjλ = αj, и (2) всех элементов βi∕t*iтаких, что βi∈{α1, ., αn}.

Свойство (1) отбрасывает подстановки неабсолютной переменной вместо самой себя.

Свойство (2) запрещает различные варианты подстановок вместо одной и той же неабсолютной переменной.

Композиция подстановок ассоциативна. Пустая подстановка ε есть одновременно и левое и правое тождество, т.е. (θ°λ)°μ = θ°(λ°μ) и ε°θ = θ°ε для всех θ, λ, μ.

Подстановка θ накрывает подстановку θ1(обозначается θ ≥ θ1), если существует подстановка θ2: θ1 = θ°θ2. Если θ ≥ θ1 и θ1 ≥ θ, то θ = θ1.

Определение 3.2.2.Подстановка θ называется унификатором для множества формул {A1θ, ., Akθ} т.т.т., когда A1θ = A2θ = ... = Akθ. Множество формул {A1, ., Ak} унифицируемо, если для этого множества существует унификатор.

Например, подстановка θ = {x∕y, z∕v}, где x, z - неабсолютные переменные, y, v - абсолютные переменные, в формулы A(x, v) и A(y, z) приводит к тому, что A(x, v)θ = A(y, v) = A(y, z)θ. Значит, множество формул {A(x, v) и A(y, z)} унифицируемо.

Определение 3.2.3.Унификатор σ для множества формул {A1, ., Ak} будет наиболее общим унификатором т.т.т., когда для каждого унификатора θ для этого множества существует такая подстановка λ, что θ = σ°λ.

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

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

Например, алгоритм не будет стараться унифицировать формулы P(x, y) и Q(x, y), поскольку данные формулы различаются между собою входящими предикаторами.

Для целей нашего исследования можно ограничиться унификацией только пар формул.

Множество рассогласованийD для непустого множества подобных формул {А1, A2} получается выявлением первой (слева) позиции, на которой символы, входящие в формулы А1 и A2, не совпадают, и затем выписыванием из формул А1 и A2 каждого терма, занимающего эту позицию. Множество этих термов есть множество рассогласований в {А1, A2}.

Например, для формул А1= P(x, v) и A2 = P(y, z), где x, z - неабсолютные переменные, y, v - абсолютные переменные, множество рассогласований D есть {x, y}.

Поскольку x - неабсолютная переменная и y - абсолютная переменная, то возможна подстановка θ1 = {x∕y}, которая устраняет множество рассогласований D1 (индекс 1 обозначает по-порядку номер позиции, на которой возникло данное множество рассогласований).

Однако θ1не является унификатором для {P(x, v), P(y, z)}, поскольку P(x, v)θ = P(y, v) ≠ P(y, z)θ.

Формулы P(y, v) и P(y, z) не совпадают на второй позиции, образуя множество рассогласований D2 = {v, z}. Поскольку z - неабсолютная переменная и v - абсолютная переменная, то возможна подстановка θ2 = {z∕v}, которая устраняет множество рассогласований D2.

Таким образом, унификатором для формул P(x, v) и P(y, z) является композиция подстановок θ1°θ2 = {x∕y, z∕v}.

В процессе унификации возможно появление унификатора (подстановки, унифицирующей две формулы), который является композицией подстановок. Значит, первоначальные формулы, унификация которых является исходной задачей, в процессе поиска унификатора изменяются с помощью новых подстановок. В предыдущем примере из формулы P(x, v) при помощи подстановки {x∕y} получили формулу P(y, v), а из формулы P(y, z) при помощи подстановки {z∕v} получили формулу P(y, v).

Другими словами, если мы обозначим исходную формулу P(x, v) как А0 и исходную формулу P(y, z) как В0, то А1 есть P(y, v) и В1 = В0 = P(y, z).

Далее А2 = А1 = P(y, v) и В2 есть P(y, v). Таким образом, А2 = В2, т.е. P(x, v) и P(y, z) унифицируемы.

При этом подстановка {x∕y, z∕v} - унификатор для формул P(x, v) и P(y, z) - является композицией подстановок {x∕y} и {z∕v}.

Поскольку {A, A} = {A}, мы будем называть множество вида {A, A} одноэлементным.

Алгоритм унификации двух подобных формул А и В.

Символами ∕.∕ обозначены комментарии

Шаг 1. k = 0, Ak = A, Bk = В, σk = ε (пустая подстановка). Мотори™ берет исходные две формулы А и В, для которых необходимо найти унификатор. Исходным унификатором при этом является пустая подстановка ε7

Шаг 2. Если ни одна переменная в выводе не ограничивает сама себя, то перейти к шагу 3.

Иначе стоп: Akи В не унифицируемы. Выход из алгоритма. уИопытка унифицировать формулы Akи Віприводит к появлению в выводе переменной, которая ограничивает сама себяУ

Шаг 3. Если {Ak, В} - одноэлементное множество, то стоп: σk- наиболее общий унификатор для Akи Вь /Устранив k множеств рассогласований между формулами A0и В0 и получив из формулы A0(B0) формулу Ak(Bk), алгоритм добился, что Ak = Bk. Значит, последняя подстановка является наиболее общим унификатором для формул A0и В07

Иначе найдем множество рассогласований Dkдля формул Akи Вь

Шаг 4. Если существуют такие элементы αkи tkв Dk, что αk- неабсолютная переменная, которая не входит в tk, то перейти к шагу 5. /Подстановка, во-первых, осуществляется только вместо неабсолютной переменной и другие термы, а также предикаты и логические связки не подлежат замене. Во-вторых, осуществляя подстановку терма вместо неабсолютной переменной, необходимо следить, чтобы заменяемая переменная не входила в этот термУ

Иначе стоп: формулы Akи В не унифицируемы. Выход из алгоритма.

Шаг 5. Пусть σk+1 = {αk∕tk}, Ak+1 = Akk∕tk} и Вк+1= Bkk/tk}. Юсуществляем подстановку σk+1в формулу AiJBk) и получаем формулу Ak+1(Bk+1)./

Заметим, что Ak+1 = Aσk+1и Bk+1 = Bσk+1. ∕3toозначает, что формула Ak+^k+O может быть получена из формулы A0φ0) с помощью подстановки σk+1 = ((σ1oσ2)oσ3).. .oσk)), т.е. с помощью композиции k подстановок.^

Шаг 6. Присвоить значение k+1 и перейти к шагу 2.

Теорема 3.2.4.Вышеприведенный алгоритм конечен и всегда находит наиболее общий унификатор для унифицируемого множества A.

Доказательство: наш алгоритм унификации отличается от оригинального алгоритма унификации, предложенного в [Чень и Ли], наличием шага 2, т.е. проверкой наличия переменной, которая ограничивает сама себя.

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

С другой стороны, данная проверка сужает множество подстановок, допустимых согласно алгоритму унификации в [Чень и Ли].

Поскольку алгоритм унификации в [Чень и Ли] конечен и всегда находит наиболее общий унификатор, наш алгоритм унификации также конечен и всегда находит наиболее общий унификатор.

Доказано.

Поясним данный алгоритм на примерах.

Рассмотрим несложный пример, когда необходимо унифицировать формулы P(x) и P(y), где х - неабсолютная переменная и y - абсолютная переменная.

Пусть А есть Р(х) и В есть Р(у). Помещаем эти формулы в алгоритм. Тогда А0 = Р(х) и В0 есть Р(у), k = 0, σk = ε (пустая подстановка) (шаг 1).

Допустим, что в вывод не входит переменная, которая ограничивает сама себя (шаг 2).

Тогда найдем область рассогласований D0 = {x, y} для формул А0 и В0 (шаг 3).

Поскольку неабсолютная переменная х не входит в у, переходим к осуществлению подстановки (шаг 4).

Осуществляем подстановку σ1 = {х^} в формулы А0, B0и получаем формулы А1, B1. Отметим, что А1= ^σ1и B1 = B0σ1(шаг 5).

Присвоить параметру k значение 1 и вернуться на шаг 2.

Допустим, что в вывод не входит переменная, которая ограничивает сама себя (шаг 2).

А1= P(y) и В1 = P(y). Значит, {A1, B1} одноэлементное множество. Стоп: σ1 = {хУу} - наиболее общий унификатор для Р(х) и Р(у) (шаг 2).

Если в вышеприведенном примере переменная x, как и переменная y, является абсолютной, то формулы не унифицируемы, т.к. подстановка θ = {x∕y} невозможна, поскольку в формулах, согласно определению подстановки, замене подлежат только неабсолютные переменные. В таком случае алгоритм унификации остановится и выдаст ответ, что данное множество формул не унифицируемо.

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

Пусть требуется унифицировать формулы P(x1, y1), P(y2, x2), где y1< x1и y2< x2и х1, х2 суть неабсолютные переменные. Напомним, что yi< xiозначает, что переменная yi абсолютна ограничена и xi относительно ограничена.

Пусть А есть P(x1, y1) и В есть P(y2, x2). Помещаем эти формулы в алгоритм. Тогда А0= P(x1, y1) и В0 есть P(y2, x2), k = 0, σk = ε (пустая подстановка) (шаг 1).

Поскольку в y1< x1и y2< x2ни одна переменная не ограничивает сама себя (шаг 2), то

найдем область рассогласований D0 = {x1, y2} для формул А0 и В0 (шаг 3).

Поскольку неабсолютная переменная х1 не входит в у2, переходим к осуществлению подстановки (шаг 4).

Осуществляем подстановку σ1 = {х^у2} в формулы А0, B0и получаем формулы А1= P(γ2, y1) и B1 = P(y2, x2). Отметим, что А1= Λ0σ1и B1 = B0σ1(шаг 5).

Присвоить параметру k значение 1 и вернуться на шаг 2.

Поскольку в y1

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме 3.2.Унификация:

  1. ЗАКЛЮЧЕНИЕ
  2. Учение о красоте и триада благо-мудрость-красота.
  3. Терминологические и методологические проблемы
  4. Психоанализ
  5. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  6. 2.2. Исторические свидетельства о трактате «О природе космоса и души»
  7. 3.4.1. Учение о душе и видах душ.
  8. Гармоника в контексте мыслительного феномена прото­упорядочивания
  9. Научные исследования в перспективе вопроса о сущности воли
  10. Ответы к экзамену по логике,
  11. Sitz im Lebenпифагорейских псевдоэпиграфов