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

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

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

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

Дата добавления: 2014-01-11