Формальная система теории семантически значимых отображений

А.М. Бабанов

ФОРМАЛЬНАЯ СИСТЕМА ТЕОРИИ СЕМАНТИЧЕСКИ ЗНАЧИМЫХ ОТОБРАЖЕНИЙ

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

Классики баз данных справедливо критикуют существующие семантические модели за их нестрогость, отсутствие однозначных определений основных понятий и тем более формальных систем [1]. Предлагаемая автором семантическая модель «Объект-Отображение» (в дальнейшем кратко - OM-модель от англоязычного ее написания - Object-Mapping Model) [2, 3] лишена этих недостатков. В настоящей статье закладываются основы формальной системы теории семантически значимых отображений (ТСЗО). Дальнейшее развитие этой системы (в основном за счет расширения системы аксиом и теорем) будет происходить параллельно с развитием ТСЗО и OM-модели.

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

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

Атомами формальной системы теории семантически значимых отображений являются:

- предикат вида х = у (истинен тогда и только тогда, когда предметные переменные х и у указывают на один и тот же объект);

- предикат вида у = ф(х) (истинен тогда и только тогда, когда объект у является образом объекта х при отображении ф);

- предикат вида R(xj,...,xn), где R - отображение

R : Xj x ...x Xn ^ {0,1} (истинен тогда и только тогда, когда кортеж объектов x1,...,xn принадлежит OM-отношению R).

Для построения формул используются традиционные для исчисления предикатов первого порядка синтаксические правила, традиционны также правила вывода, основным из которых является правило «модус поненс»: из формул ф и ф^-у выводится формула у.

Для доказательства теорем ТСЗО и ее взаимосвязей с теорией реляционных БД используется метод резолюций, поэтому аксиомы теории представляются в стандартной предикатной форме в виде множества дизъюнктов. Первые выводы теории получены из рассмотрения тернарного случая (рис. 1), при котором имеется три класса объектов (X, Y, Z), четыре отношения (одно тернарное - R(X,Y,Z) и три бинарных -Rxy(X,Y), Ryz(Y,Z), Rxz(X,Z)) и двадцать отображений (восемь из них определяет отношение R и по четыре -каждое из бинарных):

у1 : X -> Y x Z, у-1: Y x Z -> X, у2: Y -> X x Z, у-1: X x Z -> Y,

у3: Z -> X x Y, у-1: X x Y -> Z,

R : X x Y x Z ^ {0,1} , R- :{0,1} ^ X x Y x Z ,

ф1 : X -> Y, ф1-1 : Y -> X,

RXY : X x Y ^ {0,1}, Rxy- :{0,1} ^ X x Y ,

ф2: Y -> Z, ф-1: Z -> Y, RYZ : Y x Z ^ {0,1} , Ryz- :{0,1} ^ Y x Z ,

ф3: Z -> X, ф-1: X -> Z, RXZ : X x Z ^ {0,1}, RXZ- : {0,1} ^ X x Z .

Ф21 Ф2

Рис. 1. Тернарный случай

Первую часть аксиом ТСЗО составляют общезначимые формулы, связанные с операциями над отображениями.

Для инверсии отображений формула

УхУу(у = ф(х) ^ х = ф-1 (у)) порождает дизъюнкты

-У = ф( х) V х = ф-1( у), у = ф( х) V х = ф-1( у).

Для композиции отображений формула УхУ2 (2 = у(ф(х)) ^ Зу(у = ф(х) Л 2 = у(у))) порождает дизъюнкты

-2 = у (ф(х)) V/(х, 2) = ф(х) ,

-2 = у (ф(х)) V 2 = у (/(х, 2)) ,

где /х, 2) - функция Скулема,

