;;; -*- Mode:Lisp; Syntax: Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; Tensor Quantities
;;; (c) 1993 Greg Olsen and Thomas Gruber

(in-package "ONTOLINGUA-USER")

(define-theory tensor-quantities (basic-matrix-algebra
				  scalar-quantities)
  "This theory is used to represent vectors of n spatial dimensions
which are physical quantities with physical dimensions, such as 'the
velocity of particle p'.  The theory supports arbitrary numbers of
basis vector sets and hence vectors are not isomorphic to n-tuples as
is the case in some textbook representations of vectors (Note:
Multi-basis vector spaces are essential to many theories such as
kinematics).  Standard vector operations such as vector addition,
scalar multiplication, and scalar or dot product are supported.
Operators on vector-quantities must take into account the associated
units and dimensions.
  The theory now also include higher-order tensors."
  :issues ("(c) 1993, 1994 Gregory R. Olsen and Thomas R. Gruber"
	   (:see-also "The EngMath paper on line")))

(in-theory 'tensor-quantities)

(define-class TENSOR-QUANTITY (?T)

  "Every tensor has an associated spatial dimension and tensor order.  Each
tensor-quantity can be decomposed into scalar components for a given
orthonormal basis of the proper dimension (except of .  The physical-dimension
of a scalar component of the tensor-quantity is equivalent to the
physical-dimension of the tensor-quantity."
  
  :def (and (constant-quantity ?T)
	    (defined (tensor-order ?T))
	    (non-negative-integer (tensor-order ?T))
	    (defined (spatial.dimension ?T))
	    (non-negative-integer (spatial.dimension ?T)))
  
  :axiom-def (<=> (and (tensor-quantity ?t)
		       (= (tensor-order ?t) 0))
		  (scalar-quantity ?t)))
	    
		  
(define-function SPATIAL.DIMENSION (?t) :-> ?n
  "Function that returns the spatial dimension associated with a tensor."
  :def (and (tensor-quantity ?t)
	    (positive-integer ?n))
  :issues ((:formerly-called vector.dimension)))


(define-function TENSOR-ORDER (?t) :-> ?n
  "Function that returns the order associated with a tensor."
  :def (and (tensor-quantity ?t)
	    (non-negative-integer ?n)))


(define-class VECTOR-QUANTITY (?v)

  "The class of quantities which are n-dimensional vectors (first order
tensor-quantities). Each vector has an associated spatial dimension and an
associated physical dimension.  Each vector-quantity can be decomposed into
scalar components for a given orthonormal basis of the proper dimension.  The
physical-dimension of a scalar component of the vector-quantity is equivalent
to the physical-dimension of the vector-quantity."

  :iff-def (and (constant-quantity ?v)
		(tensor-quantity ?v)
		(= (tensor-order ?v) 1)
		(forall (?b ?i)
			(=> (and (orthonormal-basis ?b)
				 (= (basis.dimension ?b) 
				    (spatial.dimension ?v))
				 (positive-integer ?i)
				 (=< ?i (spatial.dimension ?v)))
			    (and (defined (vector-component ?v ?i ?b)) 
				 (= (quantity.dimension
				     (vector-component ?v ?i ?b))
				    (quantity.dimension ?v)))))

		(forall ?u (=> (and (unit-of-measure ?u)
                                    (= (quantity.dimension ?u) 
                                       (quantity.dimension ?v)))
			       (numeric-tensor (magnitude ?v ?u))))))


(define-class DYAD (?d) 

  "The class of second order tensors (aka tensors).  Given an orthornormal
basis a dyad can be decomposed into scalar components.  These components can
be represented as a square matrix.  The matrix is not unique but it a 'view'
of the tensor for a particular basis."

  :iff-def (and (constant-quantity ?d)
		(tensor-quantity ?d)
		(= (tensor-order ?d) 2)
		(forall (?b ?i ?j)
			(=> (and (orthonormal-basis ?b)
				 (= (basis.dimension ?b) 
				    (spatial.dimension ?d))
				 (positive-integer ?i)
				 (=< ?i (spatial.dimension ?d))
				 (positive-integer ?j)
				 (=< ?j (spatial.dimension ?d)))
			    
			    (and (defined (dyad-component ?d ?i ?j ?b)) 
				 (= (quantity.dimension
				     (dyad-component ?d ?i ?j ?b))
				    (quantity.dimension ?d)))))

		(forall ?u (=> (and (unit-of-measure ?u)
                                    (= (quantity.dimension ?u) 
                                       (quantity.dimension ?d)))
			       (numeric-tensor (magnitude ?d ?u))))))


(define-class MATRIX-QUANTITY (?M)
  "Class of matrices whose elements are quantities"
  :iff-def (and (matrix ?M)
		(physical-quantity ?M) 
		(forall (?i ?j)
			(=> (defined (value ?M ?i ?j))
			    (= (quantity.dimension ?M)
			       (quantity.dimension (value ?M ?i ?j)))))))


(define-class NUMERIC-MATRIX (?M)
  "Class of matrices whose elements are nondimensional quantities"
  :iff-def (and (matrix-quantity ?M)
		(dimensionless-quantity ?M))
  :axiom-def (superclass-of numeric-matrix identity-matrix))


(define-class UNIT-VEC (?v)
  "Unit length vectors."
  :iff-def (and (vector-quantity ?v)
		(= (quantity.dimension ?v) identity-dimension)
		(= (dot ?v ?v) 1)))


(define-class ORTHONORMAL-BASIS (?b)
  "A set of n vector-quantities in an n-dimensional vector space which
form an ortho-normal basis, the n vector-quantities are linearly
independent and the scalar product of any two is the identity-scalar."
  :def (and (defined (basis.dimension ?b))
	    (forall ?n (=> (and (positive-integer ?n)
				(=< ?n (basis.dimension ?b)))
			   (defined (basis.vec ?b ?n))))
	    (forall (?n1 ?n2)
		    (=> (and (positive-integer ?n1)
			     (positive-integer ?n2)
			     (=< ?n1 (basis.dimension ?b))
			     (=< ?n2 (basis.dimension ?b)))
			(=> (= ?n1 ?n2)
			    (= (dot (basis.vec ?b ?n1) (basis.vec ?b ?n2))
			       1))
			(=> (/= ?n1 ?n2)
			    (= (dot (basis.vec ?b ?n1) (basis.vec ?b ?n2))
			       0))))))


(define-function BASIS.VEC (?basis ?n) :-> ?uv
  "Function to select the individual unit vectors of a basis."
  :def (and (orthonormal-basis ?basis)
	    (positive-integer ?n)
	    (=< ?n (basis.dimension ?basis))
	    (unit-vec ?uv)))


(define-function BASIS.DIMENSION (?b) :-> ?n
  "Function that returns the spatial dimension associated with a basis
set of vectors."

  :def (and (orthonormal-basis ?b)
	    (positive-integer ?n)))

(define-function TENSOR-to-MATRIX (?T ?basis) :-> ?M 
  "Function that maps a tensor to matrix for a particular basis.
Tensor-to-Matrix is defined for first and second order tensors
(vector-quantities & dyads).  Tensor-to-Matrix maps a vector-quantity into a
row matrix of column-dimension equal to the spatial.dimension of the
vector-quantity.  Dyads are mapped into square matrices of row- and
column-dimension equal to the spatial dimension of the dyad.  The scalar
components of the resulting matrices corresspond to dot (inner) products of
the tensor with appropriate basis vectors."
  :iff-def (and (tensor-quantity ?T)
		(orthonormal-basis ?basis)
		(=> (member ?q (tensor-order ?T))
		    (member ?q (setof 1 2)))
		(matrix-quantity ?M)
		
		(=> (= (tensor-order ?T) 1)
		    (= (row-dimension ?M) 1)
		    (= (column-dimension ?M)
		       (spatial.dimension ?T))
		    (forall ?i
			    (= (value ?M 1 ?i)
			       (vector-component ?T ?i ?basis))))
		 
		(=> (= (tensor-order ?T) 2)
		    (square-matrix ?M)
		    (= (size ?M)
		       (spatial.dimension ?T))
		    (forall (?i ?j)
			    (= (value ?M ?i ?j)
			       (dyad-component ?T ?i ?j ?basis))))))
		 
;;;;;;;;;;;;;;;;;;;;;;

(define-class NUMERIC-TENSOR (?x)

  "A numeric-valued tensor.  Its components expressed in any basis are
numeric or non-dimensional."

  :def (and (tensor-quantity ?x)
	    (dimensionless-quantity ?x)))


(define-function VECTOR-COMPONENT (?v ?i ?b) :-> ?s

  "Function to generate the ith scalar component for a vector-quantity in a
particular basis.  The ith scalar component is the dot (inner) product of the
vector-quantity with the ith basis vector of the given basis."

  :iff-def (and (vector-quantity ?v)
		(positive-integer ?i)
		(orthonormal-basis ?b)
		(scalar-quantity ?s)
		(= (quantity.dimension ?s)
		   (quantity.dimension ?v))
		(= (spatial.dimension ?v)
		   (basis.dimension ?b))
		(=< ?i (spatial.dimension ?v))
		(= ?s (dot ?v (basis.vec ?b ?i)))))

(define-function DYAD-COMPONENT (?T ?i ?j ?basis) :-> ?s

  "Function to generate the i,j th scalar component for a dyad in a particular
basis.  The i,j scalar component of dyad T is equal to bi*T*bj (basis vector i
dot T dot basis vector j."

  :iff-def (and (dyad ?T)
		(positive-integer ?i)
		(positive-integer ?j)
		(orthonormal-basis ?basis)
		(scalar-quantity ?s)
		
		(= (quantity.dimension ?s)
		   (quantity.dimension ?T))
		
		(= (spatial.dimension ?T)
		   (basis.dimension ?b))
		
		(=< ?i (spatial.dimension ?T))
		(=< ?j (spatial.dimension ?T))
		
		(= ?s (dot (basis.vec ?basis ?i)
			   (dot ?T
				(basis.vec ?b ?j))))))

(define-function THE-VECTOR-QUANTITY (?M ?b) :-> ?v

  "Constructor function for vector quantities (first order tensors).  Requires
a matrix and an orthnormal-basis as arguments.  The constructed
vector-quantity is equal to the sum of matrix elements multiplied by their
corresponding basis vectors."

  :iff-def (and (matrix-quantity ?M)
		(row-matrix ?M)
		(orthonormal-basis ?b)

		(= (quantity.dimension ?v)
		   (quantity.dimension ?M))
		
		(= (column-dimension ?M)
		   (basis.dimension ?b))
		
		(= (spatial.dimension ?v)
		   (column-dimension ?M))
		
		(vector-quantity ?v)
		(= ?v (summation
		       (lambda (?j) (* (value ?M 1 ?j)
				       (basis.vec ?b ?j)))
		       1
		       (spatial.dimension ?v))))

:issues ((:example
            (= (the-vector-quantity
		(matrix-of-columns (* 3 feet) 
				   (* 1 yard))
		2D-frame-n)
	       (* 
		(the-vector-quantity (matrix-of-columns 3 3) 2D-frame-n)
		feet)))))


(define-function THE-DYAD (?M ?b) :-> ?T

  "Constructor function for second order tensors.  Requires a matrix and an
orthnormal-basis as arguments.  The constructed dyad is equal to the sum of
products of matrix elements with the corresponding basis vectors."

  :iff-def (and (matrix-quantity ?M)
		(square-matrix ?M)
		(orthonormal-basis ?b)

		(= (quantity.dimension ?T)
		   (quantity.dimension ?M))
		
		(= (size ?M)
		   (basis.dimension ?b))
		
		(= (spatial.dimension ?T)
		   (size ?M))
		
		(dyad ?T)
		(= ?T (summation
		       (lambda (?i)
			 (summation
			  (lambda (?j)
			    (* (basis.vec ?b ?i)
			       (* (value ?M ?i ?j)
				  (basis.vec ?b ?j))))
			    1
			    (spatial.dimension ?T)))
			 1
			 (spatial.dimension ?T))))

  :issues ((:example
            (= (the-dyad
		(matrix-of-columns
		 (matrix-of-rows (* 3 feet) (* 1 yard))
		 (matrix-of-rows (* 24 inches) (72 inches)))
				    2D-frame-n)
	       (* 
		(the-dyad
		 (matrix-of-rows
		  (matrix-of-columns 3 2)
		  (matrix-of-columns 3 6))
		 2D-frame-n)
		feet)))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;  Tensor Operators (orders less than 3)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; - - - - - - - ADDITION - - - - - - - - -
;; Pair of Tensors
(define-function + (?x ?y) :-> ?z

  "For Tensors in general:

Addition is defined for two tensors of equal spatial dimension, and results
in a tensor of the same spatial dimension.  The usual restrictions for
physical-quantities also apply.

For Vectors:

When defined, the addition of vector-quantities can be decomposed into
additions of scalar components.  This decomposition corresponds to choosing an
arbitrary basis, mapping the vector-quantities to components in that basis,
and summing appropriate components.

For Dyads,

When defined, the addition of dyads can be decomposed into additions of
scalar components.  This decomposition corresponds to choosing an arbitrary
basis, mapping the dyads to components in that basis, and summing appropriate
components.
"

  :when (and (tensor-quantity ?x)
	     (tensor-quantity ?y))
  :def (and 
	(tensor-quantity ?z)
	(= (spatial.dimension ?x) (spatial.dimension ?y))
	(= (spatial.dimension ?x) (spatial.dimension ?z)))

  :axiom-def
  (and
   ;; :when (and (vector-quantity ?x) (vector-quantity ?y))
   (=> (and (vector-quantity ?x) (vector-quantity ?y))
       (=> (+ ?x ?y ?z)
	   (and (vector-quantity ?z)
		(forall (?b ?i)
			(=> (and (orthonormal-basis ?b)
				 (= (spatial.dimension ?x) (basis.dimension ?b))
				 (positive-integer ?i)
				 (=< ?i (spatial.dimension ?x)))
			    (= (vector-component ?z ?i ?b)
			       (+ (vector-component ?x ?i ?b)
				  (vector-component ?y ?i ?b))))))))
   (forall (?physdim ?spatdim)
	   (abelian-group 
	    (vector-quantities-of-dimensions ?physdim ?spatdim)
	    + 
	   (the-zero-vector-of-type ?spatdim ?physdim)))
   ;; :when  (and (dyad ?x) (dyad ?y))
   (=> (and (dyad ?x) (dyad ?y))
       (=> (+ ?x ?y ?z)
	   (and 
	    (dyad ?z)
	    (forall (?b ?i ?j)
		    (=> (and (orthonormal-basis ?b)
			     (= (spatial.dimension ?x)
				(basis.dimension ?b))
			     (positive-integer ?i)
			     (positive-integer ?j)
			     (=< ?i (spatial.dimension ?x))
			     (=< ?j (spatial.dimension ?x)))
			(= (dyad-component ?z ?i ?j ?b)
			   (+ (dyad-component ?x ?i ?j ?b)
			      (dyad-component ?y ?i ?j ?b))))))))
   (forall (?physdim ?spatdim)
	   (abelian-group 
	    (dyad-of-dimensions ?physdim ?spatdim)
	    + 
	    (the-zero-dyad-of-type ?spatdim ?physdim)))
   ))


;; - - - - - - - UNARY MINUS - - - - - - - - -

(define-function - (?x) :-> ?y

  "The unary minus function is also defined for vector quantities."

  :when (vector-quantity ?x)
  :def (and (vector-quantity ?y)
		(= (+ ?x ?y) 
		   (the-zero-vector-of-type (quantity.dimension ?x) 
                                            (spatial.dimension ?x)))))

;; - - - - - - - DOT or INNER PRODUCT - - - - - - - - -

(define-function DOT (?t1 ?t2) :-> ?t

  "The DOT or inner product is defined for tensors of the same spatial
dimension.  The quantity.dimension of the product equals the product of the
quantity.dimensions of the operands.  The dot operator distributes over
addition.

For vectors:

When the operands are both vector-quantities, the dot (scalar product) can
be decomposed into the multiplication of a row- and a column-matrix.  The
product is a scalar (zero order tensor) and is the sum of the products of the
corresponding scalar components of the argument vectors for a common basis.

For dyads:

When the operands are both dyads, the dot product can be decomposed into
a multiplication of square matrices (with dimension equal to the
spatial.dimension of the dyads).  The product is a dyad (second order tensor)
and is equal to the sum of the products of the corresponding scalar components
of the argument tensors for a common basis.


For dyad dot vector:

The dot product of a dyad and a vector-quantity results in a
vector-quantity.  This product can be decomposed into the multiplication of a
square matrix an a column-matrix or row-matrix.  The product is a
vector-quantity (first order tensor) and is equal to the sum of the products
of the corresponding scalar components of the argument tensors for a common
basis.

The reverse, vector dot dyad, is analogous."
  
  :def (and (tensor-quantity ?t1)
	    (tensor-quantity ?t2)
	    (tensor-quantity ?t)
	    (= (spatial.dimension ?t1)
	       (spatial.dimension ?t2))
	    (= (quantity.dimension ?t) 
	       (* (quantity.dimension ?t1)
		  (quantity.dimension ?t2))))
  :axiom-def
  (and
   (distributes dot + tensor-quantity)
   ;; when (and (vector-quantity ?v1) (vector-quantity ?v2))
   (=> (and (vector-quantity ?v1) (vector-quantity ?v2))
       (<=> (dot ?v1 ?v2 ?s)
	    (and (scalar-quantity ?s)
		 (forall ?b
			 (= ?s
			    (value
			     (* (tensor-to-matrix ?v1 ?b)
				(transpose
				 (tensor-to-matrix ?v2 ?b)))
			     1 1)))
		 (forall (?b ?j)
			 (=> (= (basis.dimension ?b)
				(spatial.dimension ?v1))
			     (= ?s 
				(summation
				 (lambda (?j) 
				   (* (vector-component ?v1 ?j ?b)
				      (vector-component ?v2 ?j ?b)))
				 1
				 (spatial.dimension ?v1))))))))
   
   ;; :when (and (dyad ?T1) (dyad ?T2))
   (=> (and (dyad ?T1) (dyad ?T2))
       (<=> (dot ?t1 ?t2 ?t)
	    (and (dyad ?t)
		 (forall ?b
			 (= ?t
			    (the-dyad 
			     (* (tensor-to-matrix ?T1 ?b)
				(tensor-to-matrix ?T2 ?b))
			     ?b)))
		 (forall (?b ?i ?j)
			 (=> (= (basis.dimension ?b)
				(spatial.dimension ?T1))
			     (= ?t 
				(summation
				 (lambda (?i)
				   (summation
				    (lambda (?j)
				      (*
				       (* (basis.vec ?b ?i)
					  (basis.vec ?b ?j))
				       (* (dyad-component ?T1 ?i ?j ?b)
					  (dyad-component ?T2 ?j ?i ?b))))
				    1
				    (spatial.dimension ?T1)))
				 1
				 (spatial.dimension ?T1))))))))
   ;; :when (and (dyad ?T1) (vector-quantity ?v1))
   (=> (and (dyad ?T1) (vector-quantity ?v1))
       (<=> (dot ?t1 ?v1 ?v)
	    (and (vector-quantity ?v)
		 (forall ?b
			 (= ?t
			    (the-vector-quantity
			     (transpose
			      (* (tensor-to-matrix ?T1 ?b)
				 (transpose
				  (tensor-to-matrix ?v1 ?b))))
			     ?b)))
		
		 (forall (?b ?i ?j)
			 (=> (= (basis.dimension ?b)
				(spatial.dimension ?v1))
			     (= ?t 
				(summation
				 (lambda (?i)
				   (* (basis.vec ?b ?i)
				      (summation
				       (lambda (?j)
					 (* (dyad-component ?T1 ?i ?j ?b)
					    (vector-component ?v1 ?j ?b)))
				       1
				       (spatial.dimension ?v1))))
				 1
				 (spatial.dimension ?v1))))))))

   ;; :when (and (vector-quantity ?v1) (dyad ?T1))
   (=> (and (vector-quantity ?v1) (dyad ?T1))
       (<=> (dot ?v1 ?t1 ?v)
	    (and (vector-quantity ?v)
		 (forall ?b
			 (= ?t
			    (the-vector-quantity
			     (* (tensor-to-matrix ?v1 ?b)
				(tensor-to-matrix ?T1 ?b))
			     ?b)))
		 (forall (?b ?i ?j)
			 (=> (= (basis.dimension ?b)
				(spatial.dimension ?v1))
			     (= ?t 
				(summation
				 (lambda (?i)
				   (* (basis.vec ?b ?i)
				      (summation
				       (lambda (?j)
					 (* (vector-component ?v1 ?j ?b)
					    (dyad-component ?T1 ?j ?i ?b)))
				       1
				       (spatial.dimension ?v1))))
				 1
				 (spatial.dimension ?v1))))))))
   ))

;; - - - - - - - MULTIPLICATION - - - - - - - - -

(define-function * (?s ?v1) :-> ?v

  "Multiplication of a vector-quantity by a scalar-quantity results in a
vector-quantity.  The product is equal to the vector-quantity constructed by
multiplying each component of the argument vector by the argument scalar.
   The * function is commutative for scalar/vector pairs."

  :when (and (scalar-quantity ?s)
	    (vector-quantity ?v1))
  :def (and (vector-quantity ?v)
	    (= (spatial.dimension ?v1) (spatial.dimension ?v))
	    (forall (?b ?i)
		    (=> (= (basis.dimension ?b) (spatial.dimension ?v1))
			(= (vector-component ?v ?i ?b)
			   (* ?s (vector-component ?v1 ?i ?b))))))
  :axiom-def (=> (and (vector-quantity ?v1)
		      (scalar-quantity ?s))
		 (= (* ?v1 ?s) (* ?s ?v1)))
  )



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;  Other Definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define-function THE-ZERO-VECTOR-OF-TYPE (?spatdim ?physdim) :-> ?v0

  "The ?spatdim dimensional zero vector of physical dimension ?physdim."

  :def (and (vector-quantity ?v0)
	    (positive-integer ?spatdim)
	    (physical-dimension ?physdim)
	    (forall ?v
	       (=> (vector-quantity ?v)
		   (= (dot ?v (the-zero-vector-of-type ?spatdim ?physdim))
		      (the-zero-scalar-for-dimension ?physdim))))))


(define-function VECTOR-QUANTITIES-OF-DIMENSIONS (?physim ?spatdim) :-> ?class

   := (if (and (physical-dimension ?physim)
	       (positive-integer ?spatdim))
	  (kappa (?vq)
		 (and (vector-quantity ?vq)
		      (= (spatial.dimension ?vq) ?spatdim)
		      (= (quantity.dimension ?vq) ?physim)))))


(define-function THE-ZERO-DYAD-OF-TYPE (?spatdim ?physdim) :-> ?v0

  "The ?spatdim dimensional zero dyad of physical dimension ?physdim."

  :def (and (dyad ?v0)
	    (positive-integer ?spatdim)
	    (physical-dimension ?physdim)
	    (forall ?v
	       (=> (dyad ?v)
		   (= (dot ?v (the-zero-dyad-of-type ?spatdim ?physdim))
		      (the-zero-scalar-for-dimension ?physdim))))))


(define-function DYAD-OF-DIMENSIONS (?physim ?spatdim) :-> ?class

   := (if (and (physical-dimension ?physim)
	       (positive-integer ?spatdim))
	  (kappa (?vq)
		 (and (dyad ?vq)
		      (= (spatial.dimension ?vq) ?spatdim)
		      (= (quantity.dimension ?vq) ?physim)))))


This Lisp-to-HTML translation was brought to you by
François Gerbaux and Tom Gruber