Methods IDEF3

А.1.3 Термы
Язык детального описания IDEF3 обеспечивает поддержку выражений трех типов: термы (term), предложения (sentence), определения (definition). Терм обозначает объект некоторого вида, хотя сам язык (в отличие от языков с высоким уровнем типизации) не определяет точно вид объекта; вид объекта определяется отдельно посредством специальных аксиом (как показано ниже). Термы делятся на две категории:

Атомарные термы (Atomic Term): Эта категория включает все основные простые типы языка, т.е. идентификаторы (identifier), переменные (variable), целые числа (int), числа с плавающей точкой (float), строки (string).
Сложные термы (Complex Term): Сложный терм - это терм, который формируется из простых термов и (возможно) предложения и/или оператора. Простейший вид сложного терма представляет просто список идентификаторов. Грамматика данного языка позволяет формировать такие термы независимо от того, что именно эти термы означают. Так, можно сформировать терм "(Plato Socrates)". Однако, сложный терм этого вида, содержащий n+1 термов, семантически имеет смысл только в том случае, если первый терм представляет n-местную функцию.

Следовательно, в семантике языка детального описания терм "(Plato Socrates)" (если предположить, что термы "Plato" и "Socrates" означают философов Платона и Сократа) будет считаться бессмысленным; точнее говоря, этот терм будет
обозначать специальный "пустой" индивид, который называется "неопределенной величиной" (null).

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

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

означает Галена при условии if?x меньше 18; в противном случае означает сестру Галена. Термы, формируемые при использовании оператора cond, работают подобным образом, только они разрешают спецификацию множества условий. Предположим, Лэрри говорит о каком-то неспецифицированном политике. Поскольку существует только один такой политик, о котором он говорит (предположим), соответствующему терму данного политика может быть дано полное определение:

Если дополнительно знать, что объект внимания Лэрри должен быть президентом, вице-президентом или спикером палаты представителей (в августе 1995 г.), то данный объект можно обозначить более конкретно посредством сложного терма:

который обеспечивает выбор Билла Клинтона, если Лэрри говорит о президенте, Ала Гора, если Лэрри говорит о вице-президенте, и Ньюта Гинриха, если Лэрри говорит о спикере. Такие термы особенно полезны в ситуациях, когда известно, что данный объект в данной ситуации должен быть одним из нескольких объектов, который можно отличить при соответствующих условиях. Не зная конкретно, что это будет, можно, тем не менее, сформировать терм, обеспечивающий правильный выбор объекта, в зависимости от того, какое условие действует.

Остальные операторы представляют операторы "связывания переменных" (variable binding), т.е. они используют переменную и некоторое условие, включающее переменную или переменные, которые они связывают для спецификации значения. the формирует терм "определить описание" (define description) и обозначает уникальный объект, удовлетворяющий данному описанию. Например, (the ?x (current-U.S.- president ?x)) обозначает Билла Клинтона (в 1995 г.). Обратите внимание: необходимым и достаточным условием для того, чтобы терм определения описания "(the ?x j)" (где j - любое "описание" (т.е. предложение, как показано ниже)) имел определенное значение, является условие, в соответствии с которым имеется один и только один предмет, который описывается посредством j. Следовательно, поскольку существует множество политиков, терм "(the ?x (politician ?x))" не имеет конкретного значения; в семантике языка детального описания он означает "пустой" объект, т.е. имеет неопределенное значение (null).

Подобным образом, number-of используется для формирования термов, обозначающих определенное число предметов, удовлетворяющих определенному описанию. Так,

обозначает число из группы целых чисел, которое больше 0 и меньше 5, т.е. число 4.

lambda и kappa используются для формирования термов, которые, будучи семантически значимыми, обозначают функции и отношения. Так, при использовании символа "*" для обозначения умножения терм

обозначает 2-местную функцию, которая использует пару чисел m и n для суммы m и квадрата n. Подобным образом, оператор kappa позволяет сформировать термы для сложных свойств и отношений. Так, терм

представляет отношение владения между домовладельцем и его домом.

Как уже отмечалось, термы, сформированные из kappa, где kappa связывает только одну переменную, обозначают свойства или виды (kind). А поскольку объектные состояния представляются как подкласс видов, их также можно рассматривать как свойства. Следовательно, в этих случаях соглашение должно допускать использование kind-of для обозначения видов и состояний. Так, например,

обозначает вид "человек старше 40, но моложе 60". Подобным образом,

представляет способ выражения (на языке детального описания) состояния, которое определяется посредством "человек: спящий" (person: sleeping) в схематике переходов состояний.

Нетипизированный язык с использованием операторов, подобных lambda и kappa, конечно, является первым кандидатом на парадокс. Например, синтаксис данного языка разрешает формирование терма

который представляет неизвестное свойство Рассела "отрицание самого себя" (nonselfexemplification), свойство, истинное только для тех свойств, которые сами являются истинными. Однако, такие свойства могут вызвать затруднение только в контексте логики, из которой вытекает парадокс; в частности, логика, которая включает "наивный" принцип полноты (comprehension) (<=> j[var/term] ((kappa var j) term)), где j[var/term] представляет результат замены всех свободных вхождений переменной var в предложении j термом. (Вхождение переменной var в предложение или терм e происходит свободно в e в том случае, если оно не происходит в рамках выражения, имеющего форму (OP var y ) или (OP (var1 ... var ... varn) y ) или OP (var1 ... var ... varn : q) y ) в e, где OP представляет (в первой форме) term-op 'the' или один из числовых кванторов 'exists-1', 'exists!-1', 'exists-2', exists!-2' и т.д., или (в любой из трех форм) один из кванторов 'forall', 'exists'.). Мы допускаем применение некоторой приемлемой логики, в которой такие парадоксы исключены. (Точнее говоря, исключены, насколько нам известно. По причинам, впервые открытым в известной работе логика Курта Гeделя, невозможно доказать (без голословных утверждений), что какая-либо достаточно эффективная теория свободна от противоречий. См. [Godel 31] или [Enderton 72], глава 3 - на английском языке).