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

;;; Scalar Quantities 
;;; (c) 1993 Greg Olsen and Thomas Gruber 

(in-package "ONTOLINGUA-USER") 

(define-theory scalar-quantities (physical-quantities) 

"The term 'scalar' is often equated with the field of real numbers. 
In this theory we extend that notion to quantities in general, which 
are associated with dimensions and units. 
Scalar quantities are quantities whose magnitude is a real number, 
such as 'the length of rod a'.  The normal operators for real 
arithmetic such as + and *, and the relation <, are extended 
to the case of scalar quantities (i.e., to consider dimensions and units). 
Scalar-Quantities are disjoint from vectors quantities, and scalar functions.") 

(in-theory 'scalar-quantities) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;;; Scalar-Quantities 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

(define-class SCALAR-QUANTITY (?q) 

  "A scalar-quantity is a constant quantity whose magnitude is a real 
number.  An important property of scalar-quantities is that they form 
a field with respect to the addition and multiplication (with proper 
subclass restrictions).  The class of scalar-quantities forms a 
partial order with the less-than relation <, since < is a 
relation-extended-to-quantities and < is defined over the reals.  The 
< relation is not a total order over the class of scalar-quantity 
since elements from some subclasses such as length quantities are 
incomparable to elements from other subclasses such as mass 
quantities." 

   ;; all scalar-quantities are quantities whose magnitude is a real number 
  :iff-def (and (constant-quantity ?q) 
		(forall ?u 
                   (=> (and (unit-of-measure ?u) 
                            (compatible-quantities ?u ?q)) 
                       (real-number (magnitude ?q ?u))))) 

  :axiom-def (and (superclass-of scalar-quantity real-number) 
		  (partial-order scalar-quantity <))) 



(define-instance IDENTITY-SCALAR (scalar-quantity) 

  "The 'one' element for scalar-quantites or the identity element with 
respect to multiplication.  This element is unique and common to all 
scalar-quantities regardless of associated physical dimension. 
Therefore this element is equal to the number 1. The axioms tell us 
that the product of any scalar-quantity x and the identity-scalar is x." 

  := 1 
  :axiom-def (and (= (quantity.dimension identity-scalar) identity-dimension) 
                  (identity-element-for identity-scalar 
					*  
					scalar-quantity))) 



(define-function + (?x ?y) :-> ?z 

  "+ defines the specialization of the quantity addition operator + 
for scalar-quantities.  The operator enforces the restriction that the 
quantities be compatible.  The operator is defined in terms of the 
number addition operator + and the magnitudes of quantities for a 
particular unit.  Scalar-Quantities of a common dimension form an 
abelian group with respect to this operator and the zero-scalar of the 
same physical dimension." 

  :when (and (scalar-quantity ?x) 
             (scalar-quantity ?y)) 

  :iff-def (and (scalar-quantity ?z) 
                (forall ?u 
                  (=> (and (unit-of-measure ?u) 
                           (compatible-quantities ?x ?u)) 
                      (= (+ (magnitude ?x ?u)  
                            (magnitude ?y ?u)) 
                         (magnitude ?z ?u))))) 
   
  :axiom-def (forall ?d 
               (=> (physical-dimension ?d) 
                   (abelian-group  
                     (scalar-quantities-of-dimension ?d) 
                     + 
                     (the-zero-scalar-for-dimension ?d))))) 


(define-function * (?x ?y) :-> ?z 

  "* defines the specialization of the quantity 
multiplication operator * for scalar-quantities.  The operator enforces the 
relationship between the physical-dimensions of the operands and the 
product.  The operator is defined in terms of the number 
multiplication operator * and the magnitudes of quantities for a 
particular unit.  Scalar-Quantities excluding all the zero-scalars form an 
abelian group with respect to this operator and the identity-scalar 
<1>.  This operator distributes over the + operator for scalar-quantities, 
providing a field behavior with restrictions." 

  :when (and (scalar-quantity ?x) 
             (scalar-quantity ?y)) 
  :iff-def (and (scalar-quantity ?z) 
                (forall (?u ?u1 ?u2) 
                   (=> (and (unit-of-measure ?u) 
                            (compatible-quantities ?x ?u) 
                            (unit-of-measure ?u1) 
                            (compatible-quantities ?y ?u1) 
                            (unit-of-measure ?u1) 
                            (= (quantity.dimension ?u2) 
                               (* (quantity.dimension ?u) 
                                  (quantity.dimension ?u1)))) 
                       (= (* (magnitude ?x ?u1)  
                             (magnitude ?y ?u2)) 
                          (magnitude ?z ?u))))) 
  :axiom-def (abelian-group  
               (kappa (?x) 
                      (and (scalar-quantity ?x)  
                           (forall ?dim  
                                   (=> (physical-dimension ?dim) 
                                       (/= (the-zero-scalar-for-dimension ?dim)  
                                           ?x))))) 
               * 
               1)) 

(define-function - (?x) :-> ?y 

  "- defines the specialization of the quantity additive 
inverse operator for scalar-quantities." 

  :when (scalar-quantity ?x) 
  :def (and (scalar-quantity ?y) 
            (= (+ ?x ?y)  
               (the-zero-scalar-for-dimension (quantity.dimension ?x))) 
            (forall ?u 
                    (=> (and (unit-of-measure ?u) 
                             (compatible-quantities ?x ?u)) 
                        (= (magnitude ?y ?u)  
                           (- (magnitude ?x ?u))))))) 

(define-function RECIP (?x) :-> ?y 

  "RECIP defines the specialization of the multiplicative 
inverse operator for scalar-quantities." 
   
  :when (scalar-quantity ?x) 
  :def (and (scalar-quantity ?y) 
            (forall ?dim  
                    (=> (/= ?x (the-zero-scalar-for-dimension ?dim)) 
                        (= (* ?x ?y) identity-scalar))))) 

(define-function EXPT (?x ?r) :-> ?z 

  "EXPT defines real exponentiation for scalar-quantities.  Specializes 
EXPT." 
   
  :when (and (scalar-quantity ?x) 
             (real-number ?r)) 
  :def (and (scalar-quantity ?z) 
            (=> (= ?r 0) 
                (= ?z 1)) 
            (forall ?u 
               (=> (unit-of-measure ?u) 
                   (= (EXPT (magnitude ?x ?u) ?r) 
                      (magnitude ?z (EXPT ?u ?r))))))) 

(define-function SCALAR-QUANTITIES-OF-DIMENSION (?dimension) :-> ?class 

  "Scalar-Quantities are partitioned into classes of uniform dimension.  All 
instances of one of these classes have the same physical dimension. 
Each of these classes form a linear order with respect to the < 
relation.  Length scalars, time scalars, and mass scalars are examples 
of scalar subclasses." 

   ;; all instances ?x of ?class are scalars of the same dimension. 

  := (if (physical-dimension ?dimension) 
	 (kappa (?q) 
		(and (scalar-quantity ?q) 
		     (= (quantity.dimension ?q) ?dimension)))) 
  :constraints (and (physical-dimension ?dimension) 
                    (class ?class) 
                    (linear-order ?class <))) 



(define-function THE-ZERO-SCALAR-FOR-DIMENSION (?dimension) :-> ?zero-scalar 

  "The zero element for scalars of physical-dimension 
?dimension.  The real number 0 is the zero scalar-quantity for 
quantities of identity-dimension (i.e., non-dimensional scalars). 
We make the distinction between 0 meters and 0 seconds, for instance, 
to maintain our compatibility requirements for operators such as 
addition (i.e. a length quantity + a length quantity always equals 
another length quantity).  In practice, the distinction between zero 
quantities may not be important to any models, but there inclusion 
frees us from special cases for composition of quantities of different 
dimensions." 

  :iff-def (and (physical-dimension ?dimension) 
		(scalar-quantity ?zero-scalar) 
		(zero-quantity ?zero-scalar) 
		(identity-element-for 
                  ?zero-scalar 
                  + 
                  (scalar-quantities-of-dimension ?dimension))) 

  :axiom-def (= 0 (THE-ZERO-SCALAR-FOR-DIMENSION identity-dimension)))