Wristwatch: Reasoning about Time




HOME

Wristwatch: Reasoning about Time

Version 3.001 2013-09-21

Authors:: Richard Weyhrauch (IBUKI), Carolyn Talcott
Note:: The information in this document (and its companion documents) is the confidential proprietary property of IBUKI. It contains trade secret, published and unpublished components. These documents and the IBML system (appearing under various names) has been developed over a substantial period of time at IBUKI's expense.

Abstract

This paper describes how to construct [fol-context]s and use them to reason about time without using indexicals or model logic. It also addresses the question of how we can know anything "for sure" in an ever-changing asynchronous behaving world?

Introduction

In this note we show how [fol-context]s\cite{fol-url,fol-little-intro, ol-little-pgm} can be used build an artifact that can answer questions about time. This approach has several interesting properties:

We define a collection of [fol-system]s, [Tot]s, that always give correct answers when asked simple questions about what time it is.
Does not use indexicals, but it knows about now and then and furthermore it knows that now always comes after then.
Does not use modal or temporal logic.

We show that it is not necessary to extend the semantics of [fol-system]s beyond first order to formalize and answer interesting questions about time.

More important, this theory of time is constructed in such a way that it could be built as a component of the mind of a robot\cite{fol-little-intro}, and as such represents an alternative to the use of logical theories and theorem proving as a way of embedding reasoning capability in the head of a robot.

Wristwatch

What is a wristwatch? It's a device that, when we look at it, tells us what time it is, and otherwise it sits there ticking away by itself until we look at it again. We can simplify the world a little if we imagine that our watch just displays a number, e.g., 14378469252856—let's say the number of seconds since the big bang—and with each second the watch ticks and increments its display by one.

How do we use a watch? Usually, we simply leave it on our wrist ticking until we are interested in knowing what time it is is and then we find out the time by looking at it.

Note:

We do not do anything to make it tick. It runs by itself, without any intervention. Our activities are essentially disjoint from those of the watch.
We do not expect it to give us the same answer each time we look at it! A watch that always says 5:04 is broken. In this sense, as a device for telling time it is not like a "theory" in which "now" has a fixed meaning. The time changes with every tick.

We construct a “theory” of such a watch by defining a class of [fol-context]s called [wristwatch]s, Ww. An [fol-context] is a [wristwatch], ww, if its language contains only one individual constant now, attached to a natural number and whose set of facts is empty.

We call this [fol-context] a wristwatch, because, like a physical wristwatch, when you ask it what time it is, i.e., now = ??, it gives you back a number (the time).

We represent the ticking of the watch as an operation on [wristwatch]s

ww ==> tick(ww)

which maps wristwatches onto wristwatches, i.e., in the metatheory

Ww(ww) implies Ww(tick(ww))

and where the time, now, in tick(ww) is incremented by one.

Notice that tick is an FOL rule of inference, which preserves the physics, Ww

Here we see a clear case where there is a difference between the semantics of [fol-context]s and the semantics of first order theories. Consider the context

bw₁ = < <now,six> <6,6>, [ ] >

which has two individual constants, now and six, each attached to the number 6, and no facts. $now = six$ is a consequence, so lets add this as a fact, giving

bw₂ = < <now,six>, <6,6.>, [now = six] >

Viewed as descriptions of traditional theories, bw_1$ and $bw_2$ encode the same theory. Now, apply the tick rule to these contexts. This gives"

bw'₁ = tick(bw₁) = < <now,six>, <7,6>, [ ] >

bw'₂ = tick(bw₂) = < <now,six>, <7,6>, [now = six] >

