Новосельцев В.Б. Теория структурных функциональных моделей

Подождите немного. Документ загружается.

ТЕОРИЯ СТРУКТУРНЫХ ФУНКЦИОНАЛЬНЫХ МОДЕЛЕЙ 11

в силу наличия в антецеденте неявных ПВ ”перевычисления аргумен-

тов”), совпадают по n

(X) (по правилу супер пози ци и и в силу φ

)

и, наконец, кортежи обязаны совпадать по X (по правилу суперпози-

ции и в силу наличия неявных ПВ ”перевычисления результатов” вида

G . . . n

(X) → X/Q& −p). Таким образом, мы пришли к противоречию

с высказанным предположением, и правило (4) исчисления SR также

является корректным. 

Перейём теперь к вопросу исследования полноты правил исчисления SR.

Для этого нам надо показать, что если некоторое ПВ не может быть выведено

из информации о схеме S по правилам SR, то это ПВ не удовлетворяет схеме S.

Введём понятие замыкания набора атрибутов относительно схемы S, которое

понадобится нам при доказательстве теоремы о полноте исчисления.

Определение 17. Пусть S(r) = r.(A, X, . . . | fil ter) и пусть A – некоторый

набор атрибутов схемы S. Замыканием A

для A относительно S будем

называть объединение всех таких атрибутов X, что ПВ F : A → X может

быть получено с использованием правил SR из информации о схеме S.

Важное свойство замыкания A

определяется следующей леммой:

Лемма 1. ПВ F : A → X выводимо по правилам SR, если и только если

X ⊆ A

Доказательство Пусть X = x

, . . . , x

и пусть X ⊆ A

. Из определения A

следует, что для каждого i, i = 1, n по правилам SR выводимо ПВ F

: A..., x

, ...,

из которого по правилу сужения (0) может быть получено ПВ F

: A → x

. Ис-

пользуя схему аксиом N : A → A и правило суперпозиц ии, получаем Fi : A →

A, x

. Повторяя эти рассуждения для каждого i, в конце концов, выводим ПВ

F : A → X. Обратное очевидно следует из определения A

. 

Сформулируем и докажем теперь теорему о полноте приведённого исчисле-

ния.

Теорема 4. Исчисление SR является полным относительно понятия ПВ,

удовлетворяющего схеме S.

Доказательство Пусть S – исходная схема и пусть ПВ Ф  F : A → X

не может быть выведено на основании информации о схеме S с помощью пра-

вил SR. Для доказательства теоремы мы должны построить интерпретацию

I такую, что в S |

имеются кортежи s и t, для которых Ф|

имеет смысл и

которые, совпадая по компонентам A|

, различаются хотя бы по одной компо-

ненте из X|

. Рассмотрим интерпретацию I, такую, что в S|

содержаться два

кортежа s и t, компоненты которых совпадают для атрибутов из A

и раз-

личаются для всех прочих атрибутов схемы S. Предположим противное, что

ПВ Ф

 F 1: B → Y является выводимым, но не удовлетворяет S, и опреде-

ляется это на зафиксированных кортежах. Из предположения следует, что Ф

имеет смысл д ля s и t и что B ⊆ A

(в противном случае кортежи не совпали

бы по некоторому атрибуту из B). Кроме того, s и t должны различаться по

компонентам из Y , т. е. Y 6⊂A

(но, вообще говоря, неверно, что Y ∩A

= ∅).

Пусть y-атрибут, y∈Y \A

. Поскольку B ⊆A

, то ПВ G: A → B выводимо по

Лемме 1. Отсюда, с учётом Ф

по правилу суперпозиции имеем G; F

: A → Y ,

значит Y ⊆ A

, а сделанное предположение неверно. Итак, ПВ, выведенные с

помощью правил SR, удовлетворяют исходной схеме.

12 В.Б. НОВОСЕЛЬЦЕВ

Покажем теперь, что Ф не удовлетворяет S, в частности, при интерпретации

I. Предположим обратное. Поскольку A ⊆ A

, заключаем, ч то должно вы-

полняться X ⊆ A

, так как иначе s и t, совпадая по компонентам A |

, не

совпадали бы по компонентам X |

. Отсюда опять по Лемме 1 зак лючаем ,

что ПВ F : A → X может быть выведено по правилам SR. Это противоречит

сделанному предположению, а значит, не удовлетворяет схеме S, в частности ,

на кортежах s и t рассматриваемой интерпретации I. – Таким образом мы

показали полноту правил SR. 

4. Стратегия и алгоритм установления выводимости предложений

Алгоритм, включающий и стратегию вывода, описывается с использовани-