2 = у (ф(х) V -у = ф(х) V -2 = у (у) .

Для объединения отображений формула УхУу(у = (фи у)(х) о у = ф(х) V у = у(х)) порождает дизъюнкты

-у = (фиу)(х) Vу = ф(х) Vу = у(х),

у = (фи у)(х) V -у = ф(х), у = (фи у)(х) V -у = у(х).

Для пересечения отображений формула УхУу(у = (фП у)(х) о у = ф(х) Л у = у (х)) порождает дизъюнкты

-у = (ф П у)(х) V у = ф(х),

-у = (ф П у)( х) V у = у (х), у = (фП у)(х) V -у = ф(х) V -у = у(х).

Для разности отображений формула УхУу(у = (ф - у)(х) о у = ф(х) Л -у = у (х)) порождает дизъюнкты

-у = (ф-у)(х) V у = ф( х),

-у = (ф - у)(х) V -у = у (х), у = (ф - у)(х) V -у = ф(х) V у = у (х).

Для проекции отображения формула

УхУу(у = ф[7](х) о 32(< у, 2 >= ф(х))) порождает дизъюнкты

-у = ф[^](х^ < у, /(х, у) >= ф(х), где /(х, у) - функция Скулема,

у = ф[^](х) V -< у, 2 >= ф(х).

Вторую группу аксиом составляют общезначимые формулы, представляющие тот факт, что одно отношение степени п определяет 2п отображений. В рассматриваемом нами тернарном случае общезначимыми будут следующие утверждения и порождаемые ими дизъюнкты.

УхУуУ2

Лх = у-1

-Я

-Я

- Я

-Я

-Я

-Я

УхУуУ2(<у,2 >=у1 (х^х = у-1 (у,2^<х,2>=у2 (у) V у=у21(х,2К<х,у>=уз(2^2=у-1(х,у)^Я(х,у,2)):

Я

Я

Я

Я

Я

Я

УхУу(Яху (х, у) ^ у = ф1(х) л х = ф11 (у)):

-Яхт

-Яхт

УхУу(у = ф1(х) V х = ф-1 (у) ^ Яхт (х, у)):

Яхт

Яхт

УуУ2(Ят2 (у, 2) ^ 2 = ф2(у) Л у = ф-1 (2)):

-Ятх

-Ятъ

УуУ2 (2 = ф2(у) V у = ф-1 (2) ^ Ятг (у, 2)):

Ятъ

Ятъ

УхУ2(Яхг (х, 2) ^ х = ф3(2) Л 2 = ф-1 (х)):

-Яхъ

-Яхх

УхУ2(х = ф3(2) V 2 = ф-1 (х) ^ Яхг (х, 2)):

Яхх

Яхг(х,2)V-2 = ф-Чх).

Предлагаемая формальная система прошла проверку доказательством теорем. Методом резолюций во введенной формальной системе доказаны следующие теоремы.

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

Право осуществления подобных действий нам дает истинность следующих формул:

УхУуУ2

- условие многозначной зависимости х -> т | 2 и УхУуУ2

- условие зависимости соединения *(хт, т2, х2).

Теоремы 1 и 2 вводят эквивалентные аналоги этих выражений в ТСЗО.

Теорема 1. Следующие формулы являются логическими следствиями друг друга:

УхУуУ2(Я(х, у, 2) о Яхт (х, у) Л Ях2 (х, 2)) и УхУуУ2(< у, 2 >= у1 (х) о у = ф1 (х) Л 2 = ф-1 (х)) .

Теорема 2. Следующие формулы являются логическими следствиями друг друга:

УхУуУ2 (Я( х, у, 2) о Яхт (х, у) Л Ятг (у, 2) л Яхг (х, 2)) и

УхУуУ2 (< у, 2 >=у1 (х) о у = ф1 (х)л 2 = ф2 (у) Л х = ф3 (2 )) .

Следующие две теоремы служат основанием для декомпозиции без потерь функциональных зависимостей.

Теорема 3. Отображение у1 функционально тогда и только тогда, когда функциональны обе ее проекции

у1 [т ] и у^г ].

Теорема 4. Если отображения ф1 и ф-1 функциональны и являются следствиями проекций у1[т] и у1[г ] соответственно, то функциональны и проекции у1 [т ] и у№ ].

Следствие теорем 3 и 4 гарантирует функциональность отображения у1 при декомпозиции отношения Я(х, у, 2) на отношения Яхт (х, у) и Ях2 (х, 2), в которых отображения ф1 и ф-1 функциональны.

Следствие теорем 3 и 4. Если отображения ф1 и ф-1 функциональны и являются следствиями проекций у1[т] и у1[г] соответственно, то функционально отображение у1 .

Теорема 5 обеспечивает условия декомпозиции отношения Я(х, у, 2) на отношения Яхт (х, у) и

Ях2 (х, 2) без потерь информации при наличии функциональных отображений.

Теорема 5. Если одна из проекций отображения у1 функциональна, и обе проекции эквивалентны соответствующим бинарным отображениям, то выполняется условие эквивалентности схемы отношения Я(х, у, 2) схеме с отношениями Яхт (х,у) и

Яхг(2).

Теорема 6 обеспечивает условия декомпозиции отношения Я(х, у, 2) на отношения Яхт (х, у) и Ях2 (х, 2) без потерь информации.

Теорема 6. Условие эквивалентности схемы отношения Я( х, у, 2) схеме с отношениями Яхт (х, у) и Ях2 (х, 2) выполняется тогда и только тогда, когда отображения ф1 и ф-1 являются следствиями проекций у1[т] и у1[г] соответственно, и истинно следующее высказывание:

УхУуУ2(у = ф1(х) Л 2 = ф-1 (х) ^< у, 2 >= у1 (х)) .

ЛИТЕРАТУРА

1. Дейт К. Введение в системы баз данных. 7-е изд.: Пер. с англ. М.: Вильямс, 2001. 1072 с.

2. Бабанов А.М. Теория семантически значимых отображений // Вестник ТГУ. 2003. № 280. С. 239 - 248.

3. Бабанов А.М. Применение теории семантически значимых отображений для проектирования реляционных баз данных // Вестник ТГУ. 2003. № 280. С. 249 - 257.

Статья представлена кафедрой теоретических основ информатики факультета информатики Томского государственного университета, поступила в научную редакцию «Информатика» 25 мая 2005 г.