Handling implicit dependence on time

We have chosen to specify the semantics of CML by providing a translation into logic. One important aspect of this translation is the representation of time.

A time-quantity is a numeric everywhere continuous quantity whose dimension is the time-dimension. This is the only choice that is consistent with the standard mathematics for ODEs. Other representations of time, such as Allen's temporal relations, can be constructed from this one.

All time dependent quantities and relations in CML have a time-quantity as an implicit argument. To provide a translation into logic, this implicit dependence must be made explicit. In the formalization, we have chosen to make the dependence of functions and relations on time explicit by augmenting them with a first argument that is a time-quantity. Thus, the time dependent relation q becomes where t is a time-quantity.

This is not, however, sufficient to provide a correct translation for time dependent quantities. Consider the following examples:

CML syntax Inadequate translation

1. (= q1 (+ q2 q3)) (= (q1 ?t) (+ (q2 ?t) (q3 ?t)))

2. (= q1 (d/dt q2)) (= (q1 ?t) (d/dt (q2 ?t)))

The first expression is correct. It states that q1 is the sum of q2 and q3 if, for every time ?t, the value of q1 at ?t is the sum of the values of q2 and q3 at the same ?t. The second expression, however, is incorrect. The argument to d/dt, (q2 ?t), is a term denoting a number. The derivative of a number is, of course, 0, which is not at all what is desired. The problem is that some mathematical functions such as d/dt map functions to functions, whereas others, such as +, typically map numbers to numbers. Simply making the dependence on time explicit does not make this necessary distinction.

Within the logic defined by KIF, the derivative case could be handled by replacing q2 with the function:

(lambda (?t1)(if (= ?t1 ?t)(value-at q2 ?t1)))

The function value-at returns the value of the quantity q2 at the time ?t1. This lambda function is correctly mapped to its derivative by d/dt.

In the translation of CML into logic,   time is handled in three steps:

1. Every time dependent relation is augmented with a first argument, which must be a time-quantity.
2. Every time dependent quantity, q, is uniformly translated with the form:

    
   (lambda (?t1) \+
   
        (if (= ?t1 ?t) \+
   
              (value-at q ?t1)))
   
   

3. Every mathematical function that typically applies to numbers (constant quantities) is polymorphically extended to apply to function quantities as well.

The correct translation of our example is thus:

 (= (lambda (?t1)(if (= ?t1 ?t)(value-at q1 ?t1)))

		        (+ (lambda (?t1)(if (= ?t1 ?t)(value-at q2 ?t1)))

		 		          (lambda (?t1)(if (= ?t1 ?t)(value-at q1 ?t1)))

and

 (= (lambda (?t1)(if (= ?t1 ?t)(value-at q1 ?t1)))

		        (d/dt (lambda (?t1)(if (= ?t1 ?t)(value-at q2 ?t1)))

We can extend the definition of + with an axiom such as:

(=> (and (+ ?x ?y ?z)
         (function-quantity ?x) (function-quantity ?y) 
         (function-quantity ?z))
    (forall ?t
       (+ (value-at ?x ?t) (value-at ?y ?t) (value-at ?z ?t))))

Every mathematical operation that typically applies to numbers must be extended similarly. Note that such a mathematical relation is false when any of its arguments is undefined.