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

;;; Unary Scalar Functions 
;;; (c) 1993 Greg Olsen and Thomas Gruber 

(in-package "ONTOLINGUA-USER") 

(define-theory unary-scalar-functions (physical-quantities 
				       standard-units) 

  "This theory provides representation for unary functions which map a 
scalar-quantity to a scalar-quantity.  This type of function is typical in 
engineering analysis.  A common example is a time-dependent-quantity such as 
'the temperature reading of my thermometer'.  This quantity is a function from 
a scalar-quantities of dimension time to a scalar-quantity measuring 
temperature.  Although it is common for the 'independent variable' to be time, 
unary-scalar-function-quantities may be defined over any class of scalar 
quantities [of a homogenous dimension].  Unary-scalar-function-quantities are 
quantities themselves, and may be combined with addition, multiplication, and 
other functions defined for scalar-quantities.  In addition, these quantities 
also have properties such as continuity and can have derivatives.") 

(in-theory 'unary-scalar-functions) 

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;; Scalar Function Algebra 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

(define-class UNARY-SCALAR-FUNCTION-QUANTITY (?x) 

  "A unary function that maps from a scalar-quantity to a 
scalar-quantity." 

  :iff-def (and (function-quantity ?x) 
                (unary-function ?x) 
                (domain ?x scalar-quantity) 
                (range ?x scalar-quantity))) 

(define-function VALUE-AT (?q ?time) :-> ?val 

  "The function value-at returns the value of a quantity at some point 
in 'time' (or whatever the independent state variable is).  The 'time' 
argument is just a constant scalar-quantity, such as a time-quantity. 
If the quantity is a function-quantity, then its value-at is its 
function value applied to the 'time' argument.  If the quantity is 
constant-quantity, then its value-at is the quantity itself for all 
'times'." 

  :def (and (physical-quantity ?q) 
	    (scalar-quantity ?time)) 
  :lambda-body (if (function-quantity ?q) 
                   (value ?q ?time) 
                   ?q)) 

(define-relation RELATION-EXTENDED-TO-FUNCTION-QUANTITIES (?r) 
  "A relation-extended-to-function-quantities is a relation that is defined 
for both constant-quantities and unary-scalar-function-quantities. 
The relation holds on some arguments (which may be function-quantities), 
if and only if whenever all the arguments have a value-at some ?t, 
the relation holds on those values.  The relation may be of any arity. 
Since value-at is defined for both function-quantities and constant-quantities, 
a relation-extended-to-function-quantities can be defined on sequences 
of arguments that are mixes of function-quantities and constant-quantities. 
   For example, the inequality relation < is a  
relation-extended-to-function-quantities.  Consider the case of (< ?x ?y). 
Whenever (value-at ?x ?t) is defined and (value-at ?y ?t) is defined, 
then (< (value-at ?x ?t) (value-at ?y ?t)).  There can be some ?t for 
which ?x or ?y is undefined, as long as for those ?t on which 
they are both defined, they < relation holds on their values. 
Either ?x or ?y or both can be constant-quantities, since (value-at ?x ?t) 
is just ?x when ?x is a constant. 
  Since functions are relations, a function may also be extended to 
apply to function quantities.  The same axioms hold.  Intuitively, 
a the value of a function F over function-quantities qf1 and qf2 is  
another quantity-function (F qf1 qf2) such that for all ?t where (qf1 ?t)  
and (qf2 ?t) are defined, (F qf1 qf2) = (F (qf1 ?t) (qf2 ?t))." 

   ;; don't try this at home. 
  :iff-def 
  (forall (@args) 
    (<=> (holds ?r @args) 
         (forall (?t) 
           (=> (=> (item ?q (listof @args)) 
                   (defined (value-at ?q ?t))) 
               (member (map (lambda (?q) (value-at ?q ?t)) 
                            (listof @args)) 
                       ?r))))) 

   ;; this is a subclass of RELATION. Doesn't have to be binary. 
  :constraints (relation ?r) 

   ;; Here is the case for binary relations.  It's a theorem from 
   ;; the axiom-def, but it helps to see it without the @args. 
  :axiom-constraints 
  (<=> (holds ?r ?q1 ?q2) 
       (forall (?t) 
         (=> (and (defined (value-at ?q1 ?t)) 
                  (defined (value-at ?q2 ?t))) 
             (holds ?r 
                    (value-at ?q1 ?t) 
                    (value-at ?q2 ?t)))))) 


(define-relation < (?fq1 ?fq2) 
  :when (and (function-quantity ?fq1) 
             (function-quantity ?fq2)) 
  :axiom-def (relation-extended-to-function-quantities <)) 


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

  "Defines the specialization of the QUANTITY addition operator + for 
unary-scalar-function-quantitys.  This now works when the exact-domains of the 
addends are overlapping." 

  :when (and (unary-scalar-function-quantity ?x) 
             (unary-scalar-function-quantity ?y)) 
  :axiom-def (relation-extended-to-function-quantities +) 
  :constraints (unary-scalar-function-quantity ?z)) 


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

  "Defines the specialization of the multiplication operator * for 
unary-scalar-function-quantitys.  It is defined for the cases where both its 
arguments are USFs, and also when the first is a scalar and the second 
is a USF." 
   
  :when (and (unary-scalar-function-quantity ?x) 
	     (unary-scalar-function-quantity ?y)) 
  :constraints (unary-scalar-function-quantity ?z) 
  :axiom-def (relation-extended-to-function-quantities *)) 

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

  "Defines the specialization of the additive inverse operator Q-NEQ 