Assuming the standard meaning of 6 and 7 we see that ticking bw₁ preserves satisfaction, i.e., consistency, but ticking bw₂ does not. In a traditional theory, that is, a deductivly closed, therefore infinite, set of formulas, "recognizing a valid consequence" simply means confirming the truth of something already in the theory. The operation of "adding" a valid consequence to a theory is an illusion. If this were the case, "adding" the consequence now = six as a fact to bw₁ would add nothing to the "theory", but, if we think of bw₁ as an [fol-context], the addition of this consequence to the facts of bw₁ has the effect that ticking is no longer a satisfaction preserving operation. The effect of adding this fact (because it was a ‘valid consequence’ of the [fol-context], i.e., it was “already there" in the theory!!) is a mistake—equivalent to smashing a working watch and creating a broken watch for which time is "frozen"!

For [fol-ontext]s, the notion of a ‘fact of a context” (meaning that the formula explicitly referred can be found among the facts of the context) and the notion of a 'consequence of a context’ (a formula that can be validly derived from a context) are different and as we saw adding a consequence to the facts of an [fol-context] destroys the satisfaction preserving property of perfectly reasonable operations (like tick). For this reason the semantics of [fol-contect]s seperates the idea of drawing a consequence of a context and adding that consequence as a fact.

A Static Theory of Time

A context cxt is a static theory of time, Stot(cxt), if the following conditions are satisfied

Its language consists of a two individual constants now, and then, and one binary relation ≤.
The attachments to now and then are natural numbers, where the attachment to then is less than or equal to the attachment to now, and the attachment to ≤ is the ‘less than or equal to’ predicate on natural numbers.
There is one fact stating that then ≤ now.

We write

< < now, then >, <12,4>, [le(then,now)] >

to describe an example of an [fol-context] that is a static theory of time.

We might call the fact that $then <= now$ a law of physics relative to a Static theory of time FOLcontext.

A Dynamic Theory of Time

One thing our common sense theory of time tells us is that then is always before now; Although this is true in the static theory of time, tot, in the previous section, we can still askh e question: "how can we be so certain of this even though clocks are ticking away and time is "moving". In addition, clocks are ticking synchronously with respect to us and each other. Under such a seething sea of changes, how can we say with such certainty that then always comes before now. It is a universal truth standing on sand.

That said, a theory of time that is adequate for our robot MUST also believe this. Furthermore, it seems to us that this statement is naively made without reference to indexicals! It's not

" (t in Time) (then_t ≤ now_t)

it's simply

then ≤ now.

We explain this in the following way:

A system sys is a theory of time. Tot(sys), if it is an [fol-system] that contains two contexts:

a wristwatch
a static theory of time

where the attachment to now in the wristwatch is greater or equal to the attachment to now in the static theory of time. For example

< a : <now>, <17>, [ ] >

< b: <now, then>, <12, 4>, [le(then, now)] >

We extend the operation of ticking to $sys$ in the obvious way—ticking in a theory of time simply ticks the wristwatch.

<a: <now>, <17>, [ ] >
<b: <noe, then>, <12,4>, [le(then,now)] >

tick ==>

<a: <now>, <18>, [ ] >
<b: <now,then>, <12,4> [le(then,now)] >

Note that ticking a theory of time produces a theory of time. By physically embedding a theory of time FOLcontext in our robot, we have a watch that sits on its "wrist" and ticks. In fact, we could imagine implementing a wristwatch [fol-context] as an actual clock!

Now imagine implementing an operation on a theory of time called look. When the robot “looks" at his watch two things happen. First we ”update then" by replacing the attachment to then with the attachment to now. Second we "update now" by asking the wristwatch what time it is, and then attaching this time to now in our static theory of time.

< a: <now>, <18>, [ ] >
< b: <now,then>,<12, 4>, [le(then,now)] >

pdateThen ==>

<a: <now>, <18>, [ ] >
<b: now,then>,<12, 12>, [le(then,now)] >

updateNow ==>

<a: <now>, <18>, [ ] >
<b: <now,then> <18,12>, [le(then,now)] >

Note that either of these operations when thought of as an operation on our theory of time produces a new theory of time. Furthermore, any interleaving of "tick", "update then" and "update now" continues to produce the theories of time!

Now our robot can use its theory of time to determine what time it is by simply doing an "updateNow" and then asking its static theory of time the value now. Similarly, to discover the time of then the robot gets and saves the value of then in the static theory of time, does an "updateThen” and returns the value it saved.

Throughout this, at each step, then <= now!!! This can be verified both by looking at the single fact in the static theory of time, or by semantically evaluating le(then,now) in the static theory of time.

The Physics

We now give a precise description of the theory-of-time physics and associated notions of wristwatch and static-theory-of-time physics using the [fol-context] data structures~\cite{fol-little-cxt}.")

WristWatch

A context, $cxt$, is a wristwatch ($Ww(cxt)$) if it is of the form $ww(n)$ for some number $n$, where

ww(n) = < ww-label,  ww-lang, ww-ss(n), <> >

ww-simtype = < 1, < >, < >,1 >

ww-lang =
   < ww-simtype,
          < Natnum >,              ; One Sort Symbol - the Most General Sort
          < >,                            ; No Relation Symbols
          < >,                            : No Fuction Symbols
          <now> >                      ; One Individual Constant

ww-ss(n) =
      <   < ww-simtype,\csmtenv,\wwreps >
           < < natnumrep, isnatnum > >,
           < >,
           < >,
           < < natnumrep, const(n) > >

#'NATNUM? is a program that returns a representation of yes when applied to a [natnum], n.

The operation tick on wristwatch contexts is defined by tick(ww(n)) = ww(n+1).

and

ww(n) =tick=> ww(n+1)

that is, tick can also be considered an inference rule on [wristwatch]s.

Another wristwatch preserving operation is set set(ww(n),m) = ww(m).

query{now}, is defined by query{now}[ww(n)] = val{ww(n)}(now) = n.

A Static Theory Of Time

A context, cxt, is a static theory of time, Stot(cxt), if cxt is a context of the form stot(m,n) for [natnum]s m, n with m <= n where

where

\stotlang =

   < \stotsimtype,
          < \stotusort >,        ; Sort Symbols
          < \qle>,               ; Relation Symbols
          < >,                   ; Function Symbols
          <then,now >            ; Individual Constant Symbols
   >

\stotsimtype =  <1,  <2>, < >,1>

\stotss =
  <  < \stotsimtype,\csmtenv,\stotreps >,
      < < \natnumrep, \qisnatnum > >,
      < < natnumrep, \qisle >> ,
      < >,
      < < \natnumrep, \const(m) > ,
         < \natnumrep, \const(n)  > >

\stotfacts =
      [ <1:  le(then,now), [], [“law of physics'']
> ]

Note that val{stot(m,n)}(now) = n, and val{tot(m,n)}(then) = m. We may also query a static theory of time context about now and then.

query{now}(tot(m,n)) = val{tot(m,n)}(now) = n query{then}(tot(m,n)) = val{tot(m,n)}(then) = m

We call fact 1 a "law of physics" (and use that as its justification) because the tot physics demands it. Note that it has no dependencies. Thus, if we think of an [fol-context] as determining a set of models (or a set of possible worlds) and the physics as constraining what possible sets of possible worlds we can consider, then we can say that something is a law of physics just in case it is true in each world in every set of possible worlds determined by the physics. This view of [fol-context]s provides a first-order alternative to modal logic as a tool for reasoning about modalities.

Note that in static theory of time we have two ways to determine that le(then,now) is a consequence of every static theory of time. First by observing that

sat{tot(m,n)}(le(then,now))

which will always be true. Or second, by looking at fact 1 and concluding that because it has no dependencies its wff is always true.

A Theory of Time

A theory-of-time system consists of two contexts: a wristwatch and a static theory of time satisfying the constraint that now in the wristwatch is at least as large as now in the static theory of time. Define tot(m,n,n') = [stot(m,n),ww(n')]. Then

