;;; -*- 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 speed of light' are regularily 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 a quantity of some physical dimension, 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 QUANTITY-FUNCTION. All physical quantities are either CONSTANT-QUANTITYs or QUANTITY-FUNCTIONs. Every physical-quantity has exactly one associated PHYSICAL-DIMENSION. This includes ordinary numbers and numeric-valued tensors as a special case of physical-quantity; their physical dimension is the identity-dimension. The 'value' of a physical-quantity depends on its subtype. Physical quantities of the identity-dimension (dimensionless quantities) are just numbers or tensors to start with. Physical quantities of the type QUANTITY-FUNCTION are functions that map quantities to other quantities (e.g., time-varying quantities are quantity-functions). See the definitions of these other classes and functions for detail." ;; dimension is a total unary function over physical-quantities :def (defined (dimension ?x)) ;; physical quantities are either quantities or quantity functions :axiom-def (and (exhaustive-subclass-partition PHYSICAL-QUANTITY (setof CONSTANT-QUANTITY QUANTITY-FUNCTION))) :issues ((:see-also CONSTANT-QUANTITY QUANTITY-FUNCTION 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 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), and is only defined on physical quantities (as stated below)." :def (and (physical-quantity ?q) ; domain constraint (physical-dimension ?dim)) ; range constraint :issues ((:example (= (dimension (height fred)) length-dimension)))) (define-relation COMPATIBLE-QUANTITIES (?x ?y) "Two physical quantities are compatible if their physical-dimensions are equal." :iff-def (and (physical-quantity ?x) (physical-quantity ?y) (= (dimension ?x) (dimension ?y))) :issues (:example (compatible-quantities (* 6 feet) (* 20 meters)))) (define-class CONSTANT-QUANTITY (?x) "A constant-quantity is a kind of PHYSICAL-QUANTITY that is a _constant_ measure of some physical dimension, such as length or charge. Quantities can be scalars, vectors, or even higher-order tensors (i.e. the velocity of particle a, which could be represented by a 3-D vector of physical dimension 'Length/Time' and a magnitude which is a numeric-valued vector). Real numbers and numeric-valued tensors are subclasses of quantities (whose physical dimension is the identity-dimension). They are equivalent to 'dimension-less' quantities." ;; constant-quantity is a kind of physical quantity that is not a function ;; or any other kind of set (that's what INDIVIDUAL means). :def (and (physical-quantity ?x) (not (quantity-function ?x)) (individual ?x)) :axiom-def (=> (real-number ?r) (and (constant-quantity ?r) (= (dimension ?r) identity-dimension) )) :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 NONDIMENSIONAL-QUANTITY (?x) "Although it sounds contradictory, a nondimensional-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) (= (dimension ?x) identity-dimension)) ;; all real numbers are CONSTANT-QUANTITYs with the identity-dimension ;; as dimension. :axiom-def (subclass-of real-number nondimensional-quantity)) (define-class NUMERIC-TENSOR (?x) "A generalization of number to higher order. A numeric-valued tensor of order 0, 1, or 2. A subclass of constant-quantity with identity-dimension." :def (nondimensional-quantity ?x) ;; A real-number is a 0 order numeric-tensor. :axiom-def (subclass-of real-number numeric-tensor) ;; They are their own 'magnitudes' if 'measured' in identity units. :issues ((:example (numeric-tensor 6)))) (define-class ZERO-QUANTITY (?x) "The class of zero quantities which includes the number 0, and zero quantities for every physical dimension and order of tensor." :def (and (physical-quantity ?x) (forall (?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."))) (define-function MAGNITUDE (?q ?unit) :-> ?mag "Function that returns the magnitude of a quantity in terms of a given unit-of-measure. Note that the concept of a magnitude relies on a choice of a unit of measure. The unit-of-measure and quantity must be of the same physical-dimension." :iff-def (and (physical-quantity ?q) (unit-of-measure ?unit) (numeric-tensor ?mag) (compatible-quantities ?q ?unit) (= ?mag (/ ?q ?unit))) :issues ((:example (=> (= (height fred) (* 2 yards)) (= (magnitude (height fred) feet) 6))))) (define-class QUANTITY-FUNCTION (?f) "A QUANTITY-FUNCTION is a function that maps from one or more quantities to a quantity. The function must have a fixed arity of at least 1. All elements of the range have the same physical-dimension. The dimension of the quantity-function is the dimension of the elements of its range." :def (and (physical-quantity ?f) ;; an instance of QUANTITY-FUNCTION is a function (function ?f) ;; the arity is fixed (defined (arity ?f)) ;; the domains and range of the function are CONSTANT-QUANTITYs (subclass-of (relation-universe ?f) constant-quantity) ;; all the values have the same dimension (forall (?val1 ?val2) (=> (and (instance-of ?val1 (exact-range ?f)) (instance-of ?val2 (exact-range ?f))) (compatible-quantities ?val1 ?val2))) (forall ?val (=> (instance-of ?val (exact-range ?f)) (= (dimension ?f) (dimension ?val)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Operators defined for all physical quantities ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define-function + (?x ?y):-> ?z "Addition for physical-quantities. The '+' operator for complex numbers (part of KIF specification) is overloaded to operate on physical quantities. This operator is further defined for quantity subclasses. The dimensions of the addends and sum are the same. The magnitude of the sum of two quantities for a particular dimension is the sum of the magnitudes of the quantities for the same unit." :when (and (physical-quantity ?x) (physical-quantity ?y)) :def (and (physical-quantity ?z) (compatible-quantities ?x ?y) (compatible-quantities ?x ?z) (forall ?u (= (+ (magnitude ?x ?u) (magnitude ?y ?u)) (magnitude ?z ?u))))) (define-function * (?x ?y):-> ?z "Multiplication for physical-quantities. The '*' operator for complex numbers (part of KIF specification) is overloaded to operate on physical quantities. This operator is further defined for quantity subclasses. The dimension of the product is the product of the dimensions of the multipled quantities." :when (and (physical-quantity ?x) (physical-quantity ?y)) :def (and (physical-quantity ?z) (= (dimension ?z) (* (dimension ?x) (dimension ?y)))) :axiom-def (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) (= (dimension ?y) (expt (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. (= (dimension ?z) (expt (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)) :iff-def (= ?z (+ ?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)) :iff-def (= ?z (* ?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))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; 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 constructed from more primitive dimensions. For example, Length/Time ('length over time') is a dimension that can be associated with a velocity. All physical dimensions can be partitioned into fundamental-dimensions and derived dimensions; the derived-dimensions can always be generated by composition of fundamental-dimensions by multiplication and exponentiation operators." :def (individual ?x) ;not a set ) (define-function * (?d1 ?d2) :-> ?d3 "A commutative and associative operator for specifying products of physical-dimensions. The basic operator used to compose dimensions. Together with the identity-dimension, * forms an abelian group over physical-dimensions." :when (and (physical-dimension ?d1) (physical-dimension ?d2)) :def (physical-dimension ?d3) :axiom-def (abelian-group physical-dimension * identity-dimension) :issues ((:example (= force (* mass-dimension length-dimension (expt time-dimension -2))) (= work (* force length-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))))))) (define-instance IDENTITY-DIMENSION (physical-dimension) "The identity element for the * operator over physical-dimensions. This is the dimension of the so-called dimensionless quantities. It is the dimension of real numbers, considered as quantities." :axiom-def (identity-element-for identity-dimension * physical-dimension)) (define-class FUNDAMENTAL-DIMENSION-SET (?set-of-dimensions) "A set of orthogonal dimension; 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)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; UNIT-OF-MEASURE ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define-class UNIT-OF-MEASURE (?u) "A quantity which is a standard of measurement such as meters, inches, square-feet. All units have an associated physical dimension. Units-of-measure can either be atomic primitives or can be constructed as products of units or units raised to real exponents." :def (and ;; A unit is a physical 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)))))) ;; any composition of units is a unit :sufficient (exists (?a ?b) (or (and (unit-of-measure ?a) (unit-of-measure ?b) (= ?u (* ?a ?b))) (and (unit-of-measure ?a) (real-number ?b) (= ?u (expt ?a ?b))))) :axiom-def (and ;; units can be combined with * to produce units (abelian-group unit-of-measure * identity-unit) ;; * 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. This is the real number 1. Its dimension is the identity-dimension." := 1 :axiom-def (= (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 set of standard units of measure. The function standard-unit maps physical dimensions to units in the system of units (can only have one unit per dimension). A fixed set of base-units are given by fiat, and their dimensions are the fundamental dimensions of the system. All other units in the system are standard units for some dimension composed from these fundamental dimensions." :iff-def (and ;; a system of units is a CLASS of units (class ?system) (subclass-of ?system unit-of-measure) ;; It defines a set of base units whose dimensions are fundamental (defined (base-units ?system)) (=> (member ?unit (base-units ?system)) (instance-of ?unit ?system)) (fundamental-dimension-set (setofall ?dim (exists ?unit (and (member ?unit (base-units ?system)) (= ?dim (dimension ?unit)))))) ;; Every unit in the system is the standard unit for its dimension. (=> (instance-of ?unit ?system) (= (standard-unit ?system (dimension ?unit)) ?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, and (unit* meter second), then it would NOT be a system of units, because the dimension of (unit* meter second) 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." :def (and (system-of-units ?system-of-units) (physical-dimension ?dimension) (unit-of-measure ?unit) (instance-of ?unit ?system-of-units) (= (dimension ?unit) ?dimension)))