Function DISTANCE

• Defined in theory: Quantity-spaces
• Source code: quantity-spaces.lisp
• Also defined in: Simple-geometry

Slots on this function:

Documentation:

The DISTANCE function is intended to be polymorphically defined for each quantity space. Its always maps two points in the space to a scalar-quantity. It must be commutative.

Instance-Of: Function

Arity: 3

Axioms:

(Nth-Domain Distance 3 Scalar-Quantity)

(= (Distance ?B ?C) (Distance ?C ?B))

(Zero-Quantity (Distance ?A ?A))

Other Related Axioms:

(Forall (?X1 ?X2)
        (=> (And (Member ?X1 ?S) (Member ?X2 ?S))
            (Exists (?D)
                    (And (= ?D (Distance ?X1 ?X2))
                         (Scalar-Quantity ?D)))))

(<=> (Quantity-Space ?S)
     (And (Set ?S)
          (Forall (?X1 ?X2)
                  (=> (And (Member ?X1 ?S) (Member ?X2 ?S))
                      (Exists (?D)
                              (And (= ?D (Distance ?X1 ?X2))
                                   (Scalar-Quantity ?D)))))))

(Instance-Of (Distance ?A ?A) Zero-Quantity)

(=> (= (Distance ?X1 ?X2) ?D)
    (Exists (?Sp)
            (And (Quantity-Space ?Sp)
                 (Point-In ?X1 ?Sp)
                 (Point-In ?X2 ?Sp))))