```;;; -*- 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
standard-dimensions)

"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
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(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 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.
: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

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

```

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