Одной из фаз процесса доказательства некоторого целевого утверждения является унификация его аргументов с аргументами утверждений базы знаний. Как осуществляется унификация в том случае, когда аргументами цели являются списки? Чтобы пояснить этот процесс, введем понятие шаблона (образца) списка. Шаблон (образец) списка – это форма описания множества (семейства) списков, обладающих вполне определенными свойствами. Так, например, шаблон списка [Х|Y] описывает любой произвольный список, состоящий не менее чем из одного элемента; шаблон [Х1,Х2|Y] - список, состоящий не менее чем из двух элементов; аналогично [Х1,Х2,Х3|Y] - список, содержащий не менее трех элементов; а шаблон в виде переменной Z - любой список, в том числе и пустой. Шаблон может содержать как переменные, так и константы. Например, шаблон [b|Z] задает любой список, первым элементом которого является элемент b.
При унификации происходит сопоставление шаблонов. Если шаблоны целевого утверждения и утверждения базы знаний представляют списки с несовместимыми различными свойствами (разные классы списков), то унификация заканчивается неудачей. Так, например, нельзя сопоставить списки
[Х1,Х2|Т] [a]
[Х1,Х2,Х3|Z] [1,2]
и т.д.
Если шаблоны не противоречат друг другу, то осуществляется конкретизация отдельных переменных шаблона, т.е. присвоение им значений соответствующих констант, или сцепление с соответствующими переменными другого шаблона. В результате оба шаблона должны стать идентичными и породить общее решение - новый шаблон. Примеры: шаблон [[X,Y]|Z] задает список, начинающийся с подсписка из двух элементов; при сопоставлении его со списком [[a,b],c] унификация проходит успешно и переменные принимают следующие значения: Х=a, Y=b, Z=[c]. Шаблоны [X,Y|Z] и [[a,b]|T] при сопоставлении дают общее решение - новый шаблон [[a,b],Y|Z]; образец [[X|Y]|Z] описывает любой список, начинающийся с подсписка, в котором есть, по крайней мере, один элемент - элемент Х. Он соответствует, например, таким спискам:
[[a]] при X=a, Y=[], Z=[];
[[a,b],c] при X=a, Y=[b], Z=[c].
Если в процессе сопоставления и присвоения значений шаблоны не могут стать идентичными, то унификация заканчивается неудачей, как в следующем случае:
['бал',Y,Y] [X,X,'цех'],
где сопоставление показывает, что элементы обоих списков должны быть одинаковы, однако 'бал' не равно 'цех'.
|