;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-
;;; Scalar Quantities
;;; (c) 1993 Greg Olsen and Thomas Gruber
(in-package "ONTOLINGUA-USER")
(define-theory scalar-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-class SCALAR-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-instance IDENTITY-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-function RECIP (?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-function EXPT (?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-function SCALAR-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-function THE-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)))
This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber