;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; If you load this file (with translation into the "KIF" implementation
;;; -- the default ), then the definitions are saved on property lists
;;; and can be used for online documentation and in cross-reference reports.

(in-package "ONTOLINGUA-USER")   ;inherits from the KIF package
                                 ;all constants defined here are exported
                                 ;from the KIF package.

(define-theory KIF-RELATIONS (kif-sets kif-lists)
  "The KIF vocabulary concerning relations and functions.")


(in-theory 'kif-relations)

;;; Functions and relations are defined in the frame ontology.
;;; Inserted here for completeness.

(define-class RELATION (?r)
;;; REDEFINED-IN-FRAME-ONTOLOGY!
  :iff-def (and (set ?r)
                (forall ?x
                    (=> (member ?x ?r)
                        (list ?x)))))

(define-class FUNCTION (?f)
;;; REDEFINED-IN-FRAME-ONTOLOGY!
  :iff-def (and (relation ?f)
                (forall (?l ?m)
                   (=> (member ?l ?f)
                       (member ?m ?f)
                       (= (butlast ?l) (butlast ?m))
                       (= (last ?l) (last ?m))))))


(define-instance BOTTOM (undefined)
  "The unique object which is the value of functions when
applied to arguments on which they are not defined.")


(define-relation HOLDS (?r @args)
  "If $\tau$ denotes a relation, then the sentence 
{\tt (holds $\tau$ $\tau_1$ ... $\tau_k$)} is true if and only if 
the list of objects denoted by $\tau_1$,...,$\tau_k$ is a member of
that relation."
  :iff-def (and (relation ?r)
                (member (listof @args) ?r)))

(define-function VALUE (?f @args)
  "If $\tau$ denotes a function with a value for the objects denoted by
$\tau_1$,..., $\tau_k$, then the term {\tt (value $\tau$ $\tau_1$ ...
$\tau_k$)} denotes the value of applying that function to the objects
denoted by $\tau_1$,...,$\tau_k$.  Otherwise, the value is undefined."
  :lambda-body (if (and (function ?f)
                        (member ?list ?f)
                        (= (butlast ?list) (listof @args)))
                   (last ?list)))


(define-function APPLY (?f ?list)
  :lambda-body (if (and (function ?f) (= ?list (listof @args)))
                   (value ?f @args)))

(define-function MAP (?f ?list)
  :lambda-body (if (null ?list)
                   (listof)
                   (cons (value ?f (first ?list))
                         (map ?f (rest ?list)))))

(define-function UNIVERSE (?r) :-> ?set
  "The universe of a relation is the set of all objects occurring in some
list contained in that relation."
  :lambda-body (if (relation ?r)
                   (setofall ?x
                     (exists (?list) (and (member ?list ?r)
                                       (item ?x ?list))))))

(define-relation UNARY-RELATION (?r)
;;; REDEFINED-IN-FRAME-ONTOLOGY!
 "A unary relation is a non-empty relation in which all lists have
exactly one item."
  :iff-def (and (relation ?r)
		(not (empty ?r))
                (forall (?list) (=> (member ?list ?r) (single ?list)))))

(define-relation BINARY-RELATION (?r)
;;; REDEFINED-IN-FRAME-ONTOLOGY!
  "A binary relation is a non-empty relation in which all lists have
exactly two items."
  :iff-def  (and (relation ?r)
		 (not (empty ?r))
                 (forall (?list) (=> (member ?list ?r) (double ?list)))))


(define-function INVERSE (?r) :-> ?relation
;;; REDEFINED-IN-FRAME-ONTOLOGY!
  "The inverse of a binary relation is a binary relation with all
tuples reversed."
  :lambda-body (if (binary-relation ?r)
                   (setofall (listof ?y ?x) (holds ?r ?x ?y))))

(define-function COMPOSITION (?r1 ?r2) :-> ?relation
;;; REDEFINED-IN-FRAME-ONTOLOGY!
 "The composition of a binary relation $r_1$ and a binary
relation $r_2$ is a binary relation in which an object $x$ is related to an
object $z$ if and only if there is an object $y$ such that $x$ is related to
$y$ by $r_1$ and $y$ is related to $z$ by $r_2$."
  :lambda-body (if (and (binary-relation ?r1)
                        (binary-relation ?r2))
		   (setofall (listof ?x ?z)
			     (exists (?y)
				     (and (holds ?r1 ?x ?y)
					  (holds ?r2 ?y ?z))))))

(define-relation ONE-ONE (?r)
  :iff-def (and (binary-relation ?r)
                (function ?r)
                (function (inverse ?r))))

(define-relation MANY-ONE (?r) 
  :iff-def (and (binary-relation ?r)
                (function ?r)))

(define-relation ONE-MANY (?r) 
  :iff-def (and (binary-relation ?r)
                (function (inverse ?r))))

(define-relation MANY-MANY (?r) 
  :iff-def (and (binary-relation ?r)
                (not (function ?r))
                (not (function (inverse ?r)))))

(define-relation UNARY-FUNCTION (?f) 
  "A unary function is a function with a single argument and a single
value.  Hence, it is also a binary relation."
  :iff-def (and (function ?f)
                (binary-relation ?f)))

(define-relation BINARY-FUNCTION (?f)
  "A binary function is a function with two arguments and one value.  Hence, it
is a relation with three arguments."
  :iff-def (and (function ?f)
                (not (empty ?f))
                (forall (?list) (=> (member ?list ?f) (triple ?list)))))