Логическая и операционная семантика языка CCP

Логическая семантика есть функция LS, сопоставляющая каждой конструкции S языка CCP некоторую формулу LS в исчислении предикатов, т. е. LS(S) = LS. Пусть j(d: e) есть вызов предиката (4.1). Тогда

LS(j(d: e)) @ j(d, e) .

Пусть A(x:y) º K(x:y) - определение предиката (2). Тогда

LS(A(x:y) º K(x:y)) @ A(x,y) º LS(K(x:y)) [14] .

Логическая семантика LS(K(x:y)) для оператора K(x:y), обозначающего параллельный оператор, оператор суперпозиции или условный оператор, определена в разд. 4.5–4.7. Логическая семантика рекурсивных определений предикатов представлена в разд. 4.11.

Любая конструкция языка CCP легко конвертируется на язык исчисления предикатов. С операторами и предикатами языка CCP можно оперировать как с формулами исчисления предикатов. Поэтому далее будем иногда опускать применение функции LS и говорить об истинности операторов и предикатов.

Операционная семантика определена в виде метапрограммы, реализующей исполнение программы на языке CCP. Метапрограмма записана на метаязыке и исполняется абстрактным процессором. Ядром метаязыка являются базисные операции с памятью исполняемой программы. Память состоит из набора секций. Секция памяти содержит конечный набор переменных вместе с их значениями. Секция создается в начале исполнения вызова предиката, для которого имеется определение в программе. Секция состоит из аргументов, результатов и локальных переменных определения предиката.

Произвольная секция s представляется массивом. Индексами массива являются имена переменных. Пусть a - имя переменной. Тогда s[a] обозначает значение переменной с именем a в секции s. Если x - набор имен переменных, принадлежащих секции s, то s[x] обозначает соответствующий набор значений. Пусть a - имя переменной, а v - значение того же типа. Тогда s[a] := v обозначает оператор присваивания значения v переменной a в секции s. Будем также использовать групповой оператор присваивания s[x] := w, где x - набор имен переменных; w - набор значений. Оператор s = newSect(A) создает в памяти новую секцию s, соответствующую определению предиката с именем A. Секция s отлична от всех других секций, созданных ранее.

Исполнение вызова предиката j(d: e) в секции s при условии, что переменные наборов d и e принадлежат секции s, представляется на метаязыке следующей конструкцией:

runCall(s, j(d: e)) .

Исполнение оператора K(x:y) в секции s записывается на метаязыке следующей конструкцией:

runStat(s, K(x:y)) .

Конструкции метаязыка для исполнения параллельного оператора, оператора суперпозиции или условного оператора определены в разд. 4.5-4.7.

Возможен иной способ определения операционной семантики, предполагающий подстановку правой части определения предиката на место исполняемого вызова предиката. Такой способ используется для функциональных языков программирования (см., например, [1]).

Пусть H(x: y) есть вызов предиката [15] или оператор. Предикат RUN(H, x, y) для фиксированных значений наборов x и y обозначает следующее утверждение: существует такое исполнение H(x: y) для значений набора x, которое завершается, причем результатом являются значения набора y. Следует отметить, что данное определение RUN учитывает случай возможной неоднозначности, если рассматривать H как функцию из x в y. Определим свойство согласованности Cons(H):

Cons(H) @ "x "y (LS(H(x: y)) Û $y’ (RUN(H, x, y’) & eq(y, y’))) . (4.11)

Предикат eq(y, y’) определяет тождественность значений наборов y и y’ по следующим правилам. Пусть набор y есть y1, …, ym, m>0, а y’ есть y’1, …, y’m. Тогда истинны eq(y1, y’1), … eq(ym, y’m). Тождественность двух значений примитивного типа, а также типа множества подмножеств, определяется как равенство значений. Тождественность значений типа произведения или объединения определяется как покомпонентная тождественность. Тождественность значений j и j’ предикатного типа с наборами аргументов d и результатов e определяется как тождественность предикатов: "d "e (LS(j(d: e)) º LS(j’(d: e))).

Определение (4.11) свойства согласованности уточняет ранее приведенное определение (2.4). Значением переменной предикатного типа является имя предиката или массива (см. разд. 4.8 и 4.9). Порождение нового значения предикатного типа реализуется через конструктор предиката (или массива) и сопровождается заведением уникального имени предиката или массива. Поэтому разные срабатывания H(x: y) могут дать в результате разные имена предикатов (или массивов), причем эти предикаты тождественны.