Денотационная семантика.

В денотационной семантике алгебраического подхода рассматривается также система равенств вида (5.3), которая интерпретируется как система функциональных уравнений, а определяемые функции являются некоторым решением этой системы. В классической математике изучению функциональных уравнений (в частности, интегральных уравнений) уделяется большое внимание и связано с построением достаточно глубокого математического аппарата. Применительно к программированию этими вопросами серьезно занимался Д. Скотт [5.3].

Основные идеи денотационной семантики проиллюстрируем на более простом случае, когда система равенств (5.3) является системой языковых уравнений:

X1= phi[1,1]  phi[1,2]  ...  phi[1,k1],

X2= phi[2,1]  phi[2,2]  ...  phi[2,k2],

. . . . . . . . . . . . . . . . . . . . . . . . . . .

Xn= phi[n,1]  phi[n,2]  ...  phi[n,kn],

(5.4)


причем i-ое уравнение при ki=0 имеет вид

Xi=

Как известно, формальный язык - это множество цепочек в некотором алфавите. Такую систему можно рассматривать как одну из интерпретаций набора правил некоторой грамматики, представленную в форме Бэкуса-Наура (каждое из приведенных уравнений является аналогом некоторой такой формулы). Пусть фиксирован некоторый алфавит A={a1, a2, ... , am} терминальных символов грамматики, из которых строятся цепочки, образующие используемые в системе (5.4) языки. Символы X1, X2, ... , Xn являются метапеременными грамматики, здесь будут рассматриваться как переменные, значениями которых являются языки (множества значений этих метапеременных). Символы phi[i,j], i=1,...,n, j=1,...,kj, обозначают цепочки в объединенном алфавите терминальных символов и метапеременных:

phi[i,j](A | {X1, X2, ... , Xn})* .

Цепочка phi[i,j] рассматривается как некоторое выражение, определяющее значение, являющееся языком (множеством цепочек в алфавите A). Такое выражение определяется следующим образом. Если значения X1, X2, ... , Xn заданы, то цепочка

phi= Z1 Z2 ... Zk , Zi(A | {X1, X2, ... , Xn}),

обозначает сцепление множеств Z1, Z2, ... , Zk , причем вхождение в эту цепочку символа aj представляет множество из одного элемента {aj}. Это означает, что phi определяет множество цепочек

{p1 p2 ... pk | pjZj, j=1,...,k},

причем цепочка

p1 p2 ... pk

представляет собой последовательность выписанных друг за другом

цепочек p1, p2, ... , pk . Таким образом, каждая правая часть уравнений системы (5.4) представляет собой объединение множеств цепочек.

Решением системы (5.4) является набор значений (языков)

L1, L2, ... , Ln

переменных X1, X2, ... ,Xn, для которых все уравнения системы (5.4) превращаются в тождество.

Рассмотрим в качестве примера частный случай системы (5.4), состоящий из одного уравнения

X= a X  b X  c

с алфавитом A={a,b,c}. Решением этого уравнения является язык

L={ phi c | phi{a,b}*}.

Система (5.4) может иметь несколько решений. Так в рассмотренном примере помимо L решениями являются также

L1=L  {phi a | phi{a,b}*}

и

L2=L  {phi b | phi{a,b}*}.

В соответствии с денотационной семантикой в качестве определяемого решения системы (5.4) принимается наименьшее. Решение (L1,L2, ... ,Ln) системы (5.4) называется наименьшим, если для любого другого решения (L1',L2',...,Ln') выполняется

L1 L1', L2 L2', ... , Ln Ln'.

Так в рассмотренном примере наименьшим (а значит, определяемым денотационной семантикой) является решение L.

В качестве метода решения систем уравнений (5.3) и (5.4) можно использовать метод последовательных приближений. Сущность этого метода для системы (5.4) заключается в следующем. Обозначим правые части уравнений системы (5.4) операторами Ti(X1,X2,...,Xn). Тогда система (5.4) примет вид

X1=T1(X1,X2, ... ,Xn),

X2=T2(X1,X2, ... ,Xn),

. . . . . . . . . .

Xn=Tn(X1,X2, ... ,Xn).

(5.5)

В качестве начального приближения решения этой системы примем набор языков (L1[0], ... , Ln[0]) = (, ,..., ). Каждое следующее приближение определяется по формуле:

(L1[i],...,Ln[i])= (T1(L1[i-1], ..., Ln[i-1]), . . . . . . . . (Tn(L1[i-1], ..., Ln[i-1])).

Так как операции объединения и сцепления множеств являются монотонными функциями относительно отношения порядка Н , то этот процесс сходится к решению (L1,...,Ln) системы (5.5), т.е.

(L1,...,Ln)= (T1(L1,...,Ln), ..., Tn(L1,...,Ln))

и это решение является наименьшим. Это решение называют еще наименьшей неподвижной точкой системы операторов

T1, T2, ... , Tn.

В рассмотренном примере этот процесс дает следующую последовательность приближений:

 

L[0]= , L[1]= {c}, L[2]= {c,ac,bc},

L[3]= {c,ac,bc,aac,abc,bac,bbc},

. . . . . . . . . . . . . . . .

Этот процесс сходится к указанному выше наименьшему решению L.