Денотационная семантика.
В денотационной семантике алгебраического подхода рассматривается также система равенств вида (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] рассматривается как некоторое выражение, определяющее значение, являющееся языком. Такое выражение определяется следующим образом. Если значения 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 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.
В рассмотренном примере этот процесс даёт следующую последовательность приближений:
L[0]= Æ,
L[1]= {c}, L[2]= {c, ac, bc},
L[3]= {c, ac, bc, aac, abc, bac, bbc},
. . . . . . . . . . . . . . . .
Этот процесс сходится к указанному выше наименьшему решению L.
С помощью денотационной семантики можно определять более широкий класс грамматики по сравнению с формой Бэкуса-Наура. Так в форме Бэкуса-Наура не определены правила вида
X::= X
тогда как уравнение вида
X= X
имеет вполне корректную интерпретацию в денотационной семантике.
Дата добавления: 2016-04-06; просмотров: 470;