Операционная семантика.

В операционной семантике алгебраического подхода к описанию семантики функций рассматривается следующий частный случай системы равенств (5.1):

f1(x1, x2, ... , xk)= E1,

. . . . . . . . . . . . . (5.3)

fn(x1, x2, ... , xk)= En,

где в левых частях этих равенств явно указаны определяемые функции, каждая из которых зависит (для простоты) от одних и тех же параметров

x1, x2, ..., xk,

а правые части этих равенств представляют собой выражения, содержащие, вообще говоря, вхождения этих функций, т.е. определяемые функции могут быть рекурсивными. Поэтому определяемая функция может иметь дополнительные вхождения в левые части этой системы равенств с постоянными значениями некоторых параметров. Таким образом, каждый параметр xj вхождения определяемой функции fi в левую часть равенств (5.3) будем понимать либо как переменную yj, либо как константу cij, причём совокупность переменных

y1, y2, …, yk

представляет входные данные, для которых требуется вычислять определяемые функции.

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

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.

На первом шаге осуществляется подстановка этих данных в левые и правые части равенств с выполнением там, где это возможно, предопределённых операций и с переписыванием получаемых в результате этого равенств. В результате этого будет сформирована исходная преобразуемая система равенств.

На каждом следующем шаге по текущей преобразуемой системы равенств производится формирование новой преобразуемой системы равенств (которая становится текущей)путем переписывания этих равенств со следующими преобразованиями.

(1) Если правая часть очередного равенства является каким-либо значением, то это равенство не изменяется (это значение и является значением функции, указанной в левой части этого равенства).

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

(2.1) Если для этого вхождения в текущей преобразуемой системе равенств находится совпадающая с ним левая часть некоторого равенства, то проверяется правая часть этого равенства

(2.1.1) и в случае, если она является уже вычисленным значением, производится подстановка этого значения вместо указанного вхождения определяемой функции,

(2.1.2) если же эта правая часть не является вычисленным значением, то указанное вхождение переписывается в неизменном виде.

(2.2) В том же случае, если для указанного вхождения в текущей преобразуемой системе равенств не находится совпадающей с ним левой части никакого равенства, то к новой преобразуемой системе равенств дописывается новое равенство. Это равенство получается из исходного равенства для определяемой функции

fi(y1, y2, …, yk),

вхождение которой в данный момент исследуется, путем подстановки аргументов этой функции из исследуемого вхождения вместо параметров y1, y2, …, yk этой функции (с выполнением предопределённых операций там, где это возможно).

Эти шаги будут осуществляться до тех пор, пока все определяемые функции не будут иметь вычисленные значения.

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