Средства разработки приложений
При этом все переменные, входящие
Подстановка — это множество вида {x1/t1,..., xn/tn}, где для всех i, xi — переменная, а ti — терм, причем xi≠ti (отображение переменных в термы). При этом все переменные, входящие в подстановку, различны (для любого i≠j xi≠xj).
Символом ε будем обозначать пустую подстановку.
Подстановка, в которой все термы основные, называется основной подстановкой.
Простое выражение — это терм или атомная формула.
Если A — простое выражение, а θ — подстановка, то Aθ получается путем одновременной замены всех вхождений каждой переменной из θA соответствующим термом. Aθ называется частным случаем (примером) выражения A. Содержательно подстановка заменяет каждое вхождение переменной xi на терм ti.
Пусть θ и η — подстановки, θ={x1/t1,..., xn/tn}, η={y1/s1,...,yn/sn}. Композиция θη получается из множества {x1/t1η,...,xn/tn(,y1/s1,..., yn/sn} удалением пар xi/tiη, где xi≠tiη и пар yi/si, где yi совпадает с одним из xj.
Пример. Пусть θ={x/f(y),y/z}, η={x/a,y/b,z/y}. Построим θη. Для этого возьмем множество {x/f(b),y/y,x/a,y/b,z/y} и выбросим из него пары y/y (потому что заменяемая переменная совпадает с термом), ,x/a,y/b (потому что заменяемая переменная из подстановки η совпадает с заменяемой переменной из подстановки θ). Получим ответ: θη={x/f(b),z/y}.
Подстановка θ называется более общей, чем подстановка η, если существует такая подстановка γ, что η=θ γ.
Подстановка θ называется унификатором простых выражений A и B, если Aθ=Bθ. Про A и B в такой ситуации говорят, что они унифицируемы. Унификация используется в Прологе для композиции и декомпозиции структур данных.
Пример. A=p(f(x),z) и B=p(y,a) унифицируемы. Можно взять в качестве их унификатора подстановку {y/f(x),z/a} или подстановку {y/f(a),x/a,z/a}.
Вообще говоря, две формулы могут иметь бесконечно много унификаторов. Унификатор θ называют наиболее общим (или простейшим) унификатором простых выражений A и B, если он является более общей подстановкой, чем все другие унификаторы простых выражений A и B.
Пример. В рассмотренном выше примере наиболее общим унификатором является подстановка {y/f(a),z/a}.
Пусть S — конечное множество простых выражений. Определим множество d(S) разногласий (рассогласований). Зафиксируем самую левую позицию, на которой не во всех выражениях из S стоит один и тот же символ. Занесем в d(S) подвыражения выражений из S, начинающиеся с этой позиции.
Пример. Пусть S={p(f(x),h(y),a),p(f(x),z,a),p(f(x),h(y),b)}. Множество рассогласований для S d(S)={h(y),z}.
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий