<На страницу назад | На страницу вперед>
А.3.1 Основные семантические категории
В данном разделе вводятся основные семантические категории; индивид (individual),
функция (function), отношение (relation), а также неопределенный
объект (null object) - специальный объект, используемый только для указания,
что некоторый терм не имеет подлинного обозначения.
(define-relation individual (?x))
(define-relation list (?x))
(define-relation relation (?x))
(define-individual null)
(define-relation function (?x))
:=> (relation ?x))
(define-relation interval (?x)
:=> (individual ?x))
(define-relation integer (?x)
:=> (individual ?x))
Большинство формализаций, включающих функции, определяют функции как отношения определенного вида. Так, при рассмотрении с использованием теории множеств (например, KIF), двухместное отношение представляет множество упорядоченных пар, а функция представляет просто двухместное отношение; так что первый элемент любой данной пары в данном отношении не образует также пару с любым другим объектом. Формально эта идентификация очень удобна. Поэтому эта идентификация добавляется как определяющая аксиома для функций. Подобным образом, интервалы и целые числа используются как виды индивидов.
Двойственность функций, которые представляются и как функции, и как отношения, фиксируется в следующей серии аксиом:
Два объекта находятся в (двоичном) функциональном отношении
f тогда и только тогда, когда значение f, применимое к первому объекту, является
вторым.
(Two objects stand in the (binary) functional relation f iff the value of f
applied to the first object is the second).
(forall (?x ?y ?f : (function ?f)) (<=> (?f ?x ?y) (= (?f ?x) ?y))))
Три объекта находятся в (троичном) функциональном отношении
f тогда и только тогда, когда значение f для двух первых объектов является третьим.
(Three objects stand in the (ternary) functional relation f iff the value of
f on the first two objects is the third).
(forall (?x ?y ?z ?f : (function ?f)) (<=> (?f ?x ?y ?z) (= (?f ?x ?y) ?z))))
Как правило, мы имеем следующую схему аксиом:
(forall (?var1 . . . ?varn+1 ?f : (function ?f))
(<=> (?f ?var1 . . . ?varn+1) (= (?f var1 . . . ?varn) ?varn+1))))