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

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

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

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

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

......................... (5.4)

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

причем 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 U {X1, X2,..., Xn})*.

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

phi= Z1 Z2... Zk, Zi Î (A U {X1, X2,..., Xn}) для i=1,..., k,

обозначает сцепление множеств 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),

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

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

X= a X U b X U c

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

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

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

L1=L U {phi a | phi Î {a, b}*}

и

L2=L U {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),

........... (5.5)

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

В качестве начального приближения решения этой системы принимается набор языков (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.

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

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

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

................L

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

С помощью денотационной семантики можно определять более широкий класс грамматики по сравне6нию с формой Бэкуса-Наура. Так в форме Бэкуса-Наура не определены правила вида

X::= X

тогда как уравнение вида

X = X

имеет вполне корректную интерпретацию в денотационной семантике.

Дата добавления: 2014-01-11