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

;;; Quantity Space
;;; (c) 1993 Greg Olsen and Thomas Gruber

(in-package "ONTOLINGUA-USER")

(define-theory quantity-spaces (physical-quantities)
  "A quantity-space is a set that has the property that a distance function is
defined for any two elements in the set.  In addition, the range of the
distance function is a subclass of the class of scalar quantities.

This theory defines the class of quantity-space, and the associated
relations POINT-IN, DISTANCE.  It is agnostic about the semantics
of the points -- they needn't be spatial things or of any particular
dimensionality."
  :issues ("Copyright (c) 1994 Greg R. Olsen and Thomas R. Gruber"
	   (:see-also "The EngMath paper on line")))

(in-theory 'quantity-spaces)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Quantity Space
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-class QUANTITY-SPACE (?s)
  
  "A quantity-space is a set that has the property that a distance function is
defined for any two elements in the set.  In addition, the range of the
distance function is a subclass of the class of scalar quantities."
  
  :iff-def (and (set ?s)
		(forall (?x1 ?x2)
			(=> (and (member ?x1 ?s)
				 (member ?x2 ?s))
			    (exists (?d)
				    (and
				     (= ?d (distance ?x1 ?x2))
				     (scalar-quantity ?d)))))))


(define-relation POINT-IN (?pt ?sp)
  "A point in a quantity-space is simply an element in the set
that is the quantity-space."
  :iff-def (and (quantity-space ?sp)
		(member ?pt ?sp)))


(define-function DISTANCE (?x1 ?x2) :-> ?d
  "The DISTANCE function is intended to be polymorphically
defined for each quantity space.  Its always maps two
points in the space to a scalar-quantity.  It must be
commutative."
  :def (and (exists (?sp)
		    (and (quantity-space ?sp)
			 (point-in ?x1 ?sp)
			 (point-in ?x2 ?sp)))
	    (scalar-quantity ?d))

  :axiom-def (and (zero-quantity (distance ?a ?a))
		  ;; commutivity
		  (= (distance ?b ?c)
		     (distance ?c ?b))))