ем некоторого псевдокода, структуры управления которого традиционны для

императивных языков программирования. При описании алгоритма использу-

ются следующие обозначения:

• C

– множество у-атрибутов (развертки) исходной схемы, достижи-

мость которых устан овлен а на тек ущий момент;

• no-аксиома – проблемно-ориентированная или предметная аксиома –

ФС из текущей схемы;

• ”вход в подсхему” – наличие в C

у-атрибутов, которые принадлежат

подсхе ме текущей схемы;

• A

и S берутся из формулировки задачи T .

Описание алгоритма:

«установить i = 0, C

= A

»;

«поднять флаг ”продолжать доказательство” » ;

«текущей схемой объявить S»;

while «поднять флаг ”продолжать доказательство” » do

if «имеется no-аксиома текущей схемы, аргументы которой входят в C

»then

«применить правило суперпозиции, и,

если возможно, правило ветвления»;

«определить C

i+1

: к C

добавить новые у-атрибуты либо изменить

условия достижимости ранее полученных»;

«установить i = i + 1»;

«если определился вход в подсхему, запомнить её в стеке»

else if «имеется подсхема, в которую определён вход» then

«объявить её текущей схемой»

else if «текущая – рекурсивная схема» then

«применить правило введения рекурсии; установить i = i + 1»;

«определить C

i+1

else «объявить текущей внешнюю схему»

ﬁ ﬁ ﬁ

if «текущая – исходная схема S, и больше нет no-аксиом,

аргументы которых входят в C

» then

«опустить флаг ”продолжать доказательство” » ﬁ

od.

Для приведенного алгоритма справедлива

ТЕОРИЯ СТРУКТУРНЫХ ФУНКЦИОНАЛЬНЫХ МОДЕЛЕЙ 13

Теорема 5. Приведённый алгоритм корректен, т.е. обеспечивает нахож-

дение всех выводимых атрибутов. Верхней оценкой сложности алгоритма

является выражение O(|M|

)

Доказательство

(i) Индукцией по i покажем, что если некоторый y-атрибут e помещается

в C

, то e ∈ A

База индукции (i = 0). e ∈ A

, и по схеме аксиом (0) и правилу (1)

получаем A

→ e.

Индукция. Пусть i > 0 и C

состоит из атрибутов, которые принад-

лежат A

. Пусть также на i+1-ом шаге используется ПВ F : B → Y

и e ∈ Y . B ⊆ A

, поскольку B ⊆ C

, следовательно, по Лемме 1 име-

ется G: A

→ B. Используя правила композиции и сужения, получаем

G; F : A

→ e, т. е. e ∈ A

(ii) Покажем теперь, что если y-атрибут e входит в A

, то e попадает в

некоторое C

. Точнее, докажем более общее утверждение: если на осно-

вании информации о схеме S по правилам SR выведено ПВ G :A

→B,

то множество y-атрибутов B содержится в некотором C

Вывод ПВ представляет собой последовательность применений правил

SR к no-аксиомам и ранее полученным предложениям вычислимости

(начальное ПВ N :A

→A

получается в результате использования схе-

мы аксиом). Доказательство проводим индукцией по длине вывода.

База индукции (минимальная длинна вывода).

Вывод заканчивается применением схемы аксиом – A

состоит в точ-

ности из B, очевидно, B ⊆C

. Длинна вывода – два – схема аксиом (0)

и правило сужения (1). – Здесь, очевидно, также B ⊆ C

Индукция. Пред положим, сделанное утверждение ис тинн о для выво-

дов, длина которых не превосходит k, и пусть вывод ПВ Ф  F : A→B

имеет длину k + 1. Если Ф получается по правилу сужения, то B при-

надлежит C

, которое найдётся по предположению для вывода, пред-

шествующего получению Ф. Пусть B получено применением прави-

ла суперпозиции, например, из полученных ранее Ф

 F 1: A→Z и

 f: Z→b (B = Z ∪ b). Вывод каждого из двух последних ПВ име-

ет длину меньше k + 1. Следовательно по п ред пол ожен ию, найдётся

такое C

(i < k + 1), что Z ⊆ C

. По способу введения правила компо-

зиции Ф

является no-аксиомой – функциональной связью из набора

filter исходной схемы S. Отсюда заключаем, что b (а, следовательно,

и B = Z ∪ b) попадает в C

i+j

, где j – числ о применений правил SR

между получением в выводе ПВ Ф

до использования no-аксиомы Ф

(включительно).

(iii) Правила ветвления и введения рекурсии в контексте доказываемой тео-

ремы можно не различать – здесь нам не важен способ подтверждения

предположения, появляющегося в последнем правиле, достаточно про-

сто знать, что мы это делать умеем.

Итак, пусть ПВ Ф  F:A →B получено по правилу ветвления, и длина

вывода равна k +1. Пус ть также Ф п олучен о из Ф

 F

: A→B

, b/Q&p

и Ф

 F

: A→B

, b/Q&−p. Длина вывода как Ф

, так и Ф

меньше

k + 1, следовательно найдутся C

и C

, которые содержат B

, b/Q&p и

14 В.Б. НОВОСЕЛЬЦЕВ

B1, b/Q& −p, соответственно, причём при построении C

и C

обсуж-

даемый алгоритм работает от одних и тех же исходных данных A

Отсюда видно, что атрибуты множества B и, в частности, b \ Q будет

включён в C

max(i,j)+1

, в силу того, что правило ветвления применяется

сразу же, если показана достижимость атрибута при альтернативных

условиях. Поскольку по Лемме 1 принадлежность атрибута e к замы-

канию A

означает выводимость ПВ F : A

→e, можно заключить, что

обсуждаемый алгоритм корректно строит A

. 

Заключение

Как показывает практика, теория С-моделей вкупе с исчислением SR до-

пускает весьма эффективные реализации разнообразных когнитивных систем.

В силу того, что задача установления выводимости тесно связана с нахожде-

нием транзитивных замыканий специальных отношений, естественные вари-

анты реализации опираются на прекрасно зарекомендовавшие себя и весьма

эффективные подходы. Прежде всего, сред и последних имеет смысл выделить

алгоритм Армстронга [8] и алгоритм упоминавшегося ранее Диковского [10].

– В разных модификациях эти алгоритмы обладают полиномиальными оцен-

ками с невысокими сте пен ями (линейные либо квадратичные), хотя и связаны

с существенно более бедными по сравнению с описываемыми здесь моделя-

ми. В первом случае р еч ь идет о связях на атрибутах реляционных схем в

базах данных, а во втором рассматриваются линейные вычислительные моде-

ли. Известно, что наиболее распространенная система непроцедурного (логи-

ческого) программирования [11] базируется на фрагмен те классической логики

предикатов, определяемом формализмом т.н. хорновских дизъюнктов. Не ме-

нее известным является факт неразрешимости классической логики первого

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

сиях системы Пролог определяются внелогическими м еханизмами, подобными

известной операции усечения (cut), и не всегда внятными стратегиями вывода.

Возможность создания в рамках прикладной теории (спецификации Пролога)

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

связанную с классическими исчислениями.

Предлагаемая здесь теория, наследуя свойство полноты исчисления выска-

зываний, является выразительно достаточно мо-щной , чтобы использоваться

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

Список литературы

[1] Кахро М. И., Каля А. П., Тыугу Э. Х. Инструментальная система программирования ЕС

ЭВМ (ПРИЗ). - М.: Финансы и статистика, 1981.

[2] Минц Г.Е. Резолютивные исчисления для неклассических логик. // 9-ый Советский Ки-

бернетический симпозиум, М.:ВИНИТИ. - 1981. - т.2. - с.34-36

[3] Минц Г.Е., Тыугу Э.Х. Полнота правил структурного синтеза. Докл. АН СССР, 1982,

№6. - с.41-60

[4] Фейс Р. Модальная логика. - М.: Наука. - 1974.

[5] Тейз А., Грибомон П., Ж. Луи и др. Логический подход к искусственному интеллекту.

т.2. От модальной логики к логике баз данных. - М.: Мир, 1998.

[6] Дал У., Дейкстра Э., Хоар К. Структурное программирование. - М.: Мир, 1975.

[7] Дейкстра Э. Дисциплина программирования. - М.: Мир, 1978.

[8] Ульман Дж. Основы систем баз данных. - М.: Финансы и статистика, 1983.

ТЕОРИЯ СТРУКТУРНЫХ ФУНКЦИОНАЛЬНЫХ МОДЕЛЕЙ 15

[9] Новосельцев В.Б. Синтез рекурсивных программ в системе СПОРА. Препринт ИТА АН

СССР ”Алгоритмы небесной механики”, №43, Ленинград. - 1985.

[10] Диковский А.Я. Детерминирован ные вычислительные модели. Техническая кибернети-

ка, 1984, № 5, с. 84 - 105.

[11] Робинсон Дж. Машино-ориентированная логика, основанная на принципе резолюции. -

Киб.сб., №7, М.: Мир, - 1970.

Виталий Борисович Новосельцев

Томский политехнический университет,

ул. Ленина 30,

634050, Томск-050, Россия

E-mail address: vbn@osu.cctpu.edu.ru