Tot(tot(m,n,n')) iff m \le n \land n \le n'

Notice that if Tot([tot(m,n), ww(n') ], then

ww(n')}(now) le val{tot(m,n)}(now)

tick lifts to an operation on Tot systems

\tick(\tot(m,n,n')) = \tot(m,n,n'+1)

and leads to the \irtick inference rule on Tot systems

\tot(m,n,n') \irtick \tick(\tot(m,n,n'))

The updating operations \updateNow and \updateThen are defined on Tot systems by

\updatenow(\tot(m,n,n')) = \tot(m,n',n') \updatethen(\tot(m,n,n')) = \tot(n,n,n')

The look operation on Tot systems can be defined by

\look(\tot(m,n,n')) = \updatenow(\updatethen(\tot(m,n,n')))

The corresponding inference rule \irlook is

\tot(m,n,n') \irlook \look(\tot(m,n,n')) $$

We can query a $Tot$ system about now and then.

These queries are addressed to the static theory of time context.

\query{\qthen}(\tot(m,n,n')) = m

query{now}(tot(m,n,n')) = n

The interactions described above with wristwatch and theory-of-time systems each preserves the associated physics, and hence any composition of ticking and updating will do so, and so querying will give coherent answers. Furthermore, if we start with some theory of time, tot then any sequences of ticks and updatings applied to tot intuitively corresponds to some future $tot$.

Thoughts

In a wristwatch context, the meaning of now is what it is attached to. This can change, so when we ask the meaning of now again it may be different, but it causes no problem! The change is satisfaction preserving, although not validity preserving.

Wristwatch illustrates the power of attachments. Here we use them to provide the mechanism for sensors and effectors. If, as in theories, the simulation structure were simply some of the true wffs this would not be possible.

This suggests a different idea of what is meant by a "solution" to the problem of reasoning about time. We don't require complex explanation (in a validity preserving way) of the value of quot;nowquot; because it used to be quot;thenquot;. Rather, we supply our robot with a wristwatch and a context that contains its memory of what it discovers as it looks at its watch. The watch, as it should, can tick away, but the robot's Tot maintains a coherent (i.e., consistent) and correct theory of time.