LecTP5 (1127816), страница 2
Текст из файла (страница 2)
Рис. 5.2. Таблица решений "Светофор у пешеходной дорожки".
Рассмотрим в качестве примера описание работы светофора у пешеходной дорожки. Переключение светофора в нормальных ситуациях должно производиться через фиксированное для каждого цвета число единиц времени (Tкр для красного цвета, Tжел для желтого, Tзел для зеленого). У светофора имеется счетчик таких единиц. При переключении светофора в счетчике устанавливается 0. Работа светофора усложняется необходимостью пропускать привилегированные машины (при их появлении на светофор поступает специальный сигнал) с минимальной задержкой, но при обеспечении безопасности пешеходов. Приведенная на рис. 5.2 таблица решений описывает работу такого светофора и порядок движения у него в каждую единицу времени. Звездочка () в этой таблице означает произвольное значение соответствующего условия.
5.3. Операционная семантика.
В операционной семантике алгебраического подхода к описанию семантики функций рассматривается следующий частный случай системы равенств (5.1):
f1(x1, x2, ... , xk)= E1,
f2(x1, x2, ... , xk)= E2,
. . . . . . . . . . . . . (5.3)
fn(x1, x2, ... , xk)= En,
где в левых частях равенств явно указаны определяемые функции с формальными параметрами, включающими (для простоты) обозначения всех входных данных x1, x2, ... , xk, а правые части представляют собой выражения, содержащие, вообще говоря, вхождения этих функций с аргументами, задаваемыми некоторыми выражениями, зависящими от входных данных x1, ... , xk.
Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой
s
E
T
выражения (терма) T в выражение E вместо символа s (в частности, переменной) будем понимать переписывание выражения E с заменой каждого вхождения в него символа s на выражение T. Каждое равенство
fi(x1, x2, ... , xk)= Ei
задает в параметрической форме множество правил подстановок вида
x1, x2, ... , xk
fi(T1, T2, ... , Tk) Ei ,
T1, T2, ... , Tk
где T1, T2, ... , Tk конкретные аргументы (значения или определяющие их выражения) данной функции. Это правило допускает замену вхождения левой его части в какое-либо выражение на правую часть этого правила.
Интерпретация системы равенств (5.3) для получения значений определяемых функций в рамках операционной семантики производится следующим образом. Пусть задан набор входных данных (аргументов) d1, d2, ... , dk. На первом шаге осуществляется подстановка этих данных в левые и правые части равенств с выполнением там, где это возможно, предопределенных операций и с выписыванием получаемых в результате этого равенств. На каждом следующем шаге происходит переписывание этих равенств со следующими преобразованиями. Если правая часть очередного равенства является каким-либо значением, то это равенство не изменяется (это значение и является значением функции, указанной в левой части этого равенства). В противном случае правая часть является выражением, содержащим вхождения каких-либо определяемых функций с теми или иными наборами аргументов. В этом случае для каждого вхождения функции (с конкретным набором аргументов) просматриваются левые части преобразуемых равенств. Если для этого вхождения находится совпадающая с ним левая часть, то проверяется правая часть этого равенства и в случае, если она является уже вычисленным значением, производится подстановка этого значения вместо указанного вхождения определяемой функции. Если же эта правая часть не является вычисленным значением, то указанное вхождение переписывается в неизменном виде. В том же случае, если для указанного вхождения не находится совпадающей с ним левая части, то формируется (и дописывается к имеющимся) новое равенство. Это равенство получается из исходного равенства для определяемой функции, вхождение которой в данный момент исследуется, путем подстановки в него вместо параметров аргументов этой функции из исследуемого вхождения (с выполнением предопределенных операций там, где это возможно). Эти шаги будут осуществляться до тех пор, пока все определяемые функции не будут иметь вычисленные значения.
В качестве примера операционной семантики рассмотрим определение функции F(n)=n! Она определяется следующей системой равенств:
F(0)=1,
F(n)=F(n-1)n.
Для вычисления значения F(3) осуществляются следующие шаги.
1-й шаг:
F(0)=1,
F(3)=F(2)3.
2-й шаг:
F(0)=1,
F(3)=F(2)3,
F(2)=F(1)2.
3-й шаг:
F(0)=1,
F(3)=F(2)3,
F(2)=F(1)2,
F(1)=F(0)1.
4-й шаг:
F(0)=1,
F(3)=F(2)3,
F(2)=F(1)*2,
F(1)=1.
5-й шаг:
F(0)=1,
F(3)=F(2)3,
F(2)=2,
F(1)=1.
6-й шаг:
F(0)=1,
F(3)=3,
F(2)=2,
F(1)=1.
Значение F(3) на 6-ом шаге получено.
5.4. Денотационная семантика.
В денотационной семантике алгебраического подхода рассматривается также система равенств вида (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],
. . . . . . . . . . . . . . . . . . . . . . . . . . . . (5.4)
Xn= phi[n,1] phi[n,2] ... 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 {X1, X2, ... , Xn})* .
Цепочка phi[i,j] рассматривается как некоторое выражение, определяющее значение, являющееся языком (множеством цепочек в алфавите A). Такое выражение определяется следующим образом. Если значения X1, X2, ... , Xn заданы, то цепочка
phi= Z1 Z2 ... Zk , Zi (A {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 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),
. . . . . . . . . . . (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.
С помощью денотационной семантики можно определять более широкий класс грамматики по сравне6нию с формой Бэкуса-Наура. Так в форме Бэкуса-Наура не определены правила вида
X::= X
тогда как уравнение вида
X= X
имеет вполне корректную интерпретацию в денотационной семантике.
5.5. Аксиоматическая семантика.
В аксиоматической семантике алгебраического подхода система (5.1) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и/или интерпретации определяемых объектов.
Для интерпретации системы (5.1) вводится понятие аксиоматического описания (S, E) логически связанной пары понятий: S сигнатура используемых в системе (5.1) символов функций
f1, f2, ... , fm и символов констант (нульместных функциональных символов) c1,c2, ... , cl, а E набор аксиом, представленный системой (5.1). Предполагается, что каждая переменная xi, i=1, ... , k, и каждая константа ci, i=1, ... , l, используемая в E, принадлежит к какому-либо из типов данных t1, t2, ... , tr, а каждый символ fi,
i=1, ... , m, представляет функцию, типа
ti1 ti2 ... tik ti0.
Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных ti=ti', i=1, ... , r, и конкретные значения констант ci=ci', i=1, ... , l. В таком случае говорят, что задана одна конкретная интерпретация A символов сигнатуры S, называемая алгебраической системой
A=(t1', ... , tr', f1', ... , fm', c1', ... , cl'),
где fi', i=1, ... , m, конкретная функция, представляющая символ fi. Таким образом, аксиоматическое описание (S, E) определяет класс алгебраических систем (частный случай: одну алгебраическую систему), удовлетворяющих системе аксиом E, т.е. превращающих в тождества равенства системы E после подстановки в них fi',
i=1, ... , m, и ci', i=1, ... , l, вместо fi и ci соответственно.
В программировании в качестве алгебраической системы можно рассматривать, например, тип данных, при этом определяемые функции представляют операции, применимые к данным этого типа. Так К. Хоор построил аксиоматическое определение набора типов данных [5.4], которые потом Н. Вирт использовал при создании языка Паскаль.
В качестве примера рассмотрим систему равенств
УДАЛИТЬ(ДОБАВИТЬ(m, d))=m,
ВЕРХ(ДОБАВИТЬ(m, d))=d,
УДАЛИТЬ(ПУСТ)=ПУСТ,
ВЕРХ(ПУСТ)=ДНО,
где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ символы функций, а ПУСТ и ДНО символы констант, образующие сигнатуру этой системы. Пусть D, D1 и М - некоторые типы данных, такие, что m M, d D, ПУСТ M, ДНО D1, а функциональные символы представляют функции следующих типов:
УДАЛИТЬ: M M,
ДОБАВИТЬ: M D M,
ВЕРХ: M D1.
Данная сигнатура вместе с указанной системой равенств, рассматриваемой как набор аксиом, образует некоторое аксиоматическое описание.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
