Оператор суперпозиции

Оператор суперпозиции является правой частью следующего определения предиката:

A(x: y) º B(x: z); C(z: y). (4.16)

Здесь x, y и z - произвольные непересекающиеся наборы переменных, причем набор x может быть пустым. Если B или C есть имя переменной предикатного типа, оно входит в набор x. Переменные набора z являются локальными переменными. Логическая семантика оператора суперпозиции представлена следующим образом:

LS(B(x: z); C(z: y)) @ $z. (B(x, z) & C(z, y)). (4.17)

Допустим, определение предиката A исполняется в рамках секции s. Секция s состоит из переменных наборов x, y и z. Исполнение правой части определения (4.16) соответствует оператору runStat(s, K(x: y)) в (4.14) и определяется следующим образом:

runCall(s, B(x: z)); (4.18)

runCall(s, C(z: y)).

Таким образом, алгоритм вычисления суперпозиции состоит в последовательном исполнении вызовов предикатов B и C. Значения переменных набора z, вычисленные при исполнении предиката B, используются при вычислении предиката C.

Лемма 4.3. Cons(B) & Cons(C) Þ Cons(H), где H обозначает B(x: z); C(z: y).

Доказательство. Пусть истинно Cons(B) и Cons(C). Докажем истинность Cons(H). Зафиксируем значения x и y. Пусть истинна H(x: y), т. е. истинна правая часть (4.17). Для некоторого z будут истинны B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует, что исполнение B(x: z) завершается получением набора z, а исполнение C(z: y) - вычислением набора y. Поэтому исполнение операторов (4.18), а значит и H(x: y), завершается вычислением y. Это доказывает первую часть истинности Cons(H).

Допустим, исполнение H(x: y) завершается вычислением y. Докажем истинность H(x: y). Исполнение пары операторов (4.18) завершается вычислением y. В частности, завершается первый оператор runCall(s, B(x: z)). Тогда существует некоторый набор z, являющийся результатом исполнения. Таким образом, для некоторого z исполняются вызовы B(x: z) и C(z: y). Из Cons(B) и Cons(C) следует истинность B(x: z) и C(z: y). Следовательно, истинна правая часть (18) и H(x: y). □