48241 (597387), страница 6

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 6)

f_n(x₁, x₂, ... , x_k) = E_n,

где в левых частях равенств явно указаны определяемые функции с формальными параметрами, включающими (для простоты) обозначения всех входных данных x₁, x₂, ..., x_k, а правые части представляют собой выражения, содержащие, вообще говоря, вхождения этих функций с аргументами, задаваемыми некоторыми выражениями, зависящими от входных данных x₁, x₂, ..., x_k.

Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой

| s E | | T

выражения (терма) T в выражение E вместо символа s (в частности, переменной) будем понимать переписывание выражения E с заменой каждого вхождения в него символа s на выражение T. Каждое равенств

f_i(x₁, x₂, ..., x_k) = E_i

задает в параметрической форме множество правил подстановок вида

|x₁, x₂, ..., x_kf_i(T₁, T₂, ..., T_k) -> E_i | |T₁, T₂, ..., T_k

где T₁, T₂, ..., T_K — конкретные аргументы (значения или определяющие их выражения) данной функции. Это правило допускает замену вхождения левой его части в какое-либо выражение на его правую часть.

Интерпретация системы равенств (3) для получения значений определяемых функций в рамках операционной семантики производится следующим образом. Пусть задан набор входных данных (аргументов) d₁, d₂, ..., d_k. На первом шаге осуществляется подстановка этих данных в левые и правые части равенств с выполнением там, где это возможно, предопределенных операций и с выписыванием получаемых в результате этого равенств. На каждом следующем шаге просматриваются правые части полученных равенств. Если правая часть является каким-либо значением, то оно и является значением функции, указанной в левой части этого равенства. В противном случае правая часть является выражением, содержащим вхождения каких-либо определяемых функций с теми или иными наборами аргументов. Если для такого вхождения соответствующая функция с данным набором аргументов имеется в левой части какого-либо из полученных равенств, то либо вместо этого вхождения подставляется значение правой части этого равенства, если оно уже вычислено, с выполнением, где это возможно, предопределённых операций. Либо не производится никаких изменений, если значение этой правой части ещё не вычислено. В том же случае, если эта функция с данным набором аргументов не является левой частью никакого из полученных равенств, то формируется (и дописывается к имеющимся) новое равенство. Оно получается из исходного равенства для данной функции с подстановкой в него вместо параметров указанных аргументов этой функции. Эти шаги осуществляются до тех пор, пока все определяемые функции не будут иметь вычисленные значения.

В качестве примера операционной семантики рассмотрим определение функции факториала 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-ом шаге получено.

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

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

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

X₁ = φ_1,1  φ_1,2  ...  φ_1,k1,

X₂ = φ_2,1  φ_2,2  ...  φ_2,k2,

(4) .....…………………………

X_n= φ_n,1  φ_n,2  ...  φ_n,kn,

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

X_i = 

Как известно, формальный язык — это множество цепочек в некотором алфавите. Такую систему можно рассматривать как одну из интерпретаций набора правил некоторой грамматики, представленную в форме Бэкуса-Наура (каждое из приведенных уравнений является аналогом некоторой такой формулы). Пусть фиксирован некоторый алфавит A = {a₁, a₂, …, a_m} терминальных символов грамматики, из которых строятся цепочки, образующие используемые в системе (4) языки. Символы X₁, X₂, ..., X_n являются метапеременными грамматики, здесь будут рассматриваться как переменные, значениями которых являются языки (множества значений этих метапеременных). Символы φ_i,j, i = 1, ..., n, j = 1, ..., k_j, обозначают цепочки в объединенном алфавите терминальных символов и метапеременных:

φ_i,j  (A | { X₁, X₂, ..., X_n})* .

Цепочка φ_i,j рассматривается как некоторое выражение, определяющее значение, являющееся языком (множеством цепочек в алфавите A). Такое выражение определяется следующим образом. Если значения X₁, X₂, ..., X_n заданы, то цепочка

φ = Z₁ Z₂ ... Z_k, Zi(A | { X₁, X₂, ..., X_n }),

обозначает сцепление множеств Z₁ Z₂ ... Z_k, причём вхождение в эту цепочку символа a_j представляет множество из одного элемента {a_j}. Это означает, что φ определяет множество цепочек

{ p₁ p₂ ... p_k | p_jZ_j, j = 1, ..., k},

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

p₁, p₂, ..., p_k

представляет собой последовательность выписанных друг за другом цепочек p₁, p₂, ..., p_k. Таким образом, каждая правая часть уравнений системы (4) представляет собой объединение множеств цепочек.

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

