Математическая логика и теория алгоритмов

Подстановки, примененные в рассматриваемом примере, мол<но обо­ значить следующим образом: 01 = {zlx, wly}, здесь z подставляется вместо х, aw вместо • 02 = {ФУ, 03 = {g{z)lx, afyy, 04 = {dx, dy). Применение подстановки 0 к литералу Р обозначаем Ре. Тогда имеем Рь,=Ръ, •^02 -рг-' ^04 - А- Если 0 - подстановка и она применяется к каждому из литера­ лов Li, то полученные частные случаи обозначаются через {i,}e. Последовательное применение двух подстановок 0i и 02 дает новую подстановку 0з, которую обозначаем 0з - 0i = 02. Множество {L) литералов называется унифицируемым, если существует такая подстановка 0, что (^Ое (•^'2)0 ~ = (^я)в- В этом случае подстановку 0 nsswRUKfYунификатором для {i,}. Пусть имеем множество литералов [Р{а, fly), b), Р(х, flh), b)}, где L\ = Р(х, b), Li = P{a, flb), b). Подстановка 0 = {alx, biy] явля­ ется, очевидно, унификатором для этого множества литералов. Унификатор о для множества выражений {Е\,Еъ...,Ек} называ­ ется наиболее общим унификатором тогда и только тогда, когда для каждого унификатора 0 для этого множества существует такая под­ становка что 0 = о • л., Существует алгоритм, называемый алгоритмом унификации, который приводит к наиболее общему унификатору для унифицируе­ мого множества литералов {i,} и сообщает о неудаче, если это мно­ жество не унифицируемо. Алгоритм унификации: Алгоритм начинает работу с пустой подстановки и шаг за шагом строит наиболее общий унификатор, если 108