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

Замечание. Из сказанного следует, что отличие между модельно-теоретическим и доказательно-теоретическим подходами состоит в том, что, в то время как с модельно-теоретической точки зрения база данных может иметь несколько смысловых значений , с доказательно-теоретической точки зрения она обычно обладает в точности одним смысловым значением . Это верно за исключением двух случаев: когда, как уже упоминалось ранее, единственное значение является каноническим с модельно-теоретической точки зрения, а также когда единственное значение с доказательно-теоретической точки зрения прекращает быть истинным, если в базе данных содержатся какие-либо отрицаемые аксиомы [23.9], [23.10].

Ниже в неформальном виде перечислены аксиомы рассматриваемой в данном примере базы данных [23.15] (с доказательно-теоретической точки зрения).

1. Основные аксиомы, соответствующие значениям доменов и кортежей в базовых переменных-отношениях, которые называются экстенсиональной базой данных (extensional database).

2. Аксиома дополнения для каждой переменной-отношения, которая утверждает, что для любого кортежа, отличного от допустимого для данной переменной-отношения, соответствующее ей утверждение является ложным. (Фактически эти аксиомы дополнения, взятые вместе, составляют допущение о замкнутости мира, которое уже рассматривалось в главе 5.) Например, если в переменную-отношение поставщиков S не включен кортеж (S6, White, 45, Rome), то утверждение Существует поставщик с номером S6 по имени White, который имеет статус 45 и проживает в городе Rome является лолсяьш.

3. Аксиома уникального имени , которая утверждает, что каждая константа отлична от других (т.е. обладает уникальным именем).

4. Аксиома замкнутости доменов , которая утверждает, что не существует никаких других констант, кроме упомянутых в доменах базы данных.

5. Набор аксиом (по сути стандартных) для определения встроенного предиката равенства -. Эти аксиомы обязательны, поскольку в аксиомах 2-4 используется предикат равенства.

В заключение следует перечислить принципиальные различия между двумя точками зрения - модельно-теоретической и доказательно-теоретической. Но прежде всего следует отметить, что с чисто практической точки зрения между ними нет существенной разницы, по крайней мере в понятиях современных СУБД.

Аксиомы 2-5 из приведенного выше перечня согласно доказательно-теоретическому подходу указывают, что некоторые допущения являются явными, хотя с точки зрения модельно-теоретического подхода они неявные [23.15]. Вообще говоря, явное задание аксиом довольно удобно и, более того, даже не-

обходимо для явного задания дополнительных аксиом, которые используются для таких общих методов доказательства, как описанный в разделах 23.3 и 23.4 метод резолюции.

Следует отметить, что в аксиомах не упоминаются ограничения целостности. Дело в том, что с доказательно-теоретической точки зрения при добавлении таких офаничений СУБД становится дедуктивной. Подробнее об этом речь идет в разделе 23.6.

Доказательно-теоретическое представление, в отличие от модельно-теоретического, обладает некоторой элегантностью, состоящей в едином представлении нескольких конструкций, которые обычно рассматриваются как в какой-то мере разные: базовые данные, запросы, офаничения целостности (несмотря на сказанное в предыдущем пункте), виртуальные данные и т.д. Это позволяет создавать в большей степени единообразные интерфейсы и приложения.

С помощью доказательно-теоретического подхода можно решать проблемы, которые невозможно решить на основе реляционных систем, например обрабатывать дизъюнктивную информацию типа Поставщик с номером S6 проживает либо в городе Paris, либо в городе Rome , извлекать отрицаемую информацию наподобие Кто не является поставщиком? и обрабатывать рекурсивные запросы, которые будут описаны ниже. Однако в отношении последнего случая (как минимум) нет никаких принципиальных офаничений для соответствующего расширения классической реляционной системы с целью выполнения таких запросов. Более того, в нескольких коммерческих продуктах их поддержка уже реализована (см. также приложение Б). Подробнее эти вопросы рассматриваются в разделах 23.6 и 23.7.

Наконец, цитируя работу Рейтера (Reiter) [23.15], можно сказать, что доказательно-теоретический подход обеспечивает корректную обработку расширений реляционной модели для более широкого включения семантики реального мира (как уже отмечалось в разделе 23.22).

23.6. Дедуктивные СУБД

Дедуктивная СУБД- это СУБД, в которой поддерживается доказательно-теоретический подход к базам данных и которая, в частности, позволяет вывести дополнительные факты из экстенсиональной базы данных с помощью специализированных дедуктивных аксиом, или правил вывода, примененных к известным фактам*. Дедуктивные аксиомы вместе с ограничениями целостности (они будут описаны ниже) образуют интенсиональную базу данных (intensional database). Экстенсиональная и интенсиональная базы даьтых вместе составляют дедуктивную базу данных (это не совсем удачное название, поскольку на самом деле выводы делает именно СУБД, а не база данных).

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

В этой связи стоит заметить, что еще в 1974 году Кодд утверждал, что одной из задач реляционной модели является, несомненно, поглощение фактов выборки и управления файловыми полями для пополнения в дальнейшем логического сервиса в коммерческом мире [11.2], [25.8].

Рассмотрим, как будет выглядеть база данных поставщиков и деталей, преде влен-ная на рис. 3.8, в форме дедуктивной СУБД . Прежде всего следует определить набор основных аксиом, которые задают допустимые значения домена.

Замечание. Далее для лучшей читабельности будут использоваться по существу те же соглашения относительно представления значений, которые применялись, например, на рис. 3.8, и поэтому в качестве сокращения для записи QTY(300) будет использоваться просто 300 и т.д.

и т.д.

Затем следует задать основные аксиомы для кортежей базовых отношений.

S ( S1, Smith, 20, London ) S ( S2, Jones, 10, Paris ) и т.д.

P ( Pl, Nut, Red, 12, London ) и т.д.

SP ( Sl, РГ, 300 ) и т.д.

Замечан14е. Конечно, здесь всерьез не предполагается, что экстенсиональная база данных будет построена на основе всего лишь явного перечисления всех основных аксиом, как показано выше. Для этого, скорее всего, будет использовано традищ10нное определение и тради-шюнные методы ввода данных. Иначе говоря, дедуктивные СУБД применяют свои выводы для традиплонных баз данных, которые уже существуют и построены самым обычным способом. Однако следует обратить внимание на чрезвычайно важный факт: экстенсиональная база данных не нарушает заданных офаничений целостности, поскольку база данных, нарушающая эти Офаничения, представляет (на языке логических терминов) несовместимый набор аксиом. Таким образом может быть доказана истинность абсолютно любого утверждения, каким бы оно ни было (другими словами, могут быть выведены противоречия). По той же причине очень важно, чтобы набор офаничений целостности был совместимым.

Теперь перейдем к описанию интенсиональной базы данных. Для нее существует следующий набор ограничений домена.

S ( S, sn, st, sc )

S# ( s ) AND NAME ( sn ) AND STATUS ( St ) AND CITY ( so )