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

В аксиоматической семантике алгебраического подхода система (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.

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

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

M={d1,d2, ... ,dn | di Î D, i=1,...,n, ni0},

ПУСТ={}, ДНО - особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

С аксиоматической семантикой связана логика равенств (эквациональная логика), изучаемая в курсе "Математическая логика". Эта логика содержит правила вывода из заданного набора аксиом других формул (равенств).