;;; -*- 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 (scalar-quantities

  "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."
  :issues ("(c) 1993, 1994 Greg R. Olsen and Thomas R. Gruber"
	   (:see-also "The EngMath paper on line")))

(in-theory 'unary-scalar-functions)

;; Scalar Function Algebra


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

  :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

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

  "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 function-quantity (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.
  (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))

  ;; 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.
  (<=> (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 RECIP (?x) :-> ?y

  "RECIP is the multiplicative inverse operator for 

  :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

  :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

  :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-dependent-quantity ?q)
                   (deriv ?q)) 

This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber