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.
Physical-Quantities
Frame-Ontology
Kif-Relations
Kif-Sets
Kif-Lists
Kif-Numbers
Abstract-Algebra
Frame-Ontology ...
Standard-Units
Physical-Quantities ...
Cml
Thermodynamics
Dme
Thermodynamics
Relation-Extended-To-Function-Quantities
Time-Quantity
Unary-Scalar-Function-Quantity
Continuous
Time-Dependent-Quantity
Time-Dependent-Quantity
The following constants were used from included theories:
The following constants were used from theories not included:
All constants that were mentioned were defined.
A unary function that maps from a scalar-quantity to a scalar-quantity.
Slots Of Instances:
(<=> (Unary-Scalar-Function-Quantity ?X)
(And (Function-Quantity ?X)
(Unary-Function ?X)
(Domain ?X Scalar-Quantity)
(Range ?X Scalar-Quantity) ))
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'.
(Nth-Domain Value-At 2 Scalar-Quantity)
(Nth-Domain Value-At 1 Physical-Quantity)
(=> (Value-At ?Q ?Time ?Val)
(And (Physical-Quantity ?Q) (Scalar-Quantity ?Time)) )
(= (Value-At ?Q ?Time)
(If (Function-Quantity ?Q) (Value ?Q ?Time) ?Q) )
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)).
(<=> (Relation-Extended-To-Function-Quantities ?R)
(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))))))
'(<=> (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)) )))
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.
(=> (The-Identity-Unary-Scalar-Function-For-Domain ?Domain ?F)
(And (Subclass-Of ?Domain Scalar-Quantity)
(Exact-Domain ?F ?Domain)
(Forall (?T)
(=> (Instance-Of ?T ?Domain)
(= (Value ?F ?T) Identity-Scalar) ))))
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.
(Nth-Domain The-Zero-Unary-Scalar-Function-For-Dimension
3
Unary-Scalar-Function-Quantity)
(Nth-Domain The-Zero-Unary-Scalar-Function-For-Dimension
1
Physical-Dimension)
(=> (The-Zero-Unary-Scalar-Function-For-Dimension ?Physdim
?Domain
?F)
(And (Subclass-Of ?Domain Scalar-Quantity)
(Exact-Domain ?F ?Domain)
(Forall (?T)
(=> (Instance-Of ?T ?Domain)
(= (Value ?F ?T)
(The-Zero-Scalar-For-Dimension ?Physdim) )))))
Relation defining functions which are continuous. This concept is taken as primitive until representations for limits are generated.
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.
(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))) ))))
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.
Slots Of Instances:
(<=> (Time-Quantity ?T)
(And (Scalar-Quantity ?T)
(= (Quantity.Dimension ?T) Time-Dimension) ))
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.
(<=> (Time-Dependent-Quantity ?X)
(And (Unary-Scalar-Function-Quantity ?X)
(Continuous ?X)
(Subclass-Of (Exact-Domain ?X) Time-Quantity) ))
(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.
(= (D/Dt ?Q) (If (Time-Quantity ?Q) (Deriv ?Q)))