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