Конструктор предиката является базисным предикатом ConsPred(x, B: A), где x - возможно пустой набор переменных; B - имя предиката; A - имя переменной предикатного типа. Значением переменной A является новый предикат, создаваемый при исполнении вызова предиката ConsPred. Ограничение: в качестве B нельзя использовать ConsPred или ConsArray. Логическая семантика предиката ConsPred дается определением
LS(ConsPred(x, B: A)) @ "y"z. (LS(A(y: z)) º LS(B(x, y: z))) . (4.23)
Здесь x, y и z - произвольные непересекающиеся наборы переменных, причем наборы x и y могут быть пустыми. Переменная A имеет предикатный тип PRED(Y: Z), см. (4.7), где Y и Z - наборы типов, соответствующие наборам переменных y и z.
Допустим, вызов предиката ConsPred(x, B: A) находится в правой части определения некоторого предиката, исполняемого в рамках секции s. Секция s включает набор x и переменную A. Исполнение вызова ConsPred(x, B: A) является частным случаем исполнения вызова runCall(s, ConsPred(x, B: A)) (см. разд. 4.4) и реализуется следующим оператором:
s[A] := newDef(s[x], B) . (4.24)
Функция newDef строит новое определение предиката:
Ax(y:z) º =(x~: t); B(t, y:z) . (4.25)
Здесь x~ = s[x] – значение набора x; Ax – новое имя предиката, отличное от имен других предикатов в программе. Имя Ax является результатом вызова newDef. Оператор =(x~: t) присваивает набор значений x~ набору локальных переменных t.
Мы не фиксируем, каким образом абстрактный процессор исполняет оператор =(x~: t). Например, процессор может создавать дополнительные определения, строящие изображения значений x~. Существует другой способ реализации вызова ConsPred(x, B: A), в котором переменной A присваивается кортеж (s[x], B).
Лемма 4.6. Cons(ConsPred).
Доказательство. Зафиксируем значения x = x0 и A = A0. Пусть истинно ConsPred(x, B: A). Докажем, что исполнение ConsPred(x, B: A) завершается значением A = Ax, тождественным A0, т. е. Ax º A0. Из истинности ConsPred(x, B: A) следует истинность правой части (4.23). Тогда истинна формула A0(y: z) º B(x0, y: z), однозначно определяющая предикат A0. Рассмотрим исполнение вызова ConsPred(x, B: A), т. е. оператора (4.24). Получаем A = Ax, где Ax определяется формулой (4.25). Поскольку x~ = s[x] = x0, то
Ax(y:z) º =(x0: t); B(t, y:z) º t = x0 & B(t, y:z) º B(x0, y: z) . (4.26)
Таким образом, A = Ax º A0, что доказывает первую половину леммы.
Допустим, исполнение ConsPred(x, B: A) завершается вычислением A = A0 при x = x0. Докажем истинность ConsPred(x, B: A), т. е. истинность правой части (4.23). Из (4.24) следует A = Ax, и далее A0 = Ax. Из тождества (4.26) следует A0(y:z) º B(x0, y: z). Поскольку A = A0 и x = x0, получаем истинность правой части (4.23). □
Лемма 4.7. Пусть имеется вызов ConsPred(x, B: A), причем Cons(B) истинно. Тогда истинно Cons(A).
Доказательство. Значением переменной A является Ax с определением (4.25). Поскольку свойство Cons истинно для оператора =(x~:t), то по лемме 4.3 оно реализуется также для правой части (4.25). Далее, по лемме 4.2 истинно Cons(Ax), а значит – и Cons(A). □