L₁, L₂, ..., L_n

переменных X₁, X₂, ..., X_n, для которых все уравнения системы (4) превращаются в тождество.

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

X = a X  b X  c

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

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

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

L₁ = L  {φ a | φ{a, b}*}

и

L₂ = L  { φ b | φ{a, b}*}.

В соответствии с денотационной семантикой в качестве определяемого решения системы (4) принимается наименьшее. Решение (L₁, L₂, ..., L_n) системы (4) называется наименьшим, если для любого другого решения (L′₁, L′₂, ..., L′_n) выполняется

L₁  L′₁, L₂  L′₂, ..., L_n  L′_n.

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

В качестве метода решения систем уравнений (3) и (4) можно использовать метод последовательных приближений. Сущность этого метода для системы (4) заключается в следующем. Обозначим правые части уравнений системы (4) операторами T_i(X₁, X₂, ..., X_n). Тогда система (4) примет вид

X₁ = T₁(X₁, X₂, ..., X_n),

X₂ = T₂(X₁, X₂, ..., X_n),

(5) ………………………

X_n = T_n(X₁, X₂, ..., X_n).

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

(L₁[0], ..., L_n[0]) = (T₁(L₁[i–1], ..., L_n[i–1]), …………….. (T_n(L₁[i–1], ..., L_n[i–1])).

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

(L₁, ..., L_n)= (T₁(L₁, ..., L_n), ..., T_n(L₁, ..., L_n))

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

T₁, T₂, ..., T_n.

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

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

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

…………………………………………

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

1. Аксиоматическая семантика

В аксиоматической семантике алгебраического подхода система (5) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и / или интерпретации определяемых объектов.

Для интерпретации системы (1) вводится понятие аксиоматического описания (S, E) — логически связанной пары понятий: S — сигнатура используемых в системе (1) символов функций f₁, f₂, ..., f_m и символов констант (нульместных функциональных символов) c₁, c₂, ..., c_m, а E — набор аксиом, представленный системой (1). Предполагается, что каждая переменная x_i, i = 1, ..., k, и каждая константа c_j, j =1, ..., l, используемая в E, принадлежит к какому-либо из типов данных t₁, t₂, ..., t_r, а каждый символ f_i, i =1, ..., m, представляет функцию, типа

t_i1 * t_i2 * ... * t_ik → t_i0.

Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных t_i = t′_i, i = 1, ..., r, и конкретные значения констант c_i = c′_i, i = 1, ..., l. В таком случае говорят, что задана одна конкретная интерпретация A символов сигнатуры S, называемая алгебраической системой

A = (t′₁, ..., t′_r, f ′₁, ..., f ′_r, с′₁, ..., с′ _r),

где f ′_i, i = 1, ..., m, конкретная функция, представляющая символ f_i. Таким образом, аксиоматическое описание (S, E) определяет класс алгебраических систем (частный случай: одну алгебраическую систему), удовлетворяющих системе аксиом E, т.е. превращающих равенства системы E в тождества после подстановки в них f ′_i, i = 1, ..., m, и c_i = c′_i, i = 1, ..., l, вместо f_i и c_i соответственно.

В программировании в качестве алгебраической системы можно рассматривать, например, тип данных, при этом определяемые функции представляют операции, применимые к данным этого типа. Так К. Хоор построил аксиоматическое определение набора типов данных [4], которые потом Н. Вирт использовал при создании языка Паскаль.

В качестве примера рассмотрим систему равенств:

УДАЛИТЬ(ДОБАВИТЬ(m,d))=m,

ВЕРХ(ДОБАВИТЬ(m,d))=d,

УДАЛИТЬ(ПУСТ)=ПУСТ,

ВЕРХ(ПУСТ)=ДНО,

где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ — символы функций, а ПУСТ и ДНО — символы констант, образующие сигнатуру этой системы. Пусть D, D₁ и М — некоторые типы данных, такие, что mM, dD, ПУСТM, ДНО D₁, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M → M,

ДОБАВИТЬ: M * D → M,

ВЕРХ: M → D1.

Данная сигнатура вместе с указанной системой равенств, рассматриваемой как набор аксиом, образует некоторое аксиоматическое описание.

С помощью этого аксиоматического описания определим абстрактный тип данных, называемый магазином, задав следующую интерпретацию символов её сигнатуры: пусть D — множество значений, которые могут быть элементами магазина, D₁ = D | {ДНО}, а M — множество состояний магазина,

M = {d₁, d₂, ..., d_n | d_niD, i = 1, ..., n, n_i0},

Характеристики

Список файлов книги