;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-
;;; Physical Quantities Ontology
;;; (c) 1993 Greg Olsen and Thomas Gruber
(in-package "ONTOLINGUA-USER")
(define-theory physical-quantities (frame-ontology abstract-algebra)
"In engineering analysis, physical quantities such as the length of a beam
or the velocity of a body are routinely modeled by variables in equations
with numbers as values. While human engineers can interpret these numbers as
physical quantities by inferring dimension and units from context, the
representation of quantities as numbers leaves implicit other relevant
information about physical quantities in engineering models, such as physical
dimension and unit of measure. Furthermore, there are many classes of models
where the magnitude of a physical quantity is not a simple real number - a
vector or higher-order tensor for instance. Our goal here is to extend
standard mathematics to include unit and dimension semantics.
In this theory, we attempt to define the basic concepts associated
with physical quantities. A quantity is a hypothetically measurable
amount of something. We refer to those things whose amounts are
described by physical-quantities as physical-dimensions (following the
terminology used in most introductory Physics texts). Time, length,
mass, and energy are examples of physical-dimensions. Comparability
is inherently tied to the concept of quantities. Quantities are
described in terms of reference quantities called units-of-measure. A
meter is an example of an unit-of-measure for quantities of the length
physical-dimension.
The physical-quantities theory defines the basic vocabulary for
describing physical quantities in a general form, making explicit the
relationships between magnitudes of various orders, units of measure
and physical dimensions. It defines the general class
physical-quantity and a set of algebraic operators that are total over
all physical quantities. Specializations of the physical-quantity
class and the operators are defined in other theories (which use
this theory).
The theory also describes specific language for physical units such as
meters, inches, and pounds, and physical dimensions such as length,
time, and mass. The theory provides representational vocabulary to
compose units and dimensions from basis sets and to describe the basic
relationships between units and physical dimensions. This theory
helps support the consistent use of units in expressions relating
physical quantities, and it also supports conversion of units needed
in calculations.")
(in-theory 'physical-quantities)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Physical Quantities
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-class PHYSICAL-QUANTITY (?x)
"A physical-quantity is a measure of some quantifiable aspect of the
modeled world, such as 'the earth's diameter' (a constant length) and
'the stress in a loaded deformable solid' (a measure of stress, which
is a function of three spatial coordinates). The first type is called
constant-quantity and the second type is called function-quantity.
All physical quantities are either constant-quantities or
function-quantities. Although the name and definition of this concept
is inspired from physics, physical quantities need not be material.
For example, amounts of money are physical quantities. In fact,
all real numbers and numeric-valued tensors are special cases of physical
quantities. In engineering textbooks, quantities are often called variables.
Physical quantities are distinguished from purely numeric entities
like a real numbers by their physical dimensions. A
physical-dimension is a property that distinguishes types of
quantities. Every physical-quantity has exactly one associated
physical-dimension. In physics, we talk about dimensions such as
length, time, and velocity; again, nonphysical dimensions such as
currency are also possible. The dimension of purely numeric entities
is the identity-dimension.
The 'value' of a physical-quantity depends on its type. The value of
a constant-quantity is dependent on a unit-of-measure. Physical
quantities of the identity-dimension (dimensionless quantities) are
just numbers or tensors to start with. Physical quantities of the
type function-quantity are functions that map quantities to other
quantities (e.g., time-dependent quantities are function-quantities).
See the definitions of these other classes and functions for detail."
;; every physical quantity has a dimension
:def (defined (quantity.dimension ?x))
;; physical quantities are either quantities or quantity functions
:axiom-def (and (exhaustive-subclass-partition
PHYSICAL-QUANTITY
(setof CONSTANT-QUANTITY FUNCTION-QUANTITY)))
:issues ((:see-also CONSTANT-QUANTITY FUNCTION-QUANTITY PHYSICAL-DIMENSION)
("We define a general class of quantities in order to
support a generic set of operators. Most of the semantics
of these operators are not given here. Specializations
of quantity will define how each operator works over
their domains (i.e., subclasses of quantity).")))
(define-function QUANTITY.DIMENSION (?q) :-> ?dim
"A quantity has a unique physical-dimension. This function maps
quantities to physical-dimensions. It is total for all physical
quantities (as stated in the definition of physical-quantity)."
:def (and (physical-quantity ?q) ; domain constraint
(physical-dimension ?dim)) ; range constraint
:issues ((:example
(= (quantity.dimension (height fred)) length-dimension))))
(define-relation COMPATIBLE-QUANTITIES (?x ?y)
"Two physical quantities are compatible if their physical-dimensions
are equal. Compatibility constrains how quantities can be compared
and combined with algebraic operators."
:iff-def (and (physical-quantity ?x)
(physical-quantity ?y)
(= (quantity.dimension ?x) (quantity.dimension ?y)))
:issues (:example
(compatible-quantities (* 6 feet)
(* 20 meters))))
(define-class CONSTANT-QUANTITY (?x)
"A constant-quantity is a constant value of some physical-quantity, like
3 meters or 55 miles per hour. Constant quantities are distinguished from
function-quantities, which map some quantities to other quantities.
For example, the velocity of a particle over some range of time would
be represented by a function-quantity mapping values of time (which are
constant quantities) to velocity vectors (also constant quantities).
All real numbers (and numeric tensors of higher order) are constant
quantities whose dimension is the identity-dimension (i.e., the so-called
'dimensionless' or nondimensional-constant-quantity).
All constant quantites can be expressed as the product of some
nondimensional quantity and a unit of measure. This is what it means
to say a quantity `has a magnitude'. For example, 2 meters can be expressed
as (* 3 meter), where meter is defined as a unit of measure for length.
All units of measure are also constant quantities."
;; constant-quantity is a kind of physical quantity that is not a function
:iff-def (and (physical-quantity ?x)
(not (function-quantity ?x)))
:issues ((:example
(constant-quantity (height fred)))
("Why not associate a fixed unit of measure
with a quantity?"
"Assume that quantities have a property like q.unit.
Then define two quantities Q1 = (the-quantity 10 centimeters)
and Q2 = (the-quantity 0.1 meters). Clearly Q1 = Q2.
But (q.unit Q1) = centimeters and (q.unit Q2) = meters.
This is a contradiction.")
("Why include numbers as quantities?"
"This allows one to commit to the engineering math
ontologies without having to handle all the units
and dimensions. The theory can include all of normal
math as a special case.")))
(define-class FUNCTION-QUANTITY (?f)
"A FUNCTION-QUANTITY is a function that maps from one or more
constant-quantities to a constant-quantity. The function must have a
fixed arity of at least 1. All elements of the range (ie, values of the
function) have the same physical-dimension, which is the dimension of
the function-quantity itself."
:iff-def (and (physical-quantity ?f)
;; an instance of FUNCTION-QUANTITY is a function
(function ?f)
;; the arity is fixed
(defined (arity ?f))
;; the domains and range of the function are CONSTANT-QUANTITIES
(subclass-of (relation-universe ?f)
constant-quantity)
;; all the values have the same dimension
;; the dimension of ?f is the dimension of all of
;; the values of ?f (ie, instances of its exact-range)
(defined (quantity.dimension ?f))
(forall ?val
(=> (instance-of ?val (exact-range ?f))
(= (quantity.dimension ?f)
(quantity.dimension ?val))))))
(define-class NONDIMENSIONAL-CONSTANT-QUANTITY (?x)
"Although it sounds contradictory, a nondimensional-constant-quantity is a
quantity whose dimension is the identity-dimension. All numeric tensors,
including real numbers, are nondimensional quantities."
:iff-def (and (constant-quantity ?x)
(= (quantity.dimension ?x) identity-dimension))
;; all real numbers are constant-quantities with the identity-dimension
;; as dimension.
:axiom-def (superclass-of nondimensional-constant-quantity real-number))
(define-function MAGNITUDE (?q ?unit) :-> ?mag
"The magnitude of a constant-quantity is a numeric value for the
quantity given in terms of some unit-of-measure. For example, the
magnitude of the quantity 2 kilometers in the unit-of-measure meter is
the real number 2000. The
unit-of-measure and quantity must be of the same physical-dimension,
and the resulting value is a nondimensional quantity. The type of the
resulting quantity is dependent on the type of the original quantity.
The magnitude of a scalar-quantity is a real-number, and the magnitude
of a vector-quantity is a numeric-vector. In general, then, the
magnitude function converts a quantity with dimension into a normal
mathematical object.
Units of measure are scalar quantities, and magnitude is defined in
terms of scalar multiplication. The magnitude of a quantity in a
given unit times that unit is equal to the original quantity. This
holds for all kinds of tensors, including real-numbers and vectors.
For scalar quantities, one can think of the magnitude as the ratio of
a quantity to the unit quantity. See the definition of the
multiplication operator * for the various sorts of quantities. The
properties of * that hold for all physical-quantities are defined in
this theory.
There is no magnitude for a function-quantity. Instead, the value
of a function-quantity on some input is a quantity which may in turn be
a constant-quantity for which the magnitude function is defined.
See the definition of value-at."
:iff-def (and (constant-quantity ?q)
(unit-of-measure ?unit)
(nondimensional-constant-quantity ?mag)
(compatible-quantities ?q ?unit)
(defined (* ?mag ?unit))
(= (* ?mag ?unit) ?q))
;; magnitudes can be factored out of quantities
:axiom-def (forall (?q ?unit ?mag)
(=> (and (constant-quantity ?q)
(unit-of-measure ?unit)
(nondimensional-constant-quantity ?mag)
(defined (* ?mag ?q)))
(= (magnitude (* ?mag ?q) ?unit)
(* ?mag (magnitude ?q ?unit)))))
:issues ((:example
(=> (= (height fred) (* 2 yards))
(= (magnitude (height fred) feet) 6)))))
(define-class ZERO-QUANTITY (?x)
"A zero quantity is one which, when multiplied times any
quantity, results in another zero quantity (possibly the same zero).
The class of zero quantities includes the number 0, and zero
quantities for every physical dimension and order of tensor."
:def (and (physical-quantity ?x)
(forall (?q)
(=> (physical-quantity ?q)
(zero-quantity (* ?q ?x)))))
:axiom-def (zero-quantity 0)
:issues (("Q: Why not make one zero-thing which follows our
intuition?"
"A: We would have to make exceptions for all of our
operators on quantities that depend on
physical-dimension or tensor-order.")))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Operators defined for all physical quantities
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-function + (?x ?y):-> ?z
"+ is the addition operator for physical-quantities. The + function
is defined for numbers as part of KIF specification (in the kif-numbers
ontology). Here it is extended polymorphically to operate on physical
quantities. The main difference between quantities and ordinary
numbers is the notion of dimension and unit. First, the sum of two
quantities is only defined when the quantities are comparable -- having
the same dimension -- and the sum has the same dimension. Second, the
sum of two constant quantities is the sum of their magnitudes.
However, the magnitude of a quantity is relative to a unit in which it
is requested. Therefore, the sum of two quantities x and y is another
quantity z such that for all units of measure of comparable
dimension, the magnitude of z in such a unit is the sum of the
magnitude of x and y in that unit.
The + function is further specialized when applied to different kinds
of quantities, such as constant-quantities, function-quantities,
and vector-quantities."
:when (and (physical-quantity ?x)
(physical-quantity ?y))
:def (and (physical-quantity ?z)
(compatible-quantities ?x ?y)
(compatible-quantities ?x ?z)))
(define-function * (?x ?y):-> ?z
"* is the multiplication operator for physical-quantities. The *
function is defined for numbers as part of KIF specification (in the
kif-numbers ontology). Here it is extended polymorphically to operate
on physical quantities. The main difference between quantities and
ordinary numbers is the notion of dimension and unit. The dimension of
the product of two quantities is the analogous product of their
dimensions (the * function is also extended to dimensions). For
example, the product of two length quantities is a quantity of
dimension 'length * length'.
The relationship between the magnitudes of two quantities and their
product cannot be stated completely in this ontology. It depends on
the whether the magnitudes are scalars or higher-order tensors. The *
function is further specialized when applied to these different kinds
of quantities in the ontologies for scalar-quantities and
vector-quantities. It must be commutative and associative, however,
in order to allow factoring of magnitudes and units."
:when (and (physical-quantity ?x)
(physical-quantity ?y))
:def (and (physical-quantity ?z)
(= (quantity.dimension ?z)
(* (quantity.dimension ?x) (quantity.dimension ?y)))
)
:axiom-def (and (commutative * physical-quantity)
(associative * physical-quantity)
(distributes * + physical-quantity)))
(define-function - (?x) :-> ?y
"(- ?x) denotes the negative element of element ?x with respect to
addition operator: i.e., it is the additive inverse. The unary '-'
operator for complex numbers (part of KIF specification) is overloaded
to operate on physical quantities. All quantity objects have an
additive inverse and the addition of a parameter and its
additive-inverse will equal a zero element, such as the real number 0
or the zero vector of the same dimension if ?x is a vector. Each
engineering quantity algebra will define specialization of - for its
domain."
:when (physical-quantity ?x)
:def (and (physical-quantity ?y)
(compatible-quantities ?x ?y)))
(define-function RECIP (?x) :-> ?y
"(RECIP ?x) is the reciprocal element of element ?x with respect
to multiplication operator. For a number x the reciprocal would be
1/x. Not all quantity objects will have a reciprocal element defined.
The number 0 for instance will not have a reciprocal. If a parameter
x has a reciprocal y, then the product of x and y will be an identity
element of some sort such as '1' for numbers, 3*1/3 = 1. The
reciprocal of an element is equivalent to exponentiation of the
element to the power -1."
:when (physical-quantity ?x)
:def (and (physical-quantity ?y)
(= (quantity.dimension ?y) (expt (quantity.dimension ?x) -1)))
:axiom-def (= (recip ?x) (EXPT ?x -1)))
(define-function EXPT (?x ?r) :-> ?z
"EXPT is exponentiation to real powers for physical-quantities. The
'expt' operator for complex numbers (part of KIF specification) is
overloaded to operate on physical quantities. This operator is
further defined for quantity subclasses. The result is a
physical-quantity if it is defined."
:when (and (physical-quantity ?x)
(real-number ?r))
:def (and (physical-quantity ?z)
;; the dimension of the expt of two quantities is
;; the expt of their dimensions. See expt below.
(= (quantity.dimension ?z) (expt (quantity.dimension ?x) ?r)))
:axiom-def (forall (?x1 ?x2 ?r1 ?r2)
(and
(= (* (EXPT ?x1 ?r1) (EXPT ?x1 ?r2))
(EXPT ?x1 (+ ?r1 ?r2)))
(= (EXPT (* ?x1 ?x2) ?r1)
(* (EXPT ?x1 ?r1) (EXPT ?x2 ?r1)))
(= (EXPT (EXPT ?x1 ?r1) ?r2)
(EXPT ?x1 (* ?r1 ?r2))))))
(define-function - (?x ?y) :-> ?z
"Subtraction for physical-quantities. The binary '-' operator for
complex numbers (part of KIF specification) is overloaded to operate
on physical quantities. Defined in terms of addition and unary minus,
-."
:when (and (physical-quantity ?x)
(physical-quantity ?y))
:= (+ ?x (- ?y)))
(define-function / (?x ?y):-> ?z
"Division for physical-quantities. The '/' operator for complex
numbers (part of KIF specification) is overloaded to operate on
physical quantities. Defined in terms of multiplication and real
exponentiation operators."
:when (and (physical-quantity ?x)
(physical-quantity ?y))
:= (* ?x (EXPT ?y -1)))
(define-function SUMMATION (?func ?start ?end) :-> ?q
"Summation operator for a function that represents an integer
indexed quantity."
;; this says that summation is total for physical quantities
:when (range ?func physical-quantity)
:def (and (physical-quantity ?q)
(integer ?start)
(integer ?end)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Polymorphic extensions for constant quantities
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-relation RELATION-EXTENDED-TO-QUANTITIES (?r)
"A relation-extended-to-quantities is a relation that, when it is
true on a sequence of arguments that are magnitudes (e.g., real numbers or
tensors), then it is also true on a sequence of constant quantites with those
magnitudes in some units.
For example, the < relation is extended to quantities. That means
that for all pairs of quantities q1 and q2, (< q1 q2) if and only
if (< (magnitude q1 ?u) (magnitude q2 ?u)) for all units on which
the two magnitudes are defined.
There may be relations that are not instances of this class
that nonetheless hold for quantity arguments. To be a
relation-extended-to-quantities means that the relation
holds when all the arguments are of the same physical dimension."
:iff-def
(and (relation ?r)
(forall (@args)
(<=>
;; the relation holds for some constant quantities iff
(and (holds ?r @args)
(=> (item ?q (listof @args))
(and (constant-quantity ?q))))
;; for any unit that is compatible with ALL the arguments
(forall (?unit ?q)
(=> (and (unit-of-measure ?unit)
(=> (item ?q (listof @args))
(compatible-quantities ?q ?unit)))
;; it holds on the magnitudes of those quantities in that unit
(member (map (lambda (?q) (magnitude ?q ?unit))
(listof @args))
?r)))))))
(define-relation < (?q1 ?q2)
"The < relation is defined for quantities. It holds on quantities
when it holds on their magnitudes."
:when (and (constant-quantity ?q1) (constant-quantity ?q2))
:axiom-def (relation-extended-to-quantities <))
(define-function + (?x ?y):-> ?z
"The + function can be applied to all compatible constant quantities.
The sum of the magnitudes of two compatible-quantities is equal to the
magnitude of the sum of the quantities, for all units of measure."
:when (and (constant-quantity ?x)
(constant-quantity ?y))
:axiom-def (relation-extended-to-quantities +)
;; but just to be clear what that means
:iff-def (and (constant-quantity ?z)
(forall ?unit
(=> (unit-of-measure ?unit)
(= (+ (magnitude ?x ?unit)
(magnitude ?y ?unit))
(magnitude ?z ?unit))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; PHYSICAL-DIMENSIONS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-class PHYSICAL-DIMENSION (?x)
"A physical dimension is a property we associate with physical
quantities for purposes of classification or differentiation. Mass,
length, and force are examples of physical dimensions. Composite
physical dimensions can be described by composing primitive dimensions.
For example, Length/Time ('length over time') is a dimension that can
be associated with a velocity.
The composition operators for dimensions are * [dimension product]
and expt [exponentiation to a real power], which have algebraic
properties analogous to their use with real numbers. The product of
any two dimensions is a dimension. There is an indentity element for
* on dimensions; it is called the identity-dimension. The product of
any dimension and the identity-dimension is the original dimension;
any other product defines a new dimension. The analogy of division is
exponentiation to a negative number.
There is no intrinsic property of a dimension that makes it primitive.
A set of primitive dimensions is chosen by convention to define a system
of units of measure. However, the relative relationships among
dimensions can be established independently of systems of units. For
example, the dimension corresponding to velocity is length/time, and
therefore the length dimension is the same as velocity * time. This is
true regardless of whether the length or velocity dimensions are viewed
as the fundamental dimensions in some system, or whether either dimension
is denoted by a object constant or a term expression in some theory."
:def (individual ?x) ;not a set
:axiom-def (abelian-group physical-dimension * identity-dimension)
)
(define-function * (?d1 ?d2) :-> ?d3
"* is a commutative and associative operator for specifying products of
physical-dimensions. Together with the identity-dimension, * forms an abelian
group over physical-dimensions."
;; This :WHEN clause indicates a polymorphic extension of the * operator
;; to the case where it is applied to to dimensions. The :DEF constraint
;; only holds when the :WHEN condition holds.
:when (and (physical-dimension ?d1)
(physical-dimension ?d2))
:def (physical-dimension ?d3)
:issues ((:example
(= force (* mass-dimension length-dimension
(expt time-dimension -2)))
(= work (* force length-dimension)))))
(define-instance IDENTITY-DIMENSION (physical-dimension)
"identity-dimension is the identity element for the * operator over
physical-dimensions. That means that the product of identity-dimension and
any other dimension is that other dimension. Identity-dimension is the
dimension of the so-called dimensionless quantities, including the
real numbers."
:axiom-def (identity-element-for identity-dimension * physical-dimension))
(define-function EXPT (?d ?exp) :-> ?dim
"Exponentiation of physical-dimensions to a real power."
:when (and (physical-dimension ?d)
(real-number ?exp))
:def (physical-dimension ?dim)
:axiom-def (forall (?d1 ?d2 ?r1 ?r2)
(=> (and (physical-dimension ?d1)
(physical-dimension ?d2)
(real-number ?r1)
(real-number ?r2))
(and (= (expt ?d1 0) identity-dimension)
(= ?d1 (expt ?d1 1))
(= (* (expt ?d1 ?r1) (expt ?d1 ?r2))
(expt ?d1 (+ ?r1 ?r2)))
(= (expt (* ?d1 ?d2) ?r1)
(* (expt ?d1 ?r1) (expt ?d2 ?r1)))
(= (expt (expt ?d1 ?r1) ?r2)
(expt ?d1 (* ?r1 ?r2)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; UNIT-OF-MEASURE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-class UNIT-OF-MEASURE (?u)
"A unit-of-measure is a constant-quantity that serves as
a standard of measurement for some dimension. For example, the meter is
a unit-of-measure for the length-dimension, as is the inch.
Square-feet is a unit for length*length quantities.
Units-of-measure can be defined as primitives or can be defined
as products of units or units raised to real exponents.
There is no intrisic property of a unit that makes it primitive
or fundamental; rather, a system-of-units defines a set of orthogonal
dimensions and assigns units for each. Therefore, there is no distinguished
class for fundamental unit of measure.
The magnitude of a unit-of-measure is always a positive real number,
using any comparable unit. Units are not scales, which have reference origins
and can have negative values. Units are like distances between points on scales.
Any composition of units and reals using the * and expt functions is also
a unit-of-measure. For example, the quantity 'three meters' is denoted
by the expression (* 3 meter). There is an identity-unit that forms
and abelian-group with the * operator over units of measure. That means
* is commutative and associative for units. It is also commutative for
multiplying units and other constant-quantities. This is important for
factoring out units from expressions containing tensors or functions."
:iff-def (and
;; A unit is a scalar quantity.
(constant-quantity ?u)
;; its magnitude is always a positive real,
;; which implies a linear order (not density)
(forall ?other-unit
(=> (and (unit-of-measure ?other-unit)
(compatible-quantities ?u ?other-unit))
(and (real-number (magnitude ?u ?other-unit))
(positive (magnitude ?u ?other-unit))))))
:axiom-def (and
;; units can be combined with * to produce units
(abelian-group unit-of-measure * identity-unit)
;; any composition of units and reals using * and expt is a unit
(=> (and (unit-of-measure ?a)
(real-number ?b))
(unit-of-measure (* ?a ?b)))
(=> (and (unit-of-measure ?a)
(real-number ?b))
(unit-of-measure (expt ?a ?b)))
;; * is communitive for units and other quantities.
;; This is important for factoring out units
;; when multiplied with tensors or functions.
(=> (and (unit-of-measure ?a)
(constant-quantity ?b))
(= (* ?a ?b) (* ?b ?a)))))
(define-instance IDENTITY-UNIT (unit-of-measure)
"The identity unit can be combined with any other unit to produce
the same unit. The identity unit is the real number 1. Its dimension
is the identity-dimension."
:= 1
:axiom-def (= (quantity.dimension identity-unit) identity-dimension))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; SYSTEMS OF UNITS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-class SYSTEM-OF-UNITS (?system)
"A system-of-units is a class of units of measure that defines
a standard system of measurement. Each instance of the class is a canonical
unit-of-measure for a dimension. The mapping from dimensions to units
in the system is provided by the function called standard-unit; since
this mapping is functional and total, there is exactly one unit
in the system of units per dimension.
There is no intrinsic property of a dimension that makes it
fundamental or primitive, and neither is there any such property
for units of measure. However, each system of units is defined by
a basis set of units, from which all other units in the system are
composed. The function base-units maps a system-of-units to its basis set.
The dimensions of the units in the base-set must be orthogonal (see the
definition of fundamental-dimension-set). For each composition of
these fundamental dimensions (e.g., length / time) there is a corresponding
unique unit in the system-of-units (e.g., meter / second-of-time).
The System International (SI) standard used in physics is a system-of-units
based on seven fundamental dimensions and base units. Other systems of units
may have different basis sets of differing cardinality, yet share some of
the same units as the SI system."
:iff-def
(and
;; a system of units is a CLASS of units
(class ?system)
(subclass-of ?system unit-of-measure)
;; Every unit in the system is the standard unit for its dimension.
(=> (instance-of ?unit ?system)
(= (standard-unit ?system (quantity.dimension ?unit)) ?unit))
;; It defines a set of base units whose dimensions are fundamental
(defined (base-units ?system))
(=> (member ?unit (base-units ?system))
(instance-of ?unit ?system))
(orthogonal-dimension-set (setofall ?dim
(exists ?unit
(and (member ?unit (base-units ?system))
(= ?dim (quantity.dimension ?unit)))))))
:issues ((:example (system-of-units si-unit))
((("Can any set of units be the base-set for a system of units?"
"No, the base-units in a system of units must not be compositions
of each other. For example, if the base units included
meter, second-of-time, and (unit* meter second-of-time), then it would
NOT be a system of units, because the dimension of
(unit* meter second-of-time) is (* length-dimension
time-dimension), which is a composition of other
``fundamental'' dimensions.")))))
(define-function BASE-UNITS (?system-of-units) :-> ?set-of-units
"Defines a set of base units for a system of units."
:def (and (system-of-units ?system-of-units)
(set ?set-of-units)
(=> (member ?unit ?set-of-units)
(unit-of-measure ?unit))))
(define-function STANDARD-UNIT (?system-of-units ?dimension) :-> ?unit
"The standard-unit for a given system and dimension is a unit in that
system whose dimension is the given dimension."
:iff-def (and (system-of-units ?system-of-units)
(physical-dimension ?dimension)
(unit-of-measure ?unit)
(instance-of ?unit ?system-of-units)
(= (quantity.dimension ?unit) ?dimension)))
(define-function MAGNITUDE-IN-SYSTEM-OF-UNITS (?q ?system) :-> ?mag
"magnitude-in-system-of-units is like magnitude, but it maps a
quantity and a system of units into a nondimensional numeric value.
For example, one could ask for the value of 55 miles per hour in the
SI system. In SI, the standard-unit for the dimension of miles per hour
is meters per second-of-time. So the answer would be about 24 meters per second-of-time."
:constraints (and (constant-quantity ?q)
(system-of-units ?system)
(nondimensional-constant-quantity ?mag))
:= (magnitude ?q (standard-unit ?system (quantity.dimension ?q))))
(define-class ORTHOGONAL-DIMENSION-SET (?set-of-dimensions)
"A set of orthogonal dimensions; i.e., dimensions that cannot be
composed from each other."
:iff-def (and (set ?set-of-dimensions)
(=> (member ?dim ?set-of-dimensions)
(and
(physical-dimension ?dim)
(not (dimension-composable-from
?dim
(difference ?set-of-dimensions (setof ?dim))))))))
(define-relation DIMENSION-COMPOSABLE-FROM (?dim ?set-of-dimensions)
:iff-def (or (member ?dim ?set-of-dimensions)
(exists (?dim1 ?dim2)
(and (dimension-composable-from ?dim1 ?set-of-dimensions)
(dimension-composable-from ?dim2 ?set-of-dimensions)
(= ?dim (* ?dim1 ?dim2))))
(exists (?dim1 ?real)
(and (dimension-composable-from ?dim1 ?set-of-dimensions)
(real-number ?real)
(= ?dim (expt ?dim1 ?real))))))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber