;;; -*- 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-theoryunary-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-classUNARY-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-functionVALUE-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-relationRELATION-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-functionRECIP(?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-functionEXPT(?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-functionTHE-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-functionTHE-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-classCONTINUOUS(?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-functionDERIV(?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-classTIME-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-classTIME-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-functionD/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)) )