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

В аксиоматической семантике алгебраического подхода система (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₁ D Î M, ДНО Î D, ПУСТ Î M, d Î и М — некоторые типы данных, такие, что m₁, а функциональные символы представляют функции следующих типов:

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

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

ВЕРХ: M → D1.

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

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

M = {d₁, d₂, ..., d_n | d_niD, i = 1, ..., n, n Î _i0},

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

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