for unary-scalar-function-quantities." 

  :when (unary-scalar-function-quantity ?x) 
  :constraints (unary-scalar-function-quantity ?y) 
  :axiom-def (relation-extended-to-function-quantities -)) 

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

  "RECIP is the multiplicative inverse operator for  
unary-scalar-function-quantities." 

  :when (unary-scalar-function-quantity ?x) 
  :constraints (unary-scalar-function-quantity ?y) 
  :axiom-def (relation-extended-to-function-quantities RECIP)) 

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

  "Real exponentiation for unary-scalar-function-quantitys." 

  :when (and (unary-scalar-function-quantity ?x) 
             (real-number ?r)) 
  :constraints (unary-scalar-function-quantity ?z) 
  :axiom-def (relation-extended-to-function-quantities EXPT)) 

(define-function THE-IDENTITY-UNARY-SCALAR-FUNCTION-FOR-DOMAIN (?domain) :->  ?f 

  "The the-identity-unary-scalar-function-for-domain is a scalar function which has a 
range = 1 for the exact-domain ?domain; f(x) = 1 forall x in 
?domain." 

  :def (and (subclass-of ?domain scalar-quantity) 
	    (unary-scalar-function-quantity ?f) 
	    (exact-domain ?f ?domain) 
	    (forall ?t 
               (=> (instance-of ?t ?domain) 
                   (= (value ?f ?t) identity-scalar))))) 

(define-function THE-ZERO-UNARY-SCALAR-FUNCTION-FOR-DIMENSION (?physdim ?domain) :-> ?f 

  "The zero-usf-function is the scalar function that has a 
range = zero-scalar-for-dimension ?physdim for exact-domain ?domain; 
f(x)=0 forall x in ?domain." 
   
  :def (and (subclass-of ?domain scalar-quantity) 
	    (physical-dimension ?physdim) 
	    (unary-scalar-function-quantity ?f) 
	    (exact-domain ?f ?domain) 
	    (forall ?t 
               (=> (instance-of ?t ?domain) 
                   (= (value ?f ?t)  
                      (the-zero-scalar-for-dimension ?physdim)))))) 

;;;---------------------------------------------------------------------- 
;;; Properties of quantities as functions: continuity, etc. 
;;;---------------------------------------------------------------------- 

(define-class CONTINUOUS (?f) 

  "Relation defining functions which are continuous.  This concept is 
taken as primitive until representations for limits are generated." 

  :def (unary-scalar-function-quantity ?f)) 

(define-function DERIV (?x) :-> ?z 

  "deriv[?x] is the derivative of unary-scalar-function-quantity ?x 
{deriv[f[x]] = f'[x]}.  Deriv is only defined on continuous functions. 
   Deriv has the normal algebraic properties of derivatives of 
real-valued functions; see the axioms for the exact behavior of 
differentiation with respect to sums and products of 
unary-scalar-function-quantities." 

  :def (and (unary-scalar-function-quantity ?x) 
	    (continuous ?x) 
	    (unary-scalar-function-quantity ?z)) 

  :axiom-def (forall (?f ?g ?r) 
                (=> (and (unary-scalar-function-quantity ?f) 
                         (unary-scalar-function-quantity ?g) 
                         (real-number ?r)) 
                    (and (= (deriv (+ ?f ?g)) 
                            (+ (deriv ?f) (deriv ?g))) 
                         (= (deriv (* ?f ?g))  
                            (+  
                              (* (deriv ?f) ?g)  
                              (* ?f (deriv ?g)))) 
                         (= (deriv (EXPT ?f ?r)) 
                            (* ?r (EXPT (deriv ?f) (1- ?r)))))))) 


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
;; Quantity State Space 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

;this theory is used to represent time varying scalars such as the 
;height of a travelling projectile above the ground, or the mean 
;temperature of a body that is cooling.  this theory describes a 
;subclass of scalar-functions which have a continuous time quantity as 
;their domain, and all elements of their range have a common physical 
;dimension.  using this theory we can describe dynamic behavior which 
;takes the form of ordinary differential equations. 


(define-class TIME-QUANTITY (?t) 

  "A time-quantity is a scalar quantity whose dimension is time-dimension.   
Conceptually, a time-quantity is an amount [duration] of time. 
It is constant quantity, not a function or an interval.  Like all 
constant-quantities, its magnitude is given in terms of units of 
measure.  For example, the products of all real numbers and a unit like  
second-of-time are time quantities." 

  :iff-def (and (scalar-quantity ?t) 
		(= (quantity.dimension ?t) time-dimension))) 


(define-class TIME-DEPENDENT-QUANTITY (?x) 

  "A unary scalar function of continuous time.  Maps a time-quantity 
into another scalar quantity such as a temperature.  For example, a quantity 
that denotes 'the temperature of the top of the Empire State Building' 
is a time-dependent-quantity since its value depends on the time." 

  :iff-def (and (unary-scalar-function-quantity ?x) 
		(continuous ?x) 
		(subclass-of (exact-domain ?x) time-quantity))) 

(define-function D/DT (?q) :-> ?time-derivative 
  "(D/DT ?q) is the derivative with respect to time of the 
time-dependent-quantity ?q.  It is undefined on other quantities, 
including constant-quantities." 

  :lambda-body (if (time-quantity ?q) 
                   (deriv ?q))  
  )