Next: Metaknowledge Up: Functions and Relations Previous: Abstraction

The universe of a relation is the set of all objects occurring in some list contained in that relation.

`(deffunction universe (?r) :=`` (if (relation ?r)`` (setofall ?x (exists (?l) (and (member ?l ?r)`` (item ?x ?l))))))`

A unary relation is a non-empty relation in which all lists have exactly one item.

`(defrelation unary-relation (?r) :=`` (and (not (empty ?r))`` (forall (?l) (=> (member ?l ?r) (single ?l)))))`

A binary relation is a non-empty relation in which all lists have exactly two items. The inverse of a binary relation is a binary relation with all tuples reversed. The composition of a binary relation and a binary relation is a binary relation in which an object is related to an object if and only if there is an object such that is related to by and is related to by .

`(defrelation binary-relation (?r) :=`` (and (not (empty ?r))`` (forall (?l) (=> (member ?l ?r) (double ?l)))))`

`(deffunction inverse (?r) :=`` (if (binary-relation ?r)`` (setofall (listof ?y ?x) (holds ?r ?x ?y))))`

`(deffunction composition (?r1 ?r2) :=`` (if (and (binary-relation ?r1)`` (binary-relation ?r2)`` (setofall (listof ?x ?z)`` (exists (?y)`` (and (holds ?r1 ?x ?y)`` (holds ?r2 ?y ?z)))))))`

`(defrelation one-one (?r) :=`` (and (binary-relation ?r)`` (function ?r)`` (function (inverse ?r))))`

`(defrelation many-one (?r) :=`` (and (binary-relation ?r)`` (function ?r)))`

`(defrelation one-many (?r) :=`` (and (binary-relation ?r)`` (function (inverse ?r))))`

`(defrelation many-many (?r) :=`` (and (binary-relation ?r)`` (not (function ?r))`` (not (function (inverse ?r)))))`

A unary function is a function with a single argument and a single value. Hence, it is also a binary relation.

`(defrelation unary-function (?f) :=`` (and (function ?f)`` (binary-relation ?f)))`

A binary function is a function with two arguments and one value. Hence, it is a relation with three arguments.

`(defrelation binary-function (?f) :=`` (and (function ?f)`` (not (empty ?f))`` (forall (?l) (=> (member ?l ?f) (triple ?l)))))`

Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994