<На страницу назад | На страницу вперед>
А.3 ОСНОВНЫЕ ОПРЕДЕЛЕНИЯ, АКСИОМЫ И СХЕМЫ АКСИОМ
Синтаксис языка детального описания не типизирован; предложения и термы функций представляют просто списки термов без типизации. Но типизация вводится семантически; это значит, что используются аксиомы, обеспечивающие истинность атомарного предложения или обозначение правомерного объекта термом функции только в том случае, если их составляющие термы имеют допустимый вид обозначения. Для этого сначала вводятся соответствующие семантические категории (т.е. типы) и вспомогательные обозначения при использовании ряда операторов "define-relation" и "define-function", затем производится аксиоматизация этих обозначений для сбора соответствующих ограничений типизации. Обратите внимание: эти начальные семантические категории имеют абсолютно общий характер и не зависят от IDEF3. Конкретные семантические категории и определения IDEF3 вводятся в явной форме и аксиоматизируются только после ввода и аксиоматизации этих общих категорий (раздел A.5).
Следует также отметить, что в некоторых базовых семантических категориях KIF (формат обмена знаниями), на основе которых моделируется ядро языка детального описания, отсутствуют множества и списки, которые не нужны в явной форме для поставленных здесь целей. Строго говоря, для обоснования определений необходима теория множеств, поскольку необходимо (или по крайней мере следует) иметь возможность доказать существование определяемых объектов (за исключением случая, когда просто постулируется или вводится объект, существование которого не может быть доказано из данных аксиом). Исключение множества и списков в данном случае отражает идею о том, что пользователи должны иметь возможность выбора собственных теорий множеств; в частности, пользователь может использовать более слабую теорию множеств, чем мощная теория множеств KIF Неймана-Гeделя-Бернайса (Neumann-Godel-Bernays). Хотя необходимость в ассоциированной теории множеств признается, обязанность применения данной теории множеств в данном отчете лишь подразумевается в неявной форме.