;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; Scalar Quantities;;; (c) 1993 Greg Olsen and Thomas Gruber(in-package "ONTOLINGUA-USER") (define-theoryscalar-quantities(physical-quantities) "The term 'scalar' is often equated with the field of real numbers. In this theory we extend that notion to quantities in general, which are associated with dimensions and units. Scalar quantities are quantities whose magnitude is a real number, such as 'the length of rod a'. The normal operators for real arithmetic such as + and *, and the relation<, are extended to the case of scalar quantities (i.e., to consider dimensions and units). Scalar-Quantities are disjoint from vectors quantities, and scalar functions." :issues ("(c) 1993, 1994 Greg R. Olsen and Thomas R. Gruber" (:see-also "The EngMath paper on line"))) (in-theory 'scalar-quantities);;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Scalar-Quantities;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;(define-classSCALAR-QUANTITY(?q) "A scalar-quantity is a constant quantity whose magnitude is a real number. An important property of scalar-quantities is that they form a field with respect to the addition and multiplication (with proper subclass restrictions). The class of scalar-quantities forms a partial order with the less-than relation<, since<is a relation-extended-to-quantities and<is defined over the reals. The<relation is not a total order over the class of scalar-quantity since elements from some subclasses such as length quantities are incomparable to elements from other subclasses such as mass quantities.";; all scalar-quantities are quantities whose magnitude is a real number:iff-def (and (constant-quantity ?q) (forall ?u (=> (and (unit-of-measure ?u) (compatible-quantities ?u ?q)) (real-number (magnitude ?q ?u))))) :axiom-def (and (superclass-of scalar-quantity real-number) (partial-order scalar-quantity<))) (define-instanceIDENTITY-SCALAR(scalar-quantity) "The 'one' element for scalar-quantites or the identity element with respect to multiplication. This element is unique and common to all scalar-quantities regardless of associated physical dimension. Therefore this element is equal to the number 1. The axioms tell us that the product of any scalar-quantity x and the identity-scalar is x." := 1 :axiom-def (and (= (quantity.dimension identity-scalar) identity-dimension) (identity-element-for identity-scalar * scalar-quantity))) (define-function+(?x ?y) :-> ?z "+ defines the specialization of the quantity addition operator + for scalar-quantities. The operator enforces the restriction that the quantities be compatible. The operator is defined in terms of the number addition operator + and the magnitudes of quantities for a particular unit. Scalar-Quantities of a common dimension form an abelian group with respect to this operator and the zero-scalar of the same physical dimension." :when (and (scalar-quantity ?x) (scalar-quantity ?y)) :iff-def (and (scalar-quantity ?z) (forall ?u (=> (and (unit-of-measure ?u) (compatible-quantities ?x ?u)) (= (+ (magnitude ?x ?u) (magnitude ?y ?u)) (magnitude ?z ?u))))) :axiom-def (forall ?d (=> (physical-dimension ?d) (abelian-group (scalar-quantities-of-dimension ?d) + (the-zero-scalar-for-dimension ?d))))) (define-function*(?x ?y) :-> ?z "* defines the specialization of the quantity multiplication operator * for scalar-quantities. The operator enforces the relationship between the physical-dimensions of the operands and the product. The operator is defined in terms of the number multiplication operator * and the magnitudes of quantities for a particular unit. Scalar-Quantities excluding all the zero-scalars form an abelian group with respect to this operator and the identity-scalar<1>. This operator distributes over the + operator for scalar-quantities, providing a field behavior with restrictions." :when (and (scalar-quantity ?x) (scalar-quantity ?y)) :iff-def (and (scalar-quantity ?z) (forall (?u ?u1 ?u2) (=> (and (unit-of-measure ?u) (compatible-quantities ?x ?u) (unit-of-measure ?u1) (compatible-quantities ?y ?u1) (unit-of-measure ?u1) (= (quantity.dimension ?u2) (* (quantity.dimension ?u) (quantity.dimension ?u1)))) (= (* (magnitude ?x ?u1) (magnitude ?y ?u2)) (magnitude ?z ?u))))) :axiom-def (abelian-group (kappa (?x) (and (scalar-quantity ?x) (forall ?dim (=> (physical-dimension ?dim) (/= (the-zero-scalar-for-dimension ?dim) ?x))))) * 1)) (define-functionRECIP(?x) :-> ?y "RECIP defines the specialization of the multiplicative inverse operator for scalar-quantities." :when (scalar-quantity ?x) :def (and (scalar-quantity ?y) (forall ?dim (=> (/= ?x (the-zero-scalar-for-dimension ?dim)) (= (* ?x ?y) identity-scalar))))) (define-functionEXPT(?x ?r) :-> ?z "EXPT defines real exponentiation for scalar-quantities. Specializes EXPT." :when (and (scalar-quantity ?x) (real-number ?r)) :def (and (scalar-quantity ?z) (=> (= ?r 0) (= ?z 1)) (forall ?u (=> (unit-of-measure ?u) (= (EXPT (magnitude ?x ?u) ?r) (magnitude ?z (EXPT ?u ?r))))))) (define-functionSCALAR-QUANTITIES-OF-DIMENSION(?dimension) :-> ?class "Scalar-Quantities are partitioned into classes of uniform dimension. All instances of one of these classes have the same physical dimension. Each of these classes form a linear order with respect to the<relation. Length scalars, time scalars, and mass scalars are examples of scalar subclasses.";; all instances ?x of ?class are scalars of the same dimension.:= (if (physical-dimension ?dimension) (kappa (?q) (and (scalar-quantity ?q) (= (quantity.dimension ?q) ?dimension)))) :constraints (and (physical-dimension ?dimension) (class ?class) (linear-order ?class<))) (define-functionTHE-ZERO-SCALAR-FOR-DIMENSION(?dimension) :-> ?zero-scalar "The zero element for scalars of physical-dimension ?dimension. The real number 0 is the zero scalar-quantity for quantities of identity-dimension (i.e., dimensionless scalars). We make the distinction between 0 meters and 0 seconds, for instance, to maintain our compatibility requirements for operators such as addition (i.e. a length quantity + a length quantity always equals another length quantity). In practice, the distinction between zero quantities may not be important to any models, but there inclusion frees us from special cases for composition of quantities of different dimensions." :iff-def (and (physical-dimension ?dimension) (scalar-quantity ?zero-scalar) (zero-quantity ?zero-scalar) (identity-element-for ?zero-scalar + (scalar-quantities-of-dimension ?dimension))) :axiom-def (= 0 (THE-ZERO-SCALAR-FOR-DIMENSION identity-dimension)))