Опр. 1. Под функциональным пространством из домена D₁ в домен D₂ будем понимать домен [D₁->D₂], содержащий всевозможные функции с областью определения из домена D₁ и областью значений из домена D₂ :

[D₁ -> D₂] = {f | f : D₁ -> D₂}.

Опр. 2. Под декартовым (или, иначе, прямым) произведением доменов

D₁, D₂, ... D_n будем понимать домен всевозможных n-ок вида

[D₁ × D₂ × ... × D_n]= {(d₁ × d₂ × ... × d_n) | d₁ Î D₁, d₂ Î D₂, d_n Î D_n ...,}.

Опр. 3. Под последовательностью D* будем понимать домен всевозможных конечных последовательностей вида d=(d₁,d₂,...,d_n) из элементов d₁,d₂,...,d_n,... домена D, где n>0.

Опр. 4. Под дизъюнктной суммой будем понимать домен с определением

[D₁+D₂+...+D_n]={ (d_i, i) | d_i Î D_i, 0<i<n+1 },

где принадлежность элементов d_i компонентам D_i однозначно устанавливается специальными функциями принадлежности.

9.4. Формализация семантики языка функционального программирования SML

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

Прежде всего, рассмотрим синтаксис языка SMalL, т.е. перечислим основные типы конструкций, составляющих его.

1. Язык SMalL содержит множество выражений E, которые формализуются посредством БНФ в следующем виде:

E ::= true | false | 0 | 1 | I | -E |

E1==E2 | E1+E2

Заметим, что выражения включают логические (true и false) и целочисленные (в ограниченном объеме: 0 и 1) константы, множество идентификаторов (I), а также операции отрицания (-E), сравнения (E1==E2) и сложения (E1+E2).

2. Кроме того, язык SMalL содержит множество команд С, которые формализуются посредством БНФ в следующем виде:

С ::= I=E | if (E) C1 else C2 |

while(E) C | C1;C2

Отметим, что команды включают присваивание (I=E), условие

(if (E) C1 else C2), цикл с предусловием (while(E) C), а также последовательность команд (C1;C2).

Деление синтаксиса языка SMalL на выражения и команды во многом является условным и служит иллюстративным целям.

Как уже отмечалось, в качестве математической формализации, моделирующей семантику языков программирования (в частности, языка SMalL), будет использоваться теория вычислений Д. Скотта.

9.4.1. Порядок построения формальной модели семантики языка программирования SMalL согласно ранее представленному формальному описанию синтаксиса языка в терминах БНФ

1. Прежде всего, необходимо дать определение синтаксических доменов (т.е. доменов, характеризующих основные синтаксические категории) для идентификаторов (домен Ide), выражений (домен Exp) и команд (домен Com).

2. Следует представить определение вычислительной модели на основе синтаксических доменов.

3. Необходимо перейти к определению семантических функций (E для домена Exp, C для домена Com и т.д.), которые отображают синтаксические конструкции языка программирования в соответствующие им семантические представления.

4. Следует сформулировать определение семантических предложений в терминах смены состояний программы.

Заметим, что при выполнении программы (в частности, написанной на языке программирования SMalL) происходит изменение состояния памяти (m, memory), которое в простейшем случае характеризует соответствие идентификаторов и значений (то есть, по сути, связывание переменной со значением), либо имеет значение unbound (характеризующее отсутствие связи идентификатора со значением, т.е. аналог свободной переменной).

В соответствии с намеченной схемой рассуждений перейдем к описанию синтаксических доменов, которые в полной мере определяют синтаксис языка SMalL:

Ide = {I | I - идентификатор};

Com = {C | C - команда};

Exp = {E | E - выражение}.

Совокупность всех возможных идентификаторов языка SMalL организуем в домен Ide, команд - в домен Com, и, наконец, выражений - в домен Exp.

9.4.2. Вычислительная модель на основе состояний программы языка SMalL

Для наглядности она представлена в виде следующей таблицы 9.1:

Таблица 9.1. Вычислительная модель на основе состояний программы языка SMalL

Заметим, что состояние программы в произвольный момент времени определяется состоянием "памяти" абстрактной машины той или иной формы. При этом под памятью понимается отображение из домена идентификаторов в домен значений (т.е. аналог связывания переменной со значением в ламбда-исчислении). Для корректной обработки исключительных ситуаций, возникающих в случае свободных переменных, вводится дополнительный элемент unbound. Домен значений представляет собой дизъюнктную сумму доменов, содержащих существующие в языке SMalL типы Int и Bool.

9.5. Описание семантических предложений