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)))))`

Wed Dec 7 13:23:42 PST 1994