.de fill
.fi
..
.so ms.bk
.if t .nr PD 0.5v \" Paragraph spacing, troff
.if n .nr PD 1v   \" Paragraph spacing, nroff
.de TP      \" TP - Tag paragraph
.RT
.if \\n(1T .sp \\n(PDu
.ne 1.1
.if !\\n(IP .nr IP +1
.in +\\n(I\\n(IRu
.nf
.ti -0.5i
.it 1 }M
.di ]C
..
.de }M     \" End of label
.br
.di
.ti -0.5i
.]C
.fi
.ft 1
..
.de PB   \" PB - Indent and no-fill block
.sp 1
.RS
.nf
..
.de PE   \" PE - End of no-fill block
.fi
.RE
.sp 1
..
.       \" UX - UNIX macro
.de UX
.ie \\n(UX \s-1UNIX\s0\\$1
.el \{\
\s-1UNIX\s0\\$1\(dg
.FS
\(dg \s-1UNIX\s0 is a trademark of AT&T.
.FE
.nr UX 1
.\}
..
.nr PS 12
.nr PO 1.0i
.EQ
delim %%
gfont C
.EN
.       \" Page header
.ds LF Draft Only \(em Do Not Distribute
.ds RF \(co copyright 1988 University of Minnesota
.       \" Page footer
.ds RH \\n(PN
.CB "Introduction"
.MH 1
.MH 2 "Theoretical Background"
.CB "Temporal Variables"
.MH 1
.MH 2 "Bindings of Temporal Variables: \fC$t\fP-lists"
.PP
A temporal variable is bound to a Prolog structure similar
to a list, which we shall call a $t-list.  The head of a $t-list is
the value of the corresponding variable for the current time.
Its tail may again be a $t-list; thus the $t-list contains the
values of the variable for all future times, as far as these
values are known.  As execution of a
Tokio program proceeds from one time to the next, successive elements
of the $t-list for a variable become the current value of the variable
until, perhaps, the last element of the $t-list is reached, and then
this last element is the value for the variable from that time on.
Furthermore, as execution proceeds, a $t-list may 
be extended into the future if the last part
of a $t-list is uninstantiated.
.PP
A $t-list is a structure with two arguments and with $t as its functor;
the second argument may be  uninstantiated or may itself be a 
$t-list.  For example, suppose the following is associated with the
temporal variable \fCI\fR:
.IP "" 10
\fC$t(1, $t(2, _))                  .........\fB(1)\fR
.LP 
This indicates that the current value of \fCI\fR is \fC1\fR, the value of \fCI\fR for
the next time is \fC2\fR, and the value of \fCI\fR for later times is undetermined.
This $t-list may be compared with the Prolog (and hence Tokio) list
.IP "" 10
\fC[1, 2]                           .........\fB(2.1)\fR
.LP
Now recall that the primitive list functor in Prolog is \s+8.\s-8, which
takes two arguments; the second normally is either itself
a list or the special atom \fB[ ]\fR.  Thus \fB(2.1)\fR may be represented as
.IP "" 10
\fC\ .(1, .( 2, []))                  .........\fB(2.2)\fR
.LP
This looks very much like \fB(1)\fR with $t replaced by \s+8.\s-8, except the
last part is \fC[]\fR instead of \fC_\fR.
.PP
In fact, it is quite easy in Prolog to create and to use
lists with uninstantiated last parts, that is, tails.  Thus the list
made with \s+8.\s-8 as follows
.IP "" 10
\fC\ .(1, .(2, _))                    .........\fB(3.1)\fR
.LP
is written in list notation as
.IP "" 10
\fC[1, 2 | _]                       .........\fB(3.2)\fR
.PP
Now consider the usual \fCmember\fR predicate in Prolog:
.IP "" 10
\fCmember(E, [E|_]).
.ls 1
.IP "" 10
\fCmember(E, [_|T]) :-  member(E,T).\fR
.ls 2
.LP
And consider the query 
.IP "" 10
\fC?- member(3,[1,2]).\fR
.LP
or, equivalently,
.IP "" 10
\fC?- A = [1,2], member(3,A).\fR
.LP
where the list is that shown in \fB(2.1)\fR and \fB(2.2)\fR.  This finds
\fC3 \(!= 1\fR, and so tries \fCmember(3, [2])\fR.  It then finds \fC3 \(!= 2\fR, and
tries \fCmember(3, [])\fR.  The latter fails, so all goals depending on it,
back to the original, fail.  Next consider the query
.IP "" 10
\fC?- A = [1, 2|_], member(3, A)\fR
.LP
where the list is that shown in \fB(3.1)\fR and \fB(3.2)\fR.  This finds
\fC3 \(!= 1\fR, then
\fC3 \(!= 2\fR, and then tries \fCmember(3, [_])\fR.  But then the first, 
non-recursive clause in the definition of \fCmember\fR succeeds: \fC[_]\fR is
unified with \fC[E|_]\fR, but \fCE\fR is unified with \fC3\fR; thus \fC[_]\fR is unified
with \fC[3|_]\fR.  The goals depending on this subgoal thus succeed, and we
get, at the top level, \fCA=[1,2,3 | _]\fR.  Thus this definition of \fCmember\fR, when given an instantiated
first argument and a second argument that is a list with uninstantiated
tail, succeeds whether or not the first argument appears in the list.
If the first argument is not in the list, then 
it is added to the list
as the last element before the uninstantiated tail.
.PP
We have made this digression to give the reader a feel for how Tokio
may "differentiate" $t-lists to store future values for a variable.
Now suppose variable \fCA\fR is associated with $t-list \fB(1)\fR, and \fCB\fR is 
uninstantiated.  Then
.IP "" 10
\fCA = B\fR
.LP
or
.IP "" 10
\fCB = A\fR
.LP
instantiates \fCB\fR to \fC1\fR (the order of the operands makes no difference).
That is, \fC=\fR looks at only the head (or leftmost term) of a
$t-list.  Similarly, if \fCC\fR is bound to the $t-list
.IP "" 10
\fC$t(1, $t(3, _)),\fR
.LP
then 
.IP "" 10
\fCA = C\fR
.LP
succeeds, but neither \fCA\fR nor \fCC\fR changes.  If \fCD\fR is bound to
.IP "" 10
\fC$t(2,_)\fR
.LP
then
.IP "" 10
\fCD = A\fR
.LP
fails.  These results are corollaries of the meaning of \fC=\fR
inherited from Prolog and of the fact that \fC=\fR looks
only at the head of $t-lists.
Recall that generally a Prolog predicate may have different
arguments instantiated or uninstantiated in various uses.
.PP
The Tokio function \fC@\fR (read \fInext\fR) accesses the tail of a
$t-list; thus \fC@\fR used with \fC=\fR allows one to refer to the value of a 
variable at the next time.  For example, if \fCA\fR is bound to \fB(1)\fR and if
\fCB\fR is uninstantiated, 
.IP "" 10
\fC@A = B\fR
.LP
or
.IP "" 10
\fCB = @A\fR
.LP
instantiates \fCB\fR to \fC2\fR.  If \fCC\fR is uninstantiated and \fCD\fR is bound to
.IP "" 10
\fC$t(1, $t(2, $t(3, _))),\fR
.LP
then
.IP "" 10
\fC@C = @ @D\fR
.LP
(the space between repeated \fC@\fR's is required)
binds \fCC\fR to the $t-list 
.IP "" 10
\fC$t(_, $t(3, _)).\fR
.LP
If \fCE\fR is bound to 
.IP "" 10
\fC$t(1, _)\fR
.LP
then 
.IP "" 10
\fC@E = E + 1\fR 	
.LP
differentiates \fCE\fR so that it becomes
.IP "" 10
\fC$t(1, $t(2, _)).\fR
.LP
Finally, if \fCA\fR is as defined above, then
.IP "" 10
\fC@A = A\fR
.LP
fails since \fC@\fRA is \fC2\fR, and \fCA\fR is \fC1\fR, so there is no way \fC@A\fR and \fCA\fR 
can be made equal.
.PP
To give illuminating examples, we introduce the \fIalways\fR
operator, \fC#\fR. If \fCP\fR is some goal, then \fC#P\fR is executed at each time,
from the first to the last, of the interval in which it occurs.
\fCwrite(A)\fR is just as it is in Prolog, except that, instead of writing
what \fCA\fR is bound to, which may be a $t-list, it writes only the
current value of \fCA\fR. Suppose our Tokio program is simply,
.IP "" 10
\fCtest(A) :- @A = A+1, #write(A).\fR
.LP
Suppose that after, this program is compiled, we issue the following
query:
.IP "" 10
\fC?- tokio I = 1, test(I).\fR
.LP
The output will then read:
.IP "" 10
\fCt0: 1
.ls 1
.IP "" 10
\fCt1: 2
.IP "" 10
\fCI = $t(1, $t(2, _9)
.IP "" 10
\fCyes\fR
.ls 2
.LP
where \fC_9\fR is the internal name for some unbound variable. That is,
the current (at %t sub 0 %) value of \fCA\fR is \fC1\fR, and the value of \fCA\fR at the next
time (%t sub 1 %) is \fC1\fR, and nothing is determined for any time after that, 
so Tokio draws the interval to a close.
.MH 2 "One-Time Unification vs. Unification Over All Time"
.PP
The unification we have considered so far, by means of \fC=\fR,
is a "one-time unification". The unification called "unification 
over all time" is achieved by unification with the head of a clause.
For example, let us suppose \fCA\fR is bound to \fB(1)\fR, and that \fCfoo\fR is defined 
by   
.IP "" 10
\fCfoo(X) :- write(X), Y = @X, tab(3), write(Y).\fR
.LP
Then evaluating
.IP "" 10
\fCtokio foo(A).\fR
.LP
binds \fCX\fR to \fC$t(1, $t(2, _))\fR and produces the following output
.IP "" 10
\fCt0: 1    3
.ls 1
.IP "" 10
\fCt1:
.IP "" 10
\fCA = $t(1, $t(2,_9))
.IP "" 10
\fCyes\fR
.ls 2
.PP
As another example, suppose our program is
.IP "" 10
\fCtest(A) :- @A = A+1, #disp(A).
.ls 1
.IP "" 10
\fCdisp(X) :- write('=>'), write(X).\fR
.ls 2
.LP
If we use the query
.IP "" 10
\fC?- tokio I = 1, test(I).\fR
.LP
we get
.IP "" 10
\fCt0: =>1
.ls 1
.IP "" 10
\fCt1: =>2
.IP "" 10
\fCI=$t(1, $t(2, _1))
.IP "" 10
\fCyes\fR
.ls 2
.LP
Note that \fCX\fR in \fCdisp\fR must get bound to the same $t-list as \fCA\fR 
in \fCtest\fR for all information required to be available to \fCdisp\fR.
.PP
Thus far, we have considered $t-lists whose last elements are uninstantiated
variables, \fC_\fR. We now consider cases where the last element is
bound to a value. Subsequent examples will make use of the \fClength\fR operator.
.PP
Recall that Tokio will discontinue the current interval as soon
as everything in that interval is satisfied. One explicit way 
to extend or to bound an interval is by using the temporal
predicate \fClength\fR. The goal \fClength(n)\fR, where \fCn\fR is a positive
integer, forces the current interval to be of length \fCn\fR, i.e.,
to extend from some time 
%t sub i% to some time %t sub i+n % .
For example,   
.IP "" 10
\fCtest :- length(1), A = 1, @A = 2, @ @A = 3, #write(A).\fR
.LP
output only \fC1\fR and \fC2\fR.
.IP "" 10
\fCtest :- length(3), A = 1, @A = 2, @ @A = 3, #write(A).\fR
.LP
will output \fC1\fR, \fC2\fR, and \fC3\fR, for times %t sub 0 %,  % t sub 1 %, and  %t sub 2 % respectively,
and then will indicate an uninstantiated variable for %t sub 3 %.
.PP
We begin with the degenerate case, where a temporal variable, say \fCA\fR,
is bound to a \fIsimple\fR value, that is, a value other than a $t-list.
(A \fIsimple\fR value in this sense could be a list or structure of any degree
of complexity.) Then the value of \fCA\fR for the present and all future
times
is the \fIsimple\fR value to which it is bound. For example, given
the program
.IP "" 10
\fCp(a).
.ls 1
.IP "" 10
\fCt(A) :- length(3), p(A), #write(A).\fR
.ls 2
.LP
evaluation of \fCt(X)\fR will produce
.IP "" 10
\fCt0: a
.ls 1
.IP "" 10
\fCt1: a
.IP "" 10
\fCt2: a
.IP "" 10
\fCt3: a
.IP "" 10
\fCX = a\fR
.ls 2
.PP
The next greater degree of complexity arises when a temporal
variable \fCA\fR is bound to a two-element $t-list, where both elements
are instantiated. Then the first element is the value of A for the
current time, and the second element is the value of \fCA\fR for all
future time. For example, suppose we have the program
.IP "" 10
\fCq(b).
.ls 1
.IP "" 10
\fCrz(X) :- X=a, @q(X).
.IP "" 10
\fCt(A) :- length(3), rz(A), #write(A).\fR
.ls 2
.LP
then evaluating \fCt(Y)\fR produces:
.IP "" 10
\fCt0: a
.ls 1
.IP "" 10
\fCt1: b
.IP "" 10
\fCt2: b
.IP "" 10
\fCt3: b
.IP "" 10
\fCY = $t(a, b)
.IP "" 10
\fCyes\fR
.ls 2
.LP
Here the variable \fCY\fR in the initial goal shares with
\fCA\fR in the third clause; the unification is unification over
all time. Again, \fCA\fR in the third clause shares with \fCX\fR in
the second clause because of the goal \fCrz(A)\fR in the third clause;
again the unification involved a unification over all time. In the
second clause, the \fCX=a\fR goal causes the current value at \fCX\fR
(and thus for \fCA\fR and of \fCY\fR) to be \fCa\fR; and the \fC@q(X)\fR
goal causes the value for \fCX\fR (and thus for \fCA\fR and for \fCY\fR)
at the next time to be \fCb\fR. Since \fCq(b)\fR is interpreted as
asserting that \fCq(b)\fR is always true, it is reasonable that
\fC@q(X)\fR should cause X (and thus \fCA\fR and \fCY\fR) to have the value
\fCb\fR for all future time. This is indeed the case \fCX\fR (and \fCA\fR
and \fCY\fR) is bound to \fC$t(a, b)\fR. The \fCa\fR is for the current
time. At the next time point, the value for \fCX\fR is \fCb\fR, and, from
the context of \fIthis\fR time point, it is as if we start with
\fCX\fR bound to the simple value \fCb\fR. Thus this case reduces to the
previous case, but at the next point in time.
.PP
More generally, a $t-list is one of two forms:
.IP "" 10
.ls 1
.RS
.ls 1
.IP "\fB1)" 4
\fC$t(%S sub 0%\fC, $t(%S sub 1%\fC, ... $t(%S sub n%\fC, _) ...))
.IP "\fB2)" 4
\fC$t(%S sub 0%\fC, $t(%S sub 1%\fC, ... $t(%S sub n%\fC, v) ,,,))\fR
.RE
.ls 2
.LP
Here %S sub i%, \fC0 \(<= i \(<= n\fR, is either a variable or
a simple (i.e., non-$t-list) value, and \fCv\fR is a simple value.
Suppose variable \fCX\fR is bound to \fB1)\fR and the current time
is %t sub 0%. Then, because the last member of the $t-list
is \fC_\fR, the value of \fCX\fR is undetermined after %t sub n%; that
is, \fCX\fR is undifferentiated for %t sub i%, \fCi > n\fR. Next suppose
\fCX\fR is bound to \fB2)\fR and the current time again is %t sub 0%. Then,
because the last member of the $t-list is \fCv\fR, a value, the value
of \fCX\fR is \fCv\fR for all %t sub i%, \fCi \(>= n\fR.
.PP
Note that any of the %S sub i%, \fCi \(<= n \fR, in \fB1)\fR or \fB2)\fR
may be an unbound variable. For example, given the program
.IP "" 10
\fCq(b).
.ls 1
\fCrz(X) :- @@X = a, @@@q(X).
.IP "" 10
\fCt(A) :- length(4), rz(A), #write(A).\fR
.ls 2
.LP
evaluation of \fCt(Y)\fR produces:
.IP "" 10
\fCt0: _
.ls 1
.IP "" 10
\fCt1: _
.IP "" 10
\fCt2: a
.IP "" 10
\fCt3: b
.IP "" 10
\fCt4: b
.IP "" 10
\fCY = $t(_, $t(_, $t(a, b)))
.IP "" 10
\fCyes\fR
.ls 2
.PP
Sometimes Tokio must fill in gaps in a $t-list. For example, given
.IP "" 10
\fCp(a).
.ls 1
.IP "" 10
\fCq(b).
.IP "" 10
\fCr(X) :- length(3), p(X), @@q(X).\fR
.ls 2
.LP
evaluating \fCr(Y)\fR produces
.IP "" 10
\fCt0: a
.ls 1
.IP "" 10
\fCt1: a
.IP "" 10
\fCt2: b
.IP "" 10
\fCt3: b
.IP "" 10
.IP "" 10
\fCY = $t(a, $t(a, b))
.IP "" 10
\fCyes\fR
.ls 2
.LP
The second \fCa\fR in the $t-list to which \fCY\fR is bound is the
direct result of no unification, but it must be present to record the
fact the value of \fCY\fR (which shares with \fCX\fR of the third
clause) is \fCa\fR at \fCt1\fR.
.PP
Finally, an attempt to output (using \fCwrite\fR) and undifferentiated
element results in that element being differentiated. For example,
given
.IP "" 10
\fCp(a).
.ls 1
.IP "" 10
\fCq(X) :- X = b.
.IP "" 10
\fCrq(A) :- length(3), p(A), @q(A).\fR
.ls 2
.LP
evaluating \fCrq(Y)\fR produces
.IP "" 10
\fCY = $t(a, $(b, _))\fR
.LP
Here the undifferentiated \fC_\fR indicates that \fCY\fR has no value
for %t sub i%, \fCi > 1\fR. On the other hand, if \fC#write(A)\fR is
added to the \fCrq\fR clause giving
.IP "" 10
\fCrq(A) :- length(3), p(A), @q(A), #write(A).\fR
.LP
the result of evaluating \fCrq(Y)\fR is
.IP "" 10
\fCt0: a
.ls 1
.IP "" 10
\fCt1: b
.IP "" 10
\fCt2: _
.IP "" 10
\fCt3: _
.IP "" 10
\fCY = $t(a, $t(b, $t(_, $t(_,_))))\fR
.ls 2
.LP
Here the final, undifferentiated \fC_\fR indicates that \fCY\fR has no
value for %t sub i%, \fCi > 3\fR; the unbound elements for %t sub 2%
and %t sub 3% occur explicitly because \fCwrite\fR was evaluated at
%t sub 2% and %t sub 3%.
.MH 2 "Summary"
.KS 
.EQ
delim %%
gfont C
.EN
.IP "" 10
.ls 1
.TS
tab (/) box;
c || cw(1.5i) || cw(1.5i)
c || cw(1.5i) || lw(1.5i).
Value of a Prolog variable/T{
\fRValue of a Tokio variable
T}/T{
Comment
T}
=
\fCa/T{
\fCa
T}/T{
Value \fCa\fR holds at all %t sub i%, \fCi \(>= 0\fR.
T}
_
\fC[a,b|_]/T{
\fC$t(a, $t(b,_))\fR
T}/T{
Value \fCa\fR holds at %t sub 0%, value \fCb\fR holds at %t sub 1%, and there is no value for %t sub i%, \fCi > 1\fR.
T}
_
\fC[a,b|c]\fR i.e., \fC.(a, .(b,c))\fR/T{
\fC$t(a, $t(b,c))\fR
T}/T{
Value \fCa\fR holds at %t sub 0%, value \fCb\fR holds at %t sub i%, and value \fCc\fR holds at all %t sub i%, \fCi > 1\fR.
T}
_
\fC[a,b]\fR, i.e., \fC\.(a, \.(b, []))\fR/T{
\fRNothing
T}/T{
\fRThere is no analog of \fC[]\fR.
T}
.TE
.EQ
delim %%
gfont C
.EN
.sp
.ce
\fRTable 2.1: Analogy between Prolog (and Tokio) lists and Tokio $t-lists.
.ce 0
.KE
.CB "Temporal Predicates and Operators"
.MH 1
.MH 2 "Some Useful Temporal Predicates and Operators"
.MH 3 "Always (\fC#\fP) and Sometimes (\fC<>\fP)"
We have already seen the \fCalways\fR operator, \fC#\fR. Recall that
\fC#P\fR, where \fCP\fR is some Tokio predicate, requires \fCP\fR to succeed at each
time in the current interval. In declarative terms, \fC#P\fR states that
\fCP\fR is (in the current interval) always \fCtrue\fR. The dual of \fC#P\fR is \fC<>P\fR,
read \fIsometimes\fR \fCP\fR. \fC<>P\fR is \fCtrue\fR if \fCP\fR is \fCtrue\fR sometime in the future,
i.e., at some %t sub i%, \fCi > 0\fR, in the current interval. In procedural terms, \fC<>P\fR requires \fCP\fR
to be a goal at each time in the interval but the first until \fCP\fR
succeeds. Note that success of \fCP\fR (i.e., success of \fCP\fR at the current
time) does not count to success of \fC<>P\fR. In declarative terms, \fCP\fR
does not imply \fC<>P\fR. However, for \fC#P\fR to succeed, \fCP\fR must succeed at each
time in the current interval, so \fC#P\fR implies \fCP\fR. Thus \fC#P\fR and \fC<>P\fR are
not quite the duals they are claimed to be. 
Note that, if there is no way \fCP\fR can succeed, then \fC<>P\fR will cause
the interval in which it occurs to be extended indefinitely unless that
interval is closed.
Thus it is good practice to use the combination
.IP "" 10
\fClength(n), <>P,\fR
.LP
where \fCn\fR is some positive integer, rather than simply \fC<>P\fR.
Generally, \fC<>P\fR is used when we wish to extend the current 
interval far enough into the future for \fCP\fR to succeed at sometime
in the interval, but when we also do not know in advance how far 
into the future that might be. Thus one use of \fC<>\fR could be in
defining the predicate
.IP "" 10
\fCsometimes_equal(A,B) :- <>A = B.\fR
.LP
This will succeed if \fCA\fR and \fCB\fR have the same value for some time
in the current interval. Note that it will not succeed if \fCA\fR
and \fCB\fR have the same value only at a time outside the 
current interval.
.MH 3 "Next: \fC@\fP (function) and \fC@\fP (operator)"
We have already seen the \fInext\fR function, \fC@\fR. Recall that \fC@I\fR
accesses the tail of the $t-list to which \fCI\fR is bound; in
particular, if \fCJ\fR is uninstantiated, then
.IP "" 10
\fCJ = @I\fR
.LP
instantiates \fCJ\fR at the current time to the value for \fCI\fR at the 
next time. Now, there is also a \fCnext\fR temporal operator,
also symbolized by \fC@\fR. The goal \fC@P\fR succeeds if the goal \fCP\fR
succeeds at the next time. It is important to distinguish
the function \fC@\fR from the operator \fC@\fR, even though certain
analogies between the two warrant emphasis. As an example,
.IP "" 10
\fCtest :- I = 1, @(I = 2).\fR
.LP
is the same as
.IP "" 10
\fCtest :- I = 1, @I = 2.\fR
.LP
Note that
.IP "" 10
\fCtest :- length(2), I = 1, @I = 2, @ @I = 3, @ #write(I).\fR
.LP
will output \fC2\fR and \fC3\fR as the values for \fCI\fR at %t sub 1 % and % t sub 2 %, but
will not output the value for \fCI\fR at % t sub 0 %.  Also note that
.IP "" 10
\fC@ @I = 3\fR
.LP
is the same as
.IP "" 10
\fC(@ @I) =  3\fR
.PP
We have considered the \fC@\fR operator as delaying evaluation
of a goal to the next time point. Equivalently, we could
view the \fC@\fR operator as creating a subinterval of the current
interval, where the subinterval begins at the next time.
The two views are equivalent because all goals in an interval
are executed at the beginning of the interval.
.PP
Note that a necessary condition for the goal \fC@P\fR to succeed
in the current interval is that the length of this interval
be at least one, i.e., there must be a time point after the
current time \(em a next time \(em at which \fCP\fR can succeed. 
Similarly, a necessary condition for \fC@ @P\fR to succeed is that
the length of the interval be at least two (from %t sub i%
to %t sub i+2%), and, in general, a necessary condition for
.IP "" 10
\fC@ @...@ P    (\fIn \fC@\fR's)
.LP
to succeed is that the length of the interval be at least \fIn\fR.
.MH 3 "Weak Next: \fCnext\fP"
The operator \fCnext\fR (\fIweak next\fR) is similar to \fC@\fR except that
\fCnext P\fR may succeed even when there is no next time in the current
interval, i.e., it is \fInot\fR a necessary condition for the success of
\fCnext P\fR that the length of the interval be at least one. If the goal
\fCnext P\fR is evaluated and there is no next time in the interval, then
\fCnext P\fR succeeds no matter what \fCP\fR may be. Now, an interval consisting
of only one point (the current time) has length zero. A suffix subinterval of
an interval is any subinterval containing that interval's last
point.  As a Tokio execution  in an interval proceeds,
successively smaller suffix subintervals of the original interval
become the new current interval. When the last point in the original interval
is reached, the current subinterval has  length zero. Thus
we may say that, when \fC@P\fR is evaluated at the last point in an 
interval, it must fail, and, when \fCnext P\fR is evaluated at the last point
in an interval, it must succeed; all of this independent is
of what \fCP\fR may be.
.MH 3 "Interval Termination: \fCempty\fP and \fCnotEmpty\fP"
To clarify the semantics of \fCnext\fR and other operators,
we discuss a zero-argument predicate \fCempty\fR that succeeds when
evaluated at the last point in an interval (or equivalently,
that succeeds when evaluated in an interval of length zero).
Then, in declarative terms, \fCnext P\fR is \fCtrue\fR if and only if
\fCempty\fR \fBv\fR \fC@P\fR is \fCtrue\fR (where \fBv\fR means \fIor\fR). Also, \fClength(n)\fR is \fCtrue\fR  if and only if
.IP "" 10
\fC@ @...@ empty    (\fIn \fC@\fR's)
.LP
is \fCtrue\fR.  Thus we may always replace \fClength(n)\fR with \fCempty\fR preceded by \fIn\fR \fC@\fRs.
Now let \fCnotEmpty\fR be \fCtrue\fR when and only when the current time
is not the last time point in the current interval.
Then \fC@P\fR is \fCtrue\fR implies \fCnotEmpty\fR is \fCtrue\fR.
.PP
Further discussion of \fCempty\fR and \fCnotEmpty\fR requires some
understanding of how intervals are maintained by Tokio. If neither
\fCempty\fR nor any predicate definable in terms of \fCempty\fR,
such as \fClength\fR, has been evaluated, then the current interval lacks
a fixed endpoint; in such a case, we say the current interval is \fIopen-ended\fR.
Evaluation of a goal of the form \fC@P\fR in an open-ended interval requires
execution to advance at least as far as the next time, and, in general,
evaluation in an open-ended interval of \fCP\fR preceded by \fIn\fR \fC@\fR's
requires execution to advance at least \fIn+1\fR time points into the future.
When all goals resulting from the use of \fC@\fR have been evaluated, there
is no need to extend the current open-ended interval, so Tokio terminates the
interval. (Tokio, however, ensures that the top-level interval has length
at least one.)
.PP
A \fIclosed\fR interval is an interval with a fixed endpoint, and so with a
fixed length. An interval is closed because \fCempty\fR or some predicate
(such as \fClength\fR) definable in terms of \fCempty\fR has been evaluated.
In a closed interval of length \fIn\fR, a goal of the form \fCP\fR preceded
by \fIn+1\fR \fC@\fR's fails because, at the last point in the interval,
and attempt is made to evaluate \fC@P\fR \(em but there is no next time in which
\fCP\fR may succeed.
.PP
Now, there are two cases in which the goal \fCempty\fR succeeds:
.IP "\fB1)\fR" 5
if the current interval is open-ended, or
.ls 1
.IP "\fB2)\fR" 5
if the current interval is closed and the current time is the last time
in the current interval.
.ls 2
.LP
There is one case in which the goal \fCempty\fR fails:
.IP "\fB3)\fR" 3
if the current interval is closed and the current time is not the last
time in the current interval, i.e., there are times in the current interval
after the current time.
.LP
In case \fB1)\fR, evaluation of \fCempty\fR causes the current, open-ended
interval to be closed, with the current time as its last time; evaluation of
\fC@empty\fR causes the next time to be the last time; and, in general, evaluation
of \fCempty\fR preceded by \fIn\fR \fC@\fR's causes the time \fIn\fR units
after the present to be the last time of the current interval.
.PP
In an opposite manner, the goal \fCnotEmpty\fR succeeds in cases \fB1)\fR and
\fB2)\fR, and fails in case \fB2)\fR. Note that either \fCempty\fR or
\fCnotEmpty\fR will succeed in case \fB1)\fR \(em but with different effects.
Evaluation of \fCnotEmpty\fR in case \fB1)\fR causes the current, open-ended
interval to extend at least to the next time (while remaining open-ended;
evaluation of \fC@notEmpty\fR causes the current interval to extend at least
two time points into the future; and, in general, evaluation of \fCnotEmpty\fR
preceded by \fIn\fR \fC@\fRs causes the current interval to extend at least
\fIn+1\fR time points into the future.
.PP
The meaning of \fCempty\fR and \fCnotEmpty\fR may be explained in terms
of the interval variables maintained internally by Tokio. Suppose \fCI\fR is
the interval variable for the current interval. Then \fCI\fR may be thought
of as bound to the last time in the current interval if this interval is closed;
if the current interval is open-ended, then \fCI\fR is unbound. For example,
if the current time is %t sub i% and the end of the current interval is two
time points hence, then we imagine \fCI\fR bound to %t sub i+2 %. We may now
reformulate the conditions under which the goals \fCempty\fR and \fCnotEmpty\fR
succeed or fail. Let \fCI\fR be the interval variable for the current interval
and let %t sun i% be the current time. Then \fCempty\fR succeeds if
.IP "\fB1')\fR" 6
\fCI\fR is unbound, or
.ls 1
.IP "\fB2')\fR" 6
%I ~=~ t sub i %,
.ls 2
.LP
and fails if
.IP "\fB3')\fR" 6
%I ~>~ t sub i%;
.LP
and \fCnotEmpty\fR succeeds in cases \fB1')\fR and \fB3')\fR and fails in
case \fB1')\fR. Note that the goal \fCnotEmpty\fR is not the same as the
goal \fCnot(empty)\fR since the latter fails in case \fB1')\fR. In case \fB1')\fR,
evaluation of \fCempty\fR binds \fCI\fR to %t sub i% and evaluation of
\fCnotEmpty\fR places the requirement in \fCI\fR that, if it becomes bound,
it must be bound to some %t sub j ~>~ t sub i%. Evaluating \fC@empty\fR at
the current time %t sub i% causes \fCempty\fR to be evaluated at % t sub i+1%,
thus (still assuming case \fB1')\fR) binding \fCI\fR to %t sub i+1%. Similarly,
evaluating \fC@notEmpty\fR at %t sub i% will force \fCI\fR to be unbound at
%t sub i+1 %.
.PP
Notice that the goal \fC@true\fR has the same effect as the goal
\fCnotEmpty\fR. This is because evaluating \fC@true\fR causes \fCtrue\fR
to be evaluated at the next time point. If \fCI\fR is unbound, then evaluating \fC@true\fR results in execution reaching at least the next point in time,
where \fCtrue\fR is evaluated; but evaluating \fCtrue\fR imposes no further
requirements. If %I ~>~ t sub i%, then \fC@true\fR succeeds, again with no
further conditions. Finally, if %I ~=~ t sub i%, \fC@true\fR fails since
there is no next time at which \fCtrue\fR could be evaluated. It follows
that the goal consisting of \fCnotEmpty\fR preceded by \fIn\fR \fC@\fR's has
the same effect on the goal consisting of \fCtrue\fR preceded by \fIn-1\fR \fC@\fR's.
It should be evident that in, for example, the complete goal
.IP "" 10
\fCnotEmpty, @notEmpty, @@Empty,\fR
.LP
the goals \fCnotEmpty\fR and \fC@notEmpty\fR are superfluous, and the
composite goal
.IP "" 10
\fC@....@empty, @....@empty,\fR
.LP
where the number of \fC@\fR's in the two subgoals are different, always
fails.
.MH 2 "Reduction Along the Current- and Future-Time Axes"
.PP
The concept of a suffix subinterval and the \fCnext\fR operator
together allow us to characterize the execution of a Tokio
program as it advances from one time point to the next.
The term "reduction"
is used in logic programming to describe the replacement of
goals by subgoals in an attempt to satisfy a query. In Tokio,
reduction is done in two directions: along the current-time axis
and along the future-time axis. Reduction along the current-time axis
is identical to reduction in Prolog. Reduction along the future-time
axis occurs when a new subinterval is generated, for example,
when a goal of the form \fC@P\fR is evaluated. At any time point,
reduction along the future-time axis is done after reduction 
along the current-time axis is complete. Thus Tokio must keep
a list of goals to be evaluated
at the next time point; this list is called the 'next queue'.
.PP
In general, reduction of a Tokio goal will produce
subgoals to evaluate at the current time and subgoals to evaluate
at the next time. The latter are put into the next queue, and 
the former are evaluated as part of the reduction along the current-time
axis; thus all the former are evaluated before any of the
latter. For example, when \fC@P\fR is evaluated, the current-time subgoal
\fCnotEmpty\fR and the future-time subgoal \fCP\fR are generated. If the current-time 
is the last time in an interval, then \fCnotEmpty\fR is \fCfalse\fR, and so
\fC@P\fR fails, and thus backtracking along the current-time axis is initiated;
this backtracking is identical to the backtracking in Prolog.
If there is a next time, then \fCnotEmpty\fR succeeds and, assuming the rest
of the reduction along the current-time axis succeeds, evaluation proceeds
to the next time point, where \fCP\fR and other goals previously put on the
next queue are evaluated. If \fCP\fR and these other goals succeed with
respect to reduction along the current-time axis at the next time, then,
in general, a new next queue will have been built, and the goals in this 
will be evaluated in the following time (two time points after the original
time point considered). If \fCP\fR contains no temporal operators, then there
are no goals descended from \fC@P\fR when reduction along the current-time
axis occurs two time points after the original time. (This is not to say,
however, that there are no effects of \fC@P\fR at that point. Indeed, the effects of
\fC@P\fR may propagate indefinitely in the future because of variable bindings caused by the evaluation of \fCP\fR.) 
.PP
If, on the other hand, reduction along the current-time axis fails
at the time after the original time, then backtracking along the 
future-time axis is initiated. This type of backtracking is not derived from
Prolog, and will be discussed further below. Two major points should 
emerge from this discussion of reduction in Tokio. The first is that
reduction as a whole is driven by reduction along the
future-time axis, not reduction along the current-time axis. The
second major point is that each step along the future-time axis
may be viewed as evaluating the goal formed by applying the \fCnext\fR operator
to the conjunction of the subgoals in the next queue. This is because 
any commitment to the existence of a next time is covered by 
generating the current-time subgoal \fCnotEmpty\fR.
.PP
The current-time and future-time subgoals generated in
evaluating a goal containing a temporal operator are similar to the
head and tail of a $t-list bound to a temporal variable. The heads 
of the $t-lists of the program variables provide the environment
for the evaluation of the current-time subgoals and the
tails of the $t-lists of the program variables provide the
environment for the evaluation of future time-goals.
.MH 3 "\fC#\fP and \fC<>\fP Revisited"
This discussion may be applied to the evaluation of
subgoals of the form \fC#P\fR and \fC<>P\fR. Thus \fC#P\fR succeeds if \fCP\fR
succeeds and \fCnext\fR \fC#P\fR succeeds. And \fC<>P\fR succeeds if \fC@P\fR
succeeds or \fCnext\fR \fC<>P\fR succeeds. Thus \fC<>P\fR posts two subgoals,
\fCP\fR and \fC<>P\fR, into the future, only one of which need succeed
at the next time. Also, \fC<>P\fR can extend an open-ended
interval in search of a time when \fCP\fR succeeds; this is because
it evaluates the goal \fC@P\fR before the goal \fCnext\fR \fC<>P\fR, and \fC@P\fR 
evaluated at the last point in an open-ended interval extends
the interval by one point. 
In contrast, \fC#P\fR evaluates one subgoal, \fCP\fR, at the
current time, and posts another subgoal, \fC#P\fR, into the future
if there is a future.  If there is a future, both subgoals must
succeed; obviously, the second subgoal ensures that \fCP\fR is evaluated
at all points of the current interval.  If there is no future,
then only the \fCP\fR subgoal at the current time need succeed for the
\fC#P\fR to succeed; this is because the second subgoal from the point of
view of the current time is \fCnext\fR \fC#P\fR, and \fCnext Q\fR, where \fCQ\fR is any goal,
always succeeds when there is no future.  Thus \fC#P\fR cannot extend
an open-ended interval.
.MH 3 "Interval Length: \fClength\fP and \fCskip\fP "
Next, \fClength(n)\fR is equivalent to
.IP "" 10
\fC@ @...@ empty    (\fIn \fC@\fR's)
.LP
This succeeds if 
.IP "" 10
\fC@...@ empty    (\fIn-1 \fC@\fR's)
.LP
succeeds at the next time. There is no subgoal for the current time,
or, rather, the subgoal for the current time is simply \fCtrue\fR. 
Obviously, 
.IP "" 10
\fC@ @...@ empty    (\fIn \fC@\fR's)
.LP
extends an open-ended interval to have a length of \fIn\fR and (because
of the \fCempty\fR) makes it closed; it also fails in a closed interval
of length other than \fIn\fR, but succeeds (but without effect)
in a closed interval of length \fIn\fR.  A goal 
.IP "" 10
\fClength(1)\fR
.LP
is equivalent to the zero-argument goal
.IP "" 10
\fCskip\fR.
.MH 2 "Interval Diagrams: Graphical Representation of Goals and Variable Values"
.PP
We now present a unified graphical representation of the evaluation
of Tokio goals and the values of temporal variables.  We draw a
discrete time-line with the points labeled % t sub 0 %, % t sub 1 %, ...:
.LP
.KS
.sp
.PS < fig1
.sp
.KE
.LP
Beneath this line, we include a line for each temporal variable on which
we write its value for each time.  Thus, if the $t-lists for \fCI\fR and \fCJ\fR are
.IP "" 10
\fC$t(1, $t(2, $t(3, _)))\fR
.LP
and
.IP "" 10
\fC$t(4, $t(_, $t(3, $t(2, $t(1, _)))))\fR
.LP
respectively, we draw
.LP
.KS
.sp
.PS < fig2
.sp
.KE
.LP
We indicate an open-ended interval if length \fCn\fR as follows:
.LP
.KS
.sp
.PS < fig3
.sp
.KE
.LP
A closed interval of length \fCn\fR is indicated by
.LP
.KS
.sp
.PS < fig4
.sp
.KE
.LP
Subintervals are shown below the intervals containing them.  Thus, if
the original goals include \fC@P\fR and \fClength(3)\fR, then:
.LP
.KS
.sp
.PS < fig5
.sp
.KE
.LP
The goals to evaluate at time % t sub i % are shown directly below the
% t sub i % label.  An arrow from these goals points down to their
current-time subgoals, and another arrow points to the right, to their future-time subgoals,
which are the goals shown directly below % t sub i+1 %.  Thus we have the
following, where we assume the original interval is closed and of length \fC3\fR:
.LP
.KS
.sp
.PS < fig6
.sp
.KE
.LP
.KS
.sp
.PS < fig7
.sp
.KE
.LP
.KS
.sp
.PS < fig8
.sp
.KE
.LP
Note that no current-time subgoal is shown at % t sub 0 % in the case of
\fC@P\fR.  We could have put \fCtrue\fR as such a goal, but we shall keep
things simple.  Likewise, no current-time subgoal is shown at % t sub 0 %
for \fC<>P\fR.  We could show \fC@P\fR as a current-time subgoal at % t sub 0 %, but
this is the same as having \fCP\fR as a goal at % t sub 1 %.  We have shown the
future-time subgoals of \fC<>P\fR separated by the Prolog \fIor\fR operator \fC;\fR
.IP "" 10
\fCP;
.ls 1
.IP "" 10
\fC<>P\fR
.ls 2
.LP 
to indicate that an attempt is made to satisfy \fCP\fR and only if this attempt
fails is an attempt made to satisfy the subgoal \fC<>P\fR.  Also, at % t sub i %,
\fCi > 0\fR, in the \fC<>P\fR case, \fCP\fR is included both in the goals at % t sub i %
and in the current-time subgoals at % t sub i %.
In general, a goal at % t sub i % that includes no temporal operators will
also appear as a current-time subgoal at % t sub i %.  Finally, we have
assumed that \fC<>P\fR, as of % t sub 3 %, has not yet succeeded 
since we have shown \fC<>P\fR
at % t sub i %, \fC0 \(<= i \(<= 3\fR.  If, for example, \fCP\fR succeeds at 
% t sub 2 %, then \fC<>P\fR succeeds, and we get the diagram
.LP
.KS
.sp
.PS < fig9
.sp
.KE
.LP
Similarly, we have assumed that \fC#P\fR has not yet failed as of %t sub 3%
since we have shown \fC#P\fR
as a goal at % t sub i %, \fC0 \(<= i \(<= 3\fR.  If \fCP\fR fails at % t sub 2 %, then
\fC#P\fR fails, and we get the diagram
.LP
.KS
.sp
.PS < fig10
.sp
.KE
.LP
We shall henceforth indicate whether evaluation of a query succeeds or
fails by writing "succeed" or "fail" to the right of its diagram.  We shall
also indicate for certain critical current-time subgoals whether they succeed
or fail by writing  "<succeed>" or "<fail>" next to them.
.PP
We may combine the representation of the values of temporal variables
and the representation of current-time and future-time subgoals in a
diagram.  For example, suppose we have
.IP  "" 10
\fCtest :- I = 2, J = 1, # @I = I+1, # @J = J+1, <> I = J.\fR
.LP
We represent the evaluation of this with the following diagram:
.LP
.KS
.sp
.PS < fig11
.sp
.KE
.LP
We have used arrows from current-time subgoals to variable values when the 
subgoals affect values at times later than the present current-time.  The
current interval in this example terminates at %t sub 2%, when all the original 
subgoals have succeeded; we indicate this with a dashed line at % t sub 2 % closing the
interval.  Note that neither of the current-time subgoals \fC@I = I+1\fR and
\fC@J = J+2\fR at % t sub 2 % were evaluated; this is because, as soon
as \fCI=J\fR was found to be true at % t sub 2 %, all original goals were
known to be satisfied, and so evalustion could terminate.
.MH 2 "More on Interval Lengths and Interval Diagrams"
.MH 3 "And: \fC,\fP (parallel), \fC&&\fP (sequential -- \fIchop\fP), and \fC&\fP (neutral)"
The \fCand\fR of Prolog, that is \fB,\fR, is used in Tokio to indicate
parallel conjunction of subgoals.  Thus, for example, if \fCP\fR is defined by the
clause
.IP "" 10
\fCP :- Q, R.\fR
.LP
then evaluating \fCP\fR involves evaluating \fCQ\fR and \fCR\fR in parallel.  Tokio also
has a sequential \fCand\fR, \fC&&\fR, read \fIchop\fR.  Suppose, for
example, P is defined by the clause
.IP "" 10
\fCP :- Q && R.\fR
.LP
Then the interval in which \fCQ\fR can be satisfied and the interval in which
\fCR\fR can be satisfied are both subintervals of the interval in which \fCP\fR can
be satisfied:
.LP
.KS
.sp
.PS < fig12
.sp
.KE
.PP
Note that the last time point in the interval for \fCQ\fR is the
first time point in the interval for \fCR\fR.  Also note that \fC&&\fR
has lower precedence than the parallel \fCand\fR (\fB,\fR).  Thus,
the following will always fail:
.IP "" 10
\fCA = 1, @A = A + 1 && A = 3.\fR
.LP
We may represent this as
.LP
.KS
.sp
.PS < fig13
.sp
.KE
.LP
The two sequential subgoals here are
.IP "" 10
\fCA = 1, @A = A + 1\fR
.LP
followed by
.IP "" 10
\fCA = 3\fR
.LP
Notice that the interval for subgoal \fCA=3\fR has length zero.  In general,
the only intervals that cannot have length zero are the top-level
interval and the first of two
subintervals resulting from a \fCchop\fR.  This example
fails because the first sequential subgoal requires \fCA\fR to be \fC2\fR at % t sub 1 %,
while the second sequential subgoal requires \fCA\fR to be \fC3\fR at % t sub 1 %.  Also
note that, ignoring the effects of backtracking and assuming no \fC@\fR
operation (as opposed to function) occur, the first of two subintervals
resulting from a \fCchop\fR has length zero.
.PP
The above example should be compared with the following, which succeeds:
.IP "" 10
\fCA = 1, @A = A + 1 && length(1) && A = 3\fR
.LP
.KS
.sp
.PS < fig14
.sp
.KE
.LP
Since \fC&&\fR is associative, we consider the subintervals generated by
multiple occurrences of \fC&&\fR as immediate subintervals of a single
parent interval; in this case, the parent interval is divided into three
subintervals, the first two of length one, and the third of length zero.
This example succeeds because the second subinterval adds a time point
after the point (at the end of the first subinterval) when \fCA\fR is \fC2\fR; this
added point is then the time when \fCA = 3\fR.  The Tokio predicate \fCskip\fR
is identical with \fClength(1)\fR, so the above could be rewritten as
.IP "" 10
\fCA = 1, @A = A + 1 && skip && A = 3\fR
.PP
Instantiations of temporal variables are not carried over from
one subinterval to the next (except at the common time point terminating
the one and initiating the next).  Consider, for example,
.IP "" 10
\fCA = 1, @A = A + 1, @ @A = A + 2 && skip && A = 4, @A = A+1\fR
.LP
.KS
.sp
.PS < fig15
.sp
.KE
.LP
Here again the parent interval is divided into three subintervals, the first
two of length one and the third of length zero.  In the first subinterval, \fCA\fR
is bound to the $t-list
.IP "" 10
\fC$t(1, $t(2, $t(3, _))).\fR
.LP
This records that at % t sub 0 % \fCA\fR is \fC1\fR, at % t sub 1 % \fCA\fR is \fC2\fR, at % t sub 2 %
\fCA\fR is \fC3\fR, and \fCA\fR is undefined at % t sub i %, \fCi > 2\fR.  However, the only time
points included in the first temporal interval are % t sub 0 % and % t sub 1 %,
so the only values of any significance are \fC1\fR at % t sub 0 % and 2 at % t sub 1 %.
In the third subinterval, \fCA\fR is bound to
.IP "" 10
\fC$t(4, $t(5, _))\fR
.LP
Since this subinterval begins (and ends) at % t sub 2 %, the \fC4\fR is the value of
\fCA\fR at % t sub 2 %.  Since \fCA\fR does not appear in the subgoal for the second
subinterval, we have a consistent sequence of values for \fCA\fR throughout the parent
interval, from % t sub 0 % to % t sub 2 %.  The $t-list records that \fCA\fR is \fC5\fR at
% t sub 4 %.  But % t sub 4 % is past the third subinterval (and the entire
parent interval), so the fact that \fCA\fR is \fC5\fR at % t sub 4 % is of no significance.
Note that the \fC@\fR function (as opposed to the \fC@\fR operator) does not
extend intervals.
.PP
In contrast, consider the following, where the \fC@\fR is now the operator \fC@\fR,
not the function \fC@\fR:
.IP "" 10
\fCA = 1, @(A = 2), @ @(A = 3) && skip && A = 4, @(A = 5)\fR
.LP
.KS
.sp
.PS < fig16
.sp
.KE
.LP
Here the parent interval is again divided into three subintervals, but now
the first is of length two, the second is of length one (as before), and the
third is of length one.  The first subinterval must be of length two
because the occurrence of the subgoal \fC@ @(A = 3)\fR at % t sub 0 % implies
the occurrence in the same (sub)interval of \fCA = 3\fR at % t sub 0+2 ~=~ t sub 2%.
Two suffix subintervals of the first subinterval are distinguished: one of
length one from % t sub 1 % to % t sub 2 % corresponding to the subgoal
\fC@(A = 2)\fR and the other of length zero at % t sub 2 % corresponding to the
subgoal \fC@ @(A = 3)\fR in the subinterval or, equivalently, to the subgoal
\fC@(A = 3)\fR in the suffix subinterval <% t sub 1 % % t sub 2 %>.  In the
part of the first subinterval not covered by a suffix subinterval, that is,
at % t sub 0 %, \fCA\fR is bound to
.IP "" 10
\fC$t(1, _).\fR
.LP
Since this subinterval begins at % t sub 0 %, this $t-list records that \fCA\fR is
\fC1\fR at % t sub 0 %.  In the part of the suffix subinterval <% t sub 1% % t sub 2 %>
of the first subinterval not covered by the suffix subinterval <% t sub 2 %>, that
is, at % t sub 1 %, \fCA\fR is bound to
.IP "" 10
\fC$t(2, _).\fR
.LP
Since this subinterval begins at % t sub 1 %, this $t-list records that \fCA\fR is \fC2\fR
at % t sub 1 %.  Finally, in the suffix subinterval <% t sub 2 %> of the
first subinterval, that is, at % t sub 2 %, \fCA\fR is bound to
.IP "" 10
\fC$t(3, _).\fR
.LP
Since this subinterval begins (and ends) at % t sub 3 %, this $t-list records
that \fCA\fR is \fC3\fR at % t sub 3 %.  Similarly, the third subinterval must be of
length two, and one suffix subinterval of this subinterval is distinguished.
In the part of the third subinterval not covered by the suffix subinterval
(i.e., at % t sub 3 %), \fCA\fR is bound to \fC$t(4, _)\fR, and in the final suffix
subinterval of the third subinterval \fCA\fR is bound to \fC$t(5, _)\fR.  Since \fCA\fR does
not occur in the second subinterval, <% t sub 2 % % t sub 3 %>, we have a
consistent sequence of values for \fCA\fR throughout the parent interval
<% t sub 1 % % t sub 2 % % t sub 3 % % t sub 4 %>.
.MH 3 "Discussion of Interval Lengths"
Often the length of an interval is not obvious, but depends on the length
of time required to satisfy subgoals formulated with user-defined predicates.
In such cases, one must take care that two different lengths are not specified
for the same interval, which is an inconsistency.  For example, suppose that
the predicate \fCp\fR is defined by the clause
.IP "" 10
\fCp :- r, s.\fR
.LP
Now suppose \fCr\fR and \fCs\fR are defined, respectively, by the clauses
.IP "" 10
\fCr :- length(1).
.ls 1
.IP "" 10
\fCs :- length(2).         ...(*)\fR
.ls 2
.LP
Then two different diagrams are specified:
.LP
.KS
.sp
.PS < fig17
.sp
.KE
.LP
Both intervals are closed, but they have different lengths \(em there is no
way they may be viewed as one and the same interval, and so the goal \fCp\fR
must fail.  In contrast, suppose \fCr\fR and \fCs\fR are defined by
.IP "" 10
\fCr :- @write(r).
.ls 1
.IP "" 10
\fCs :- @ @write(s).      ...(**)\fR
.ls 2
.LP
Then the diagram for \fCr\fR shows an open-ended interval of length one
.LP
.KS
.sp
.PS < fig18
.sp
.KE
.LP
and the diagram for \fCs\fR shows an open-ended interval of length two.
.LP
.KS
.sp
.PS < fig19
.sp
.KE
.LP
Since both intervals are open-ended, they may be viewed as one and the same
interval.  Specifically, since the interval for \fCr\fR is open-ended, it may be
seen as the first part of an (open-ended or closed \(em in this case, open-ended)
interval of length two.  Thus, combining the diagrams for \fCr\fR and \fCs\fR,
we get
.LP
.KS
.sp
.PS < fig20
.sp
.KE
.LP
Since Tokio terminates an interval when all subgoals are satisfied, the length
of the interval for \fCp\fR is two.  Notice that we have not bothered to indicate
the suffix subintervals generated by the \fC@\fR operators.
.MH 3 "Interval Diagrams and User-Defined Predicates"
In the last example, there are two subgoals, \fCr\fR and \fCs\fR, for
the goal \fCp\fR. The subgoals \fCr\fR and \fCs\fR themselves have
subgoals \fC@write(r)\fR and \fC@ @write(s)\fR, respectively. When we drew
the diagram for \fCp\fR, we wrote subgoals as if \fCr\fR and \fCs\fR were 
replaced with their subgoals in the definition of \fCp\fR. In general, we
shall draw diagrams so that each user-defined predicate is eliminated
in favor of the subgoals in its definition. In the last diagram, we identified
the immediate, user-defined subgoals of \fCp\fR with \fCr\fR and \fCs\fR
enclosed in \fC*\fR's to the left of where these subgoals come into play; a dotted
line was used to separate the subgoals of \fCr\fR from those of \fCs\fR.
We shall continue with this convention. This convention runs into
difficulties when a recursive predicate appears as a subgoal. If a recursive
predicate posts no subgoals into the future, then we shall treat it as a
primitive. If it does post subgoals into the future, we shall treat it as 
we treated \fC#\fR and \fC<>\fR. Finally a disjunction of subgoals will
be indicated with the Prolog \fIor\fR, \fC;\fR, as was done when we discussed
\fC<>\fR.
.PP
Consider, for example, the predicate \fCp1\fR defined by the clause
.IP "" 10
\fCp1 :- q && r, s.\fR
.LP
where \fCr\fR and \fCs\fR are defined by \fC(**)\fR and \fCq\fR is defined by
.IP "" 10
\fCq :- write(q), length(1).\fR
.LP
and \fCr\fR and \fCs\fR are defined as above. The diagram for this is
.LP
.KS
.sp
.PS <fig21
.sp
.KE
.LP
We have parameterized \fCempty\fR to indicate that the interval for \fCq\fR
is of length zero at % t sub 1 %.  
.MH 2 "Other Temporal Predicates and Operators"
.MH 3 "Enforcing a Constraint Throughout an Interval: \fC<--\fP"
With the groundwork on intervals behind us, we may now describe 
the remaining basic temporal operators of Tokio.
Evaluation of
.IP "" 10
\fCA <-- B\fR
.LP
causes the value of \fCA\fR throughout the current interval to be the value of
\fCB\fR at the beginning of the interval. Thus for example, instead of
.IP "" 10
\fC#(A = 1),\fR
.LP
we may use
.IP "" 10
\fCA <-- 1\fR
.LP
Notice that
.IP "" 10
\fClength(3), B = 1, @B = 2, A <-- B.\fR
.LP
will cause \fCB\fR to be bound to \fC$t(1, $t(2, _))\fR and  \fCA\fR to \fC$t(1, $t(1, $t(1, _)))\fR,
that is, \fCA\fR is \fC1\fR (the value of \fCB\fR at % t sub 0 %) throughout <% t sub 0 % % t sub 1 %
% t sub 2 %>.
In contrast,
.IP "" 10
\fClength(3), B = 1, @B = 2, #(A = B).\fR
.LP
will cause \fCA\fR to be \fC1\fR at % t sub 0 %, 2 at % t sub 1 %, and unbound at
% t sub 2 %. Finally,
.IP "" 10
\fCA <-- 1 && skip && length(1), A <-- 2.\fR
.LP
will cause \fCA\fR to have the value \fC1\fR at % t sub 0 %  and % t sub 1 %, and \fC2\fR at
% t sub 2 % and % t sub 3 %, while
.IP "" 10
\fCA <-- 1 && length(1), A <-- 2.\fR
.LP
will fail since it tries to bind \fCA\fR to \fC1\fR and \fC2\fR at % t sub 1 %.
.MH 3 "Evaluating a Goal Until, or Only At, the End of an Interval: \fCkeep\fP and \fCfin\fP"
Evaluation of the goal
.IP "" 10
\fCkeep(P) :-\fR
.LP 
causes \fCP\fR to be evaluated at every point but the last in the current
interval:
.LP
.KS
.sp
.PS <fig22
.sp
.KE
.LP
Evaluation of the goal
.IP "" 10
\fCfin(P)\fR
.LP
causes \fCP\fR to be evaluated at only the last point in the current interval.
.LP
.KS
.sp
.PS <fig23
.sp
.KE
.LP
Thus
.IP "" 10
\fClength(3), keep(A = 1), fin(A = 1).\fR
.LP
has the same effect as
.IP "" 10
\fClength(3), A <-- 1.\fR
.LP
However, \fCkeep\fR and \fCfin\fR are much more versatile than \fC<--\fR
since their arguments are goals, not variables. Thus, for example,
we may have
.IP "" 10
\fCkeep(write(a)), fin(write(b)).\fR
.LP
In practice, the arguments of \fCkeep\fR and \fCfin\fR usually involve
user defined predicates and produce more interesting results.
.PP
We may use \fCkeep\fR to avoid introducing an interval whose sole goal
is \fCskip\fR since, for example, \fCkeep(A = 1)\fR does not give \fCA\fR a value 
the last point in the current interval, where it overlaps with
the next interval. Thus,
.IP "" 10
\fClength(2), keep(A = 1) && A = 2\fR
.LP
is consistent, and gives \fCA\fR the value \fC1\fR for % t sub 0 % and % t sub 1 %
and the value \fC2\fR for % t sub 2 %. We may use \fCfin\fR to avoid \fC&&\fR
in this example:
.IP "" 10
\fClength(2), keep(A = 1), fin(A = 2).\fR
.PP
We may describe the meanings of \fCkeep\fR and \fCfin\fR very succinctly
in terms of \fCif ... then ...\fR and the zero-argument predicates
\fCempty\fR and \fCnotEmpty\fR we introduced earlier:
.IP "" 10
\fCkeep(P) :- #(if notEmpty then P).
.IP "" 10
\fCfin(P) :- #(if empty then P).\fR
.LP
Recall that \fCempty\fR is true only at the last time point of an interval
and not \fCnotEmpty\fR is true at all points in the interval but the last. (We
shall come to \fCif ... then\fR and \fCif ... then ... else\fR later.
In fact, in Tokio, \fCif ... then\fR is not a more
primitive notion than \fCkeep\fR or \fCfin\fR.)
.MH 3 "Dependence of Interval Termination on a Goal: \fChalt\fP"
We may introduce \fChalt(P)\fR, where \fCP\fP is some goal, in a similar fashion:
.IP "" 10
\fChalt(P) :- #(if P then empty else notEmpty).\fR
.LP
Thus, if the current interval is open-ended, then
\fChalt(P)\fR closes the current interval when \fCP\fR becomes true.
.LP
.KS
.sp
.PS < fig24
.sp
.KE
.LP
For example, the goal
.IP "" 10
\fChalt(I = J).\fR
.LP
causes the current, open-ended interval to be closed at the time % t sub i % when \fCI\fR and
\fCJ\fR have the same value. If the current interval is already closed at some
time % t sub j %, then \fChalt(I = J)\fR succeeds if and only if \fCI\fR and \fCJ\fR have 
the same value for the first time at % t sub j %.
.PP
If \fCI\fR or \fCJ\fR (or both) is unbound, then the goal %I ~=~ J% must succeed;
in this case, then, \fChalt(I=J)\fR means the same as
.IP "" 10
\fCempty, I = J\fR
.LP
From the above definition of \fChalt\fR, it follows that \fChalt(true)\fR
means the same as \fCempty\fR and \fChalt(fail)\fR means the same as
\fCnotEmpty\fR.
.MH 3 "Repeated Assignment: \fCgets\fP"
We may define further temporal operators in terms of \fC<--\fR, \fCkeep\fR
and \fCfin\fR. Thus \fCgets\fR is defined as
.IP "" 10
\fCA gets B :- keep(@A = B).\fR
.LP
For an interval of length \fCn\fR, if B has the values %v sub 0 %, ..., %v sub i %, ...,
%v sub n %
at times % t sub 0 %, ..., % t sub i %, ..., % t sub n %, we may 
diagram \fCA gets B\fR as 
.LP
.KS
.sp
.PS < fig25
.sp
.KE
.LP
Note that no value is hereby determined for \fCA\fR at the beginning 
of the interval, % t sub 0 %, and \fC@A = B\fR is not evaluated at the end of the interval
% t sub n %. The most salient fact is that the value of \fCA\fR lags that of \fCB\fR
by one time unit \(em \fCgets\fR has an obvious application in modelling a
device with unit delay. 
.MH 3 "Holding a Variable's Value Constant: \fCstable\fP"
Again, \fCstable\fR is defined as 
.IP "" 10
\fCstable(A) :- keep(@A = A).\fR
.LP
or, equivalently, as
.IP "" 10
\fCstable(A) :- A gets A.\fR 
.LP
Thus \fCstable(A)\fR forces \fCA\fR's value to remain constant, at the value it
has at % t sub 0 %, throughout the interval. An obvious use of \fCstable\fR
is to carry a value from the beginning of one interval to the beginning of
the next. For example, if \fCp(A)\fR determines the value of \fCA\fR only at the
current time and \fCq(A,B)\fR uses the current value of \fCA\fR to determine the
value of \fCB\fR, then
.IP "" 10
\fClength(2), p(A), stable(A) && q(A, B)\fR
.LP
makes available to \fCq\fR at % t sub 2 % the value of \fCA\fR determined by \fCp\fR at
% t sub 0 %. Thus:
.LP
.KS
.sp
.PS <fig26
.sp
.KE
.LP
where \fCa\fR is the value of \fCA\fR determined by  \fCp(A)\fR and \fCb\fR
is the value of \fCB\fR determined by \fCq(a,B)\fR. The reason \fCstable\fR can
carry a value from the beginning of one interval to the beginning of the
next is that the last point in the first interval is identical to
the first point of the next, and \fCstable\fR carries a value from the
first to the last point of an interval.  A common error in Tokio 
programming is to assume that the value for a variable remains stable.
In fact, however, future-time values do not exist unless they are
explicitly determined by means of temporal operators.
.MH 3 "Temporal Assignment: \fC<-\fP"
Using \fCstable\fR, we may propagate the value that a variable has
at the beginning of an interval to all future points in that interval.
Frequently, however, as just discussed, we are really interested in
setting the value of a variable at the end of an interval in terms of
the value of that variable or other variables at the beginning of 
the interval. In that case, \fC<-\fR should be used; it is defined as
.IP "" 10
\fCB <- A\ \ :-\ \ C <-- A, fin(B = C),\fR 
.LP
or, equivalently, as
.IP "" 10
\fCB <- A\ \ :-\ \ A =C, stable(C), fin(B = C).\fR
.LP
In either definition, variable \fCC\fR is a dummy variable introduced for
the sake of the definition; the specification of Tokio does not require
Tokio actually to introduce this third variable. The clearest way to
think of \fCA <- B\fR  is as \fCA <-- B\fR, but with the value of \fCA\fR determined 
only for the last time in the interval, not for the entire interval.
As with \fC<--\fR, the second argument may be a constant, variable, or
arithmetic expression. If it is a variable, its value at the beginning of 
the interval is used; if it is an arithmetic expression,  it is 
evaluated at the beginning of the interval, and the resulting value is used. An interesting application
of \fC<-\fR is to model the interchange of values in two registers. 
Suppose registers \fCA\fR and \fCB\fR each require one time unit to stabilize. Then
.IP "" 10
\fClength(1), A <- B, B <- A\fR
.LP
will cause \fCA\fR at % t sub 1 % to have the value \fCB\fR had at % t sub 0 % and
\fCB\fR at % t sub 1 % to have the value \fCA\fR had at % t sub 0 %. Note that
no intermediate variable is needed. The state of affairs described is
consistent since: although \fCA\fR (or \fCB\fR) has different values at different
times, it never has different values at the same time.
.MH 2 "Summary"
.CB "Backtracking into the Past"
.MH 1
.MH 2 "Backtracking into the Past: Simple Cases"
.PP
Recall that, in Tokio, reduction (the replacement of goals by subgoals
in an attempt to satisfy a query) is done in two directions: along the
current-time axis, and along the future-time axis. Thus there are two
sorts of backtracking: backtracking along the current-time axis, and
backtracking along the future-time axis. We shall call the latter
"backtracking into the past" since it moves backwards in time looking for
a fresh choice at an earlier time.  Reduction and backtracking along the 
current-time axis are identical to reduction and backtracking in Prolog.
We have already extensively discussed reduction along the future-time 
axis.  Backtracking into the past is easily understood in terms of 
reduction along the future-time axis.  The only difficulty occurs with
the division of the interval into subintervals by means of a \fC&&\fR
operator.  When backtracking into the past returns to a chop point,
Tokio advances the chop point to the next time.  Since the initial
division of an interval makes the first subdivision of minimal length
(length one), Tokio is thus able to generate all possible divisions
of an interval into two subintervals.  To explain the advance of a
chop point on backtracking into the past, we shall introduce interval
variables, which are internal variables marking the ends of (sub)intervals.
However, we begin discussing the simple cases of backtracking into the
past, those that do not encounter chop points.
.PP
When backtracking into the past returns to a time point % t sub i %, it
checks the subgoals that were executed when execution last was at
% t sub i %.  The first subgoal that can be resatisfied, if there is one,
is resatisfied, and execution then proceeds in the normal, forward
fashion.  If there is no goal at % t sub i % that can be resatisfied,
the backtracking returns to % t sub i-1 %.  If backtracking into the past
reaches % t sub 0 % and finds no resatisfiable subgoal there, then the
entire query fails.  We shall refer to a resatisfiable subgoal as a
"choice point".  We may then describe backtracking into the past as a
movement back through time in an attempt to find a choice point.
.PP
When backtracking returns to some time % t sub i %, the search for a
choice point at % t sub i % proceeds as in Prolog.  The catch is, however,
that the subgoals at % t sub i % are in general generated by evaluation
of subgoals at % t sub i-1 % \(em the subgoals evaluated at % t sub i % 
were put into the next queue at % t sub i-1 %.  As an example, suppose
our database contains
.IP "" 10
\fCp(1).
.ls 1
.IP "" 10 
\fCp(2).
.IP "" 10 
\fCq(1).
.IP "" 10 
\fCq(2).
.IP "" 10 
.sp
\fCr(X,Y) :- length(3), @p(X), @ @q(Y), fin(X = Y), #write((X,Y)).\fR
.ls 2
.LP
If we now issue the query
.IP "" 10
\fCtokio r(X,Y).\fR
.LP
then, at % t sub 0 %, neither \fCX\fR nor \fCY\fR has a value.  At % t sub 1 %, the
subgoal \fCp(X)\fR is evaluated. It matches the \fCp(1)\fR fact in the database, and
\fCX\fR unifies with \fC1\fR. This is a case of unification across all time, and \fCX\fR is \fC1\fR
from % t sub 1 % on.  At % t sub 2 %, \fCq(Y)\fR matches the \fCq(1)\fR fact, again a unification 
across all time, and so \fCY\fR is \fC1\fR from % t sub 2 % on. Thus, at % t sub 3 %, 
\fCfin(X = Y)\fR succeeds, and the entire query succeeds. The terminal output is:
.IP "" 10
\fC% t sub 0 %\fC: _100,_104
.ls 1
.IP "" 10
\fC% t sub 1 %\fC: 1,_108
.IP "" 10
\fC% t sub 2 %\fC: 1,1
.IP "" 10
\fC% t sub 3 %\fC: 1,1
.IP "" 10
\fC3 clock and 0.133335 sec.
.sp
.IP "" 10
\fCX = $t(_100,1)
.IP "" 10
\fCY = $t(_104,$t(_108,1))\fR
.ls 2
.LP
The \fC1\fR in \fCX\fR's $t-list represents the value of \fCX\fR for % t sub 1 % and 
subsequent times, and the \fC1\fR in \fCY\fR's $t-list represents the value of \fCY\fR
for % t sub 2 % and subsequent times. The diagram for the calculation of this 
query is
.LP
.KS
.sp
.PS <fig27
.sp
.KE
.PP
Now suppose we force a failure by typing a '\fC;\fR' before the carriage return.
There is no choice point at % t sub 3 %, so the backtrack returns to %t sub 2%.
Here it finds an alternative for \fCq(Y)\fR, which matches the fact \fCq(2)\fR.
Thus \fCY\fR's value at % t sub 2 % and subsequent times becomes \fC2\fR. Execution 
now proceeds
in the normal, forward fashion. The \fCwrite\fR at % t sub 2 % is evaluated,
then the \fCwrite\fR at % t sub 3 %, and finally the \fCX = Y\fR at % t sub 3 %
fails, forcing another backtrack. The output generated thus far since the
forced failure is:
.IP "" 10
\fC% b sub 2 %\fC: 1, 2
.ls 1
.IP "" 10
\fC% t sub 3 %\fC: 1, 2\fR
.ls 2
.LP
Note that \'% b sub i %:\' is output when a transition from % t sub i+1 %
to % t sub i % is made, while \'% t sub i %:\' is output when a transition
from % t sub i-1 % to % t sub i % is made.  Also notice that only the 
current-time goals (below the arrows) need to be considered on backtracking
into the past and when execution returns forward; there is only one way
these subgoals may be generated. (We shall find that this is no longer the
case when we consider backtracking that encounters a chop point). Backtracking
through the current-time goals at a particular time, which
is backtracking along the current-time axis, 
proceeds as if they formed the body of a Prolog clause. Note that their
order is determined partly by the order in which subgoals appear in the Tokio
clause and partly by the reordering done by Tokio.
.PP
After the failure of \fCX = Y\fR at % t sub 3 % (where \fCX\fR is \fC1\fR and \fCY\fR is \fC2\fR), another
backtrack into the past is initiated.  This finds the choice point at % t sub 2 %
exhausted (both \fCq\fR facts in the database have been used), so it returns to
% t sub 1 %. Here it finds an alternative for \fCp(X)\fR, matching it with the 
fact \fCp(2)\fR in the database. Thus the value of \fCX\fR is \fC2\fR from % t sub 1 % on.
Execution now proceeds forward. The \fCwrite\fR at % t sub 1 % is evaluated,
then the \fCq(Y)\fR goal at % t sub 2 % is encountered. Since this is encountered
anew, it presents the same two alternatives it did when first encountered.
The first alternative is taken; that is, \fCq(Y)\fR is matched with the fact
\fCq(1)\fR, and so \fCY\fR is \fC1\fR from % t sub 2 % on.  Next, the \fCwrite\fR goal at
% t sub 2 % is evaluated, then the \fCwrite\fR at % t sub 3 %, and finally
the \fCX = Y\fR goal at % t sub 3 % fails. Thus the output generated since the last
failure is:
.IP "" 10
\fC% b sub 2 %\fC: 
.ls 1
.IP "" 10
\fC% b sub 1 %\fC: 2,_108
.IP "" 10
\fC% t sub 2 %\fC: 2,1
.IP "" 10
\fC% t sub 3 %\fC: 2,1\fR
.ls 2
.PP
The failure of the \fCX = Y\fR subgoal at % t sub 3 % initiates another backtrack. 
This finds an alternative solution for \fCq(Y)\fR at % t sub 2 %\fC: q(Y)\fR is matched
with \fCq(2)\fR, so \fCY\fR is \fC2\fR from % t sub 2 % on. With execution now advancing forward,
the \fCwrite\fR goal at % t sub 2% is evaluated, then the \fCwrite\fR at 
% t sub 3 %, and \fCX = Y\fR at % t sub 3 % succeeds, so the top-level query now
succeeds for a second time. The new output is
.IP "" 10
\fC% b sub 2 %\fC: 2,2
.ls 1
.IP "" 10
\fC% t sub 3 %\fC: 2,2
.IP "" 10
\fC3 clock and 0.400002 sec.
.sp
.IP "" 10
\fCX = $t(_100,2)
.IP "" 10
\fCY = $t(_104, $t(_108,2))\fR
.ls 2
.LP
Note that the $t-lists for \fCX\fR and \fCY\fR are as they were the last time the query
succeeded except that, in place of \fC1\fR, we now have \fC2\fR. If we now
force another failure by typing ';', the backtrack thus initiated searches
back through % t sub 3 %, % t sub 2 %, % t sub 1 %, and % t sub 0 % for a
choice point, but finds none, so the query now fails. The output thus produced
is
.IP "" 10
\fC% b sub 2 %\fC:
.ls 1
.IP "" 10
\fC% b sub 1 %\fC:
.IP "" 10
\fC--fail--
.sp
.IP "" 10
\fCX = _0
.IP "" 10 
\fCY = _1\fR
.PP
.ls 2
The example just presented was chosen so that all choice points occur at
% t sub 1 % or later. This was done because of an anomaly in the 
% b sub i % lines and labels when backtracking into the past reaches
% t sub 0 %. For then the line recording the transition from % t sub 2 % to
% t sub 1 %, which should be labeled % b sub 1 %, does not appear,
and the line recording the transition from % t sub 1 % to % t sub 0 % and 
any subsequent evaluations at % t sub 0 %, which should be labeled 
% b sub 0 %, is labeled % b sub 1 %. To illustrate, we shall take
the previous example and replace \fClength(3)\fR with \fClength(2)\fR,
\fC@p(X)\fR with \fCp(X)\fR, and \fC@ @q(X)\fR with \fC@q(X)\fR. This amounts
to shifting the time line left one unit, and discarding the original 
% t sub 0 %, where nothing takes place. The database now contains
.IP "" 10
\fCp(1).
.ls 1
.IP "" 10
\fCp(2).
.sp
.IP "" 10
\fCq(1).
.IP "" 10
\fCq(2).
.sp
.IP "" 10
\fCr(X,Y) :- length(2), p(X), @q(Y), fin(X = Y), #write((X,Y)).\fR
.sp
.LP
.ls 2
The following is a transcription of a query evaluation that exactly parallels
the evaluation and re-evaluations discussed at length above:
.IP "" 10
\fC| ?- tokio r(X, Y).
.ls  1
.IP "" 10
\fC% t sub 0 %\fC: 1,_91
.IP "" 10
\fC% t sub 1 %\fC: 1,1
.IP "" 10
\fC% t sub 2 %\fC: 1,1
.IP "" 10
\fC2 clock and 0.100001 sec.
.sp
.IP "" 10
\fCX = 1
.IP "" 10
\fCY = $t(_91, 1);
.sp
.IP "" 10
\fC% b sub 1 %\fC: 1, 2
.IP "" 10
\fC% t sub 2 %\fC: 1, 2
.IP "" 10
\fC% b sub 1 %\fC: 2, _91   <--
.IP "" 10
\fC% t sub 1 %\fC: 2, 1 
.IP "" 10
\fC% t sub 2 %\fC: 2, 1
.IP "" 10
\fC% b sub 1 %\fC: 2, 2
.IP "" 10
\fC% t sub 2 %\fC: 2, 2
.IP "" 10
\fC2 clock and 0.283334 sec.
.sp
.IP "" 10
\fCX = 2
.IP "" 10 
\fCY = $t(_91, 2);
.sp
.IP "" 10
\fC% b sub 1 %\fC:
.IP "" 10
\fC-- fail --
.sp
.IP "" 10
\fCX = _0
.IP "" 10
\fCY = _1\fR
.sp
.LP
.ls 2
The arrow indicates the anomalous line. In place of this line, we should expect
the following two lines:
.IP "" 10 
\fC% b sub 1 %\fC:
.ls 1
.IP "" 10 
\fC% b sub 0 %\fC: 2, _91\fR
.ls 2
.LP
Indeed, Tokio never outputs the labels \'% b sub 0 %:\'.
It does not like to admit that 
it backtracks back to % t sub 0 %. 
.MH 2 "Backtracking into the Past: Cases Involving \fC&&\fP"
.PP
Backtracking is more difficult to understand when a chop point is encountered.
Associated with each interval is an interval variable, which is not visible
to the programmer. If an interval is closed, the interval variable for that
interval marks its last point. If an interval is open, its interval variable
has no value. In either case, the interval variable for an interval is stored
at its last point - this is where backtracking encounters it, and all
backtracking can do is advance the interval variable forward to the next time. 
Recall that a \fC&&\fR divides a parent interval into two subintervals. The 
first subinterval initially has length one, unless an \fC@\fR operator occurs
in it; this is the smallest length allowed for the first of two intervals 
generated by \fC&&\fR. We shall assume for now that no \fC@\fR operator occurs
in the first interval. The last point of the first subinterval is the first
point of the second interval. We consider here only the simple case of two
subintervals, that is, one \fC&&\fR operator. Thus, if the parent interval is
< %t sub 0 % ... % t sub n % >, then initially the first subinterval is 
< %t sub 0 %  % t sub 1 % > and the second subinterval is 
< %t sub 1 % ... % t sub n % >. If backtracking returns to  % t sub 1 %, then
the interval variable for the last subinterval is advanced to  % t sub 2 %, 
which now becomes the chop point, and the two intervals are now
< %t sub 0 % % t sub 1 % % t sub 2 % > and < %t sub 2 % ... % t sub n % >.
Each time backtracking encounters the chop point, the chop point is advanced
one unit, and so the first subinterval's length increases by one and the
second subinterval's length is decreased by one. If the only choice 
backtracking ever finds is that afforded by the chop point, and the query
never succeeds, then eventually the first subinterval is 
< %t sub 0 % ... % t sub n % > and the second is ,< % t sub n % > \(em
recall that
the second subinterval, unlike the first, may have length zero. If the query
is not satisfied at this stage, then it fails, for there are no other ways to 
divide the parent interval into two subintervals.
.PP
To introduce a succinct notation, we shall use \fCI\fR for the interval variable
of the first subinterval. If there are only two subintervals, then 
the interval variable for the parent interval and that for the 
second subinterval always mark the same point - hence neither is of much
interest in a discussion of backtracking. When \fCI\fR marks % t sub i %, and so is
stored at % t sub i %, we shall assume that its value is % t sub i %.
.PP
To take an example, suppose the database contains
.IP "" 10
\fCp(a).
.ls 1
.IP "" 10
\fCq(b).
.IP "" 10
\fCr(A) :- p(A) && @q(A).\fR
.ls 2
.LP
Suppose we then issue the query
.IP "" 10
\fCtokio length(5), r(A), #write(A).\fR
.LP
Then the chop point is at % t sub 1 %, the first subinterval is
< %t sub 0 %  % t sub 1 % >, and the second subinterval is 
< %t sub 1 % ... % t sub 5 % >. The \fCp(A)\fR goal in the first subinterval 
matches the \fCp(a)\fR fact in the database (a case of unification across
all time), so A is \fCa\fR during < %t sub 0 %  % t sub 1 % >. The \fC@q(A)\fR
goal in the second subinterval becomes the goal of \fCq(A)\fR for its
suffix subinterval < %t sub 2 % % t sub 3 % % t sub 4 % %t sub 5 % >. This
matches the \fCq(b)\fR fact in the database, so \fCA\fR is \fCb\fR during
< %t sub 2 % % t sub 3 % % t sub 4 % %t sub 5 % >. It is obvious what Tokio
will output in this case. We diagram this situation as follows:
.LP
.KS
.sp
.PS < fig28
.sp
.KE
.LP
We have written the interval variable for the first subinterval and its value
over the point where it is stored. The $t-list for \fCA\fR will be
.IP "" 10
\fC$t(a, $t(a, b))\fR
.LP
The first \fCa\fR is for %t sub 0 %, the second for % t sub 1 %, and the
\fCb\fR is the value of \fCA\fR for %t sub 2 %, % t sub 3 %, % t sub 4 %  and 
%t sub 5 %. 
.PP
Suppose that we now type ';' to force a failure. Since there are no goals or
chop points at % t sub 4 % or % t sub 3 %, backtracking returns to %t sub 2 %
in search of a choice point. But there is no choice point at %t sub 2 % 
since there is only one clause for \fCq\fR in the database. Thus backtracking 
returns to the chop point % t sub 1 %, where it finds \fCI\fR and advances it to
%t sub 2 %. After advancing \fCI\fR and while still at % t sub 1 %, execution
evaluates the \fCwrite\fR goal (not shown above) as it resumes its normal
forward progress. The first subinterval, during which \fCA\fR is \fCa\fR, is now
< %t sub 0 %  % t sub 1 % %t sub 2 % >, and the second, during which \fCA\fR, except
for its initial point, is \fCb\fR, is < %t sub 2 % % t sub 3 % % t sub 4 % %t sub 5 % >.
The output produced by Tokio, from the time the failure is
forced until the query succeeds with the second solution, is:
.IP "" 10
\fCb4 :
.ls 1
.IP "" 10 
\fCb3 :
.IP "" 10 
\fCb2 :
.IP "" 10 
\fCb1 : a
.IP "" 10 
\fCt2 : a
.IP "" 10 
\fCt3 : b
.IP "" 10 
\fCt4 : b
.IP "" 10 
\fCt5 : b\fR
.ls 2
.LP
The diagram for the second solution is
.LP
.KS
.sp
.PS < fig29
.sp
.KE
.LP
Note that it is not the case that the locations of the subgoals are unaffected
by backtracking. This is because advancing the chop point forces the goals
in the second subinterval to be generated one time unit later. Also (what is
not illustrated here), the subgoals at %t sub 0 % may be the sources for 
subgoals at one additional later time unit when \fCI\fR is advanced.
.PP
If we force a failure at the top level a second time, \fCI\fR is advanced to
% t sub 3 %, and we get
.LP
.KS
.sp
.PS < fig30
.sp
.KE
.LP
A third forced failure advances \fCI\fR to % t sub 4 %:
.LP
.KS
.sp
.PS < fig31
.sp
.KE
.LP
If we force a failure a fourth time, Tokio backtracks to % t sub 4 %, where
it finds \fCI\fR and advances it to %t sub 5 %. It then evaluates the \fCwrite\fR 
at  % t sub 4 %, then the \fCwrite\fR at %t sub 5 %, which now outputs
an \fCa\fR. It then evaluates the \fC@q(A)\fR goal at %t sub 5 %, which fails
since there is no next time. So Tokio initiates backtracking again. \fCI\fR, now
at %t sub 5 %, cannot be advanced, so backtracking goes back through 
% t sub 4 %, % t sub 3 %, and so on, searching for a choice point. The only
goal it encounters is \fCp(A)\fR at %t sub 0 %, but the single \fCp\fR clause in
the database has already been used, so the query now fails. The output
produced by Tokio beginning with the last forced failure is:
.IP "" 10
.ls 1
\fCb4 : a
.IP "" 10
\fCt5 : a
.IP "" 10  
\fCb4 : 
.IP "" 10  
\fCb3 : 
.IP "" 10  
\fCb2 :
.IP "" 10  
\fCb1 :
.IP "" 10  
\fC-- fail --\fR
.ls 2
.PP
The account just given must be modified slightly when \fC@\fR operators
occur in the first subinterval. Suppose a goal \fCP\fR contains no \fC&&\fR
operator. Then we define the "futurity" of \fCP\fR as follows:
.IP "1)" 4
If \fCP\fR contains no occurences of the \fC@\fR operation, then the futurity
of \fCP\fR is \fC0\fR.
.IP "2)" 4
If \fCP\fR is of the form \fCQ, R\fR or \fCQ; R\fR, then the futurity of 
\fCP\fR is
the maximum of the futurities of \fCQ\fR and \fCR\fR.
.IP "3)" 4
If \fCP\fR is of the form \fC@Q\fR, where \fCQ\fR is
a (possibly conjunctive or disjunctive)
goal with futurity \fCn\fR, then the futurity of \fCP\fR is \fCn+1\fR.
.LP
Thus, for example, both the following goals have futurity \fC2\fR:
.IP "" 10
\fC@@p(A)
.ls 1
.IP "" 10 
\fC@(q(B), @p(A))\fR
.ls 2
.LP
Intuitively, the futurity of a goal is the number of future time units it 
demands in the current interval. (The notion of futurity can be extended
to goals containing \fC&&\fR's; each \fC&&\fR requires at least one future
time unit.) Now suppose the (possibly conjunctive or disjunctive) subgoal
constituting the first subinterval has futurity \fCn \(>= 1\fR.
Then the length of the first subinterval is initially  \fCn\fR, not \fC1\fR
(unless \fCn = 1\fR), as we have thus far assumed. As before, however, backtracking
increases, and never decreases, the length of the first interval.
.PP
We may generalize this discussion of chop and backtracking by considering
clauses that involve more than one \fC&&\fR. If there are \fCn &&\fR
operators, none of which are within parenthesized expressions, then the
parent interval is divided into \fCn+1\fR subintervals. As before, all subintervals
but the last have minimum length of one, and the last may have length zero.
We are now concerned with the interval variables of all subintervals but the 
last. So, to distinguish the interval variables of various subintervals,
we let % I sub i % denote the interval variable of the \fCi\fRth subinterval.
We shall first present an example in which there are three chop points,
and then we shall generalize to the \fCn\fR-chop-points case. So suppose
the database contains
.IP "" 10
\fCp(a).
.ls 1
.IP "" 10 
\fCq(b).
.IP "" 10 
\fCs(c).
.IP "" 10 
\fCr(A) :- p(A) && @q(A) && @s(A).\fR
.ls 2
.LP
If we issue the query
.IP "" 10 
\fCtokio length(5), r(A), #write(A).\fR
.LP
then we get the situation
.LP
.KS
.sp
.PS < fig32
.sp
.KE
.LP
Here again we write an interval variable above the time point it marks.
If we now force a failure at the top level by typing a ';', backtracking will
search into the past and find the first choice point at % t sub 2 %, where it
advances % I sub 2 % to % t sub 3 %. After the next forced failure, backtracking will advance % I sub 2 % to % t sub 4 %:
.LP
.KS
.sp
.PS < fig33 
.sp
.KE
.LP
Another forced failure will cause Tokio to advance % I sub 2 % to % t sub 5 %.
Then, however, the \fC@s(A)\fR subgoal fails, so Tokio must backtrack into the past
and find another choice point. It thus goes back to % t sub 1 % and advances
% I sub 1 % to % t sub 2 %. As execution proceeds forward, % I sub 2 % is set
at the minimal distance from % t sub 2 %, that is, at % t sub 3 %:
.LP
.KS 
.sp
.PS < fig34
.sp
.KE
.LP
Subsequent forced failures now advance % I sub 2 % to % t sub 4 %, and then 
to % t sub 5 %, where \fC@s(A)\fR again fails, so % I sub 1 % is advanced to 
% t sub 3 % with % I sub 2 % at % t sub 4 %. There are no more solutions after
this. The following table summarizes the solutions.
.IP "" 10
.ls 1
.KS 
.EQ
delim %%
gfont R
.EN
.TS
tab (/) box;
c   s   s || c   s   s   s   s   s
c | c | c || c | c | c | c | c | c
c | c | c || c | c | c | c | c | c .
Intervals/values of A
=
%I sub 1 %/%I sub 2 %/%I sub 3 %/%t sub 0 %/%t sub 1 %/%t sub 2 %/%t sub 3 %/%t sub 4 %/%t sub 5 %
_
<%t sub 0 t sub 1%>/<%t sub 1 t sub 2 %>/<%t sub 2 t sub 3 t sub 4 t sub 5 %>/a/a/b/c/c/c
<%t sub 0 t sub 1%>/<%t sub 1 t sub 2 t sub 3 %>/<%t sub 3 t sub 4 t sub 5 %>/a/a/b/b/c/c
<%t sub 0 t sub 1%>/<%t sub 1 t sub 2 t sub 3 %>/<%t sub 4 t sub 5 %>/a/a/b/b/b/c
<%t sub 0 t sub 1 t sub 2 %>/<%t sub 2 t sub 3 %>/<%t sub 3 t sub 4 t sub 5 %>/a/a/a/b/c/c
<%t sub 0 t sub 1 t sub 2 %>/<%t sub 2 t sub 3 t sub 4 %>/<%t sub 4 t sub 5 %>/a/a/a/b/b/c
<%t sub 0 t sub 1 t sub 2 t sub 3 %>/<%t sub 3 t sub 4 %>/<%t sub 4 t sub 5 %>/a/a/a/a/b/c
.TE
.EQ
delim %%
gfont C
.EN
.sp
.KE
.ls 2
.PP
If backtracking returns to some chop point % t sub i % marked by an interval
variable % I sub j % and there exists at % t sub i % some choice other than
advancing % I sub j %, Tokio will take the other choice. For example, suppose
the database contains
.IP "" 10
\fCq(b).
.ls 1
.IP "" 10
\fCq(c).
.IP "" 10
\fCr(A) :- (keep(A = a) && q(A)), keep(write(A)), fin(write(A)).\fR
.ls 2
.LP
Note that there are two clauses for \fCq\fR, thus there are two solutions for
the goal \fCq(A)\fR. We are interested in the behaviour of the goal
.IP "" 10
\fCkeep(A = a) && q(A)\fR
.LP
in the clause defining \fCr\fR. The other two subgoals are included in this
clause only so we may see the values for \fCA\fR. We must use \fCkeep\fR  and
\fCfin\fR since the goal \fCkeep(A = a)\fR would be evaluated \fCafter\fR a simple
\fCwrite(A)\fR, which would thus not show \fCA\fR's value properly at each time.
When we issue the query
.IP "" 10
\fCtokio length(5), r(A).\fR
.LP
the following situation ensues (we ignore in the diagram goals involving
\fCwrite\fR):
.LP
.KS 
.sp
.PS < fig35
.sp
.KE
.LP
After forcing a failure at the top level, backtracking finds the first choice point
at % t sub 1 %. There are two choices here: resatisfy \fCq(A)\fR by matching the
fact \fCq(b)\fR or advancing \fCI\fR. Since advancing the interval variable is
always the last choice taken, \fCq(A)\fR is resatisfied at % t sub 1 %, and then
the value of \fCA\fR from % t sub 1 % to % t sub 5 % become \fCc\fR, not \fCb\fR.
If we force another failure, backtracking returns to % t sub 1 %. Since the
alternatives for \fCq(A)\fR have been exhausted, advancing \fCI\fR to % t sub 2 %
is the only alternative. Proceeding forward, Tokio now satisfies \fCq(A)\fR anew,
so \fCA\fR is \fCb\fR from % t sub 2 % on, and is \fCa\fR before % t sub 2 %.
Another backtrack would resatisfy \fCq(A)\fR at % t sub 2 % (changing \fCb\fR's
to \fCc\fR's); a subsequent backtrack would advance \fCI\fR to % t sub 3 % and 
satisfy \fCq(A)\fR  anew (giving \fCA\fR the value \fCb\fR from % t sub 3 % on);
etc. The following table summarizes the sequence of solutions.
.IP "" 10
.ls 1
.KS
.sp
.EQ
delim %%
gfont R
.EN
.TS
tab (/) box;
c   s || c   s   s   s   s   s
c | c || c | c | c | c | c | c
c | c || c | c | c | c | c | c .
Intervals/values of A
=
first/second/%t sub 0 %/%t sub 1 %/%t sub 2 %/%t sub 3 %/%t sub 4 %/%t sub 5 %
_
<%t sub 0 t sub 1%>/<%t sub 1 t sub 2 t sub 3 t sub 4 t sub 5 %>/a/b/b/b/b/b
<%t sub 0 t sub 1%>/<%t sub 1 t sub 2 t sub 3 t sub 4 t sub 5 %>/a/c/c/c/c/c
<%t sub 0 t sub 1 t sub 2%>/<%t sub 2 t sub 3 t sub 4 t sub 5 %>/a/a/b/b/b/b
<%t sub 0 t sub 1 t sub 2 %>/<%t sub 2 t sub 3 t sub 4 t sub 5 %>/a/a/c/c/c/c
<%t sub 0 t sub 1 t sub 2 t sub 3%>/<%t sub 3 t sub 4 t sub 5 %>/a/a/a/b/b/b
<%t sub 0 t sub 1 t sub 2 t sub 3 %>/<%t sub 3 t sub 4 t sub 5 %>/a/a/a/c/c/c
<%t sub 0 t sub 1 t sub 2 t sub 3 t sub 4%>/<%t sub 4 t sub 5 %>/a/a/a/a/b/b
<%t sub 0 t sub 1 t sub 2 t sub 3 t sub 4%>/<%t sub 4 t sub 5 %>/a/a/a/a/c/c
<%t sub 0 t sub 1 t sub 2 t sub 3 t sub 4 t sub 5%>/<%t sub 5 %>/a/a/a/a/a/b
<%t sub 0 t sub 1 t sub 2 t sub 3 t sub 4 t sub 5%>/<%t sub 5 %>/a/a/a/a/a/c
.TE
.EQ
delim %%
gfont C
.EN
.sp
.KE
.ls 2
.PP
It is possible simultaneously to chop up the same parent interval in two
different ways. This may happen any time we have a goal of the form
.IP "" 10
\fC ...,(%P sub 1% \fC&& %P sub 2%), ..., (%Q sub 1% \fC&& %Q sub 2%), ...\fR
.LP
and backtracking resets the interval variable for % P sub 1 % or % Q sub 1 %.
Hence the two \fC&&\fR's chop the parent interval independently. Let us 
denote the interval variable for % P sub 1 % by % I sup 1 % and the interval
variable for % Q sub 1 % by % I sup 2 %. Initially both % I sup 1 % and 
% I sup 2 % mark % t sub 1 %, so both \fC&&\fR's chop up the parent interval 
in the same way. Suppose backtracking returns to % t sub 1 % and there are no
alternatives at % t sub 1 % other than those presented by % I sup 1 % and 
% I sup 2 %. (For simplicity we assume that the only choice points anywhere
result from % I sup 1 % and % I sup 2 %.) Since the composite goal
(% Q sub 1 % \fC&& % Q sub 2 %) appears after (in the clause - we are concerned 
at this point with backtracking along the current time axis) the composite
goal (% P sub 1 % \fC&& % P sub 2 %), % I sup 2 % will be advanced to % t sub 2 %.
Note that now the two \fC&&\fR's chop up the parent interval in two different
ways. Subsequent backtracks into the past will encounter % I sup 2 % before
% I sup 1 %, and % I sup 2 % will be advanced until it reaches the last point
in the parent interval (assuming the parent interval is closed). Another 
failure will then cause Tokio to backtrack back to % t sub 1 %. At this
point, the only choice now is to advance % I sup 1 %. As Tokio proceeds forward,
% I sup 2 % is set anew to mark % t sub 1 %. Subsequent backtracks into the
past now encounter % I sup 1 % before % I sup 2 %, so % I sup 1 % is now
advanced, while % I sup 2 % sits at % t sub 1 %. Eventually, after a 
sufficient number of failures, % I sup 1 % will reach the end of the parent 
interval. Another failure would cause the entire goal shown above to fail.
.PP
This sort of situation is complex enough to warrant an example. So suppose the
database contains
.IP "" 10
\fCtest :- length(5),
.ls 1
.IP "" 15
\fCN = 3, (N gets N + 1 && stable(N)),
.IP "" 15
\fCM = 0, (M gets M + 1 && stable(M)),
.IP "" 15
\fCfin(M = N),
.IP "" 15
\fC#write((N,M)).\fR
.ls 2
.LP
if we issue the query,
.IP "" 10
\fCtokio test.\fR
.LP
at first both % I sup 1 % and % I sup 2 % mark % t sub 1 %. Thus \fCN\fR is
incremented from \fC3\fR at % t sub 0 % to \fC4\fR at % t sub 1 % and then remain constant,
and \fCM\fR is incremented from \fC0\fR at % t sub 0 % to 1 at % t sub 1 % and then remains
constant. Consequently, at % t sub 5 % \fCN\fR is \fC4\fR and \fCM\fR is \fC1\fR, so \fCfin(M = N)\fR
fails:
.LP
.KS
.sp
.PS < fig36
.sp
.KE
.LP
We have simplified the lists of goals shown in the diagram. Also the 
subintervals due to the first \fC&&\fR are drawn with a \(em line, while those
due to the second \fC&&\fR are drawn with a --- line. The failure of 
\fCfin(M = N)\fR at % t sub 5 % initiates backtracking into the past, which
finds no choice points until % t sub 1 %. Neither \fCstable\fR goal can be
resatisfied, so the interval variable due to the second \fC&&\fR, that is, 
% I sup 2 %, is advanced to % t sub 2 %. Thus the \fCM gets M + 1\fR subgoal
must be evaluated at % t sub 2 %, resulting in \fCM\fR having the value \fC2\fR at 
% t sub 2 %. The \fCstable(M)\fR subgoal now does not appear until % t sub 2 %,
marked now by % I sup 2 %. Thus,
.LP
.KS
.sp
.PS < fig37
.sp
.KE
.LP
The failure of \fCfin(M = N)\fR at % t sub 5 % again initiates another 
backtrack, which advances % I sup 2 % to % t sub 3 %. Thus \fCM\fR is incremented to
\fC3\fR before it is held stable. At % t sub 5 %, \fCM\fR is now \fC3\fR, so \fCfin(M = N)\fR
again fails. The resulting backtrack advances % I sup 2 % to % t sub 4 %, and
thus \fCfin(M = N)\fR finally succeeds:
.LP
.KS
.sp
.PS < fig38
.sp
.KE
.PP
Notice that there are two invariants at % t sub 5 %:
.IP "" 10
\fCN = 3 + % I sup 1 %
.ls 1
.IP "" 10
\fCM = 0 + % I sup 2 %\fR 
.ls 2
.LP
If backtracking never advances % I sup 1 % beyond % t sub 1 %, then \fCN = 3+1 = 4\fR
at % t sub 5 %. Thus \fCM = N = 4\fR at % t sub 5 % when \fCM = % I sup 2 %  = 4\fR,
that is, when \fC% I sup 2 % = 4\fR. Thus we know in advance that \fCfin(M = N)\fR 
will fail three times before it succeeds. We may describe the entire
evaluation succintly by showing only the termination of intervals after
subsequent backtracks, and by writing the invariants at % t sub 5 % beneath
% t sub 5 %:
.LP
.KS 
.sp
.PS < fig39
.sp
.KE 
.LP 
.PP
In the example just presented, only % I sup 2 % (and not % I sup 1 %) was
advanced by backtracking. We now modify the example so that both % I sup 2 % 
and % I sup 1 % must be advanced before a solution is found. The database
will now contain:
.ft C
.IP "" 10
\fCtest :- length(5),
.ls 1
.IP "" 15
\fCN = 0, (N gets N + 1 && stable(N)),
.IP "" 15
\fCM = 3, (M gets M + 1 && stable(M)),
.IP "" 15
\fCfin(M = N),
.IP "" 15
\fC#write((N,M)).
.ft R
.ls 2
.LP
Comparing this with the previous example, we see that, for this example, the
invariant at % t sub 5 % is
.ft C
.IP "" 10
\fCN = 0 + % I sup 1 %
.ls 1
.IP "" 10
\fCM = 3 + % I sup 2 %
.ft R
.ls 2
.LP
and the successive states of affairs that result when backtracking advances
% I sup 2 % are, in our succint notation:
.LP
.KS
.sp
.PS < fig40
.sp
.KE
.LP
If backtracking never advances % I sup 1 % beyond % t sub 1 %, then \fCN = 1\fR.
With \fC1 \(<=\fR % I sup 2 % \fC\(<= 5\fR and \fCM = 3 +\fR % I sup 2 % at % t sub 5 %, there is
no solution to %M ~=~ N% at % t sub 5 %. Thus to find a solution, % I sup 1 %
must be advanced.
.PP
Consider the state of affairs when % I sup 1 % = % t sub 1 %, and % I sup 2 %
= % t sub 5 %. (This is the last state of affairs covered in the succint 
diagram above.) The diagram for this is:
.LP
.KS
.sp
.PS < fig41
.sp
.KE
.LP
The failure at % t sub 5 % causes evaluation to backtrack back through 
% t sub 4 %, % t sub 3 %, and % t sub 2 %, until it finds a choice point at
% t sub 1 %. When backtracking into the past previously reached % t sub 1 %,
backtracking along the current-time axis resatisfied the second \fC&&\fR
subgoal, with the result that % I sup 2 % was advanced to % t sub 2 %. When
backtracking into the past reaches % t sub 1 % this time, it again backtracks
along the current-time axis. It now finds the alternatives for the second 
\fC&&\fR subgoal (governing % I sup 2 %) exhausted. Thus Tokio backtracks
further along the current-time axis at % t sub 1 %. The next choice it
encounters ( and indeed, the only choice remaining at % t sub 1 %) is the
alternative for the first \fC&&\fR subgoal (governing % I sup 1 %). Thus
% I sup 1 % is advanced to % t sub 2 %. Proceeding forward, Tokio evaluates
the second \fC&&\fR goal anew, and so % I sup 2 % is placed at % t sub 1 %.
.LP
.KS
.sp
.PS < fig43
.sp
.KE
.PP
Failure of \fCfin(M = N)\fR at % t sub 5 % initiates a backtrack that
advances % I sup 1 % to % t sub 3 %, and % I sup 1 % now advances on
success or failure as % I sup 2 % did before.  With % I sup 2 % fixed at \fC1\fR,
we see from our invariant that, at % t sub 5 %, \fCM = 3 + 1 = 4\fR and \fC1 \(<= N \(<= 5\fR.
There is thus a solution for \fCM = N\fR at % t sub 5 %, namely, when % I sub 1 ~=~ 4 %.
Thus, \fCfin(M = N)\fR and the entire top-level goal succeed after two failures
as evaluation proceeds from the state of affairs depicted above.  The sequence
of backtracks advancing % I sub 2 % are succintly portrayed as
.LP
.KS
.sp
.PS < fig44
.sp
.KE
.PP
The chops we have just considered may be referred to as parallel chops: they
chop up the same interval, possibly in different ways.  The chops we
considered  earlier were sequential chops: they chop up a single interval
into a sequence of subintervals.  As there may be two or more sequential 
chops in a single parent interval, so there may be two or more parallel
chops in a parent interval.  Any one of a set of parallel intervals may be treated
like any other interval.  In particular, there may be sequential chops
within a parallel interval.  Similarly, there may be parallel chops within a 
sequential interval.
.MH 2 "Summary"
.CB "Conditionals and Iteration"
.MH 1
.MH 2 "Conditionals"
.PP
Tokio defines its own conditional statement, which has the form:
.IP "" 10
if % G sub 1 % then % G sub 2 % else % G sub 3 %
.LP
The \fCelse\fR part is optional.  Here % G sub 1 %, % G sub 2 %, and % G sub 3 %
are any Tokio goals.  There is no need to enclose any of % G sub 1 %, % G sub 2 %,
or % G sub 3 % within parentheses since they are evaluated before the
conditional itself.
.PP
As an example, consider the clause
.ls 1
.IP "" 10
.ft C
.nf
test :- length(5), Flg = 0,
	#( Flg gets 1 - Flg,
	   if Flg = 0
	       then write (0)
	       else write (1)
	 ).
.fill
.sp
.ls 2
.ft R
.LP
The following diagram illustrates how this is evaluated:
.LP
.KS
.sp
.PS < fig42
.sp
.KE
.LP
Thus, the value of \fCFlg\fR is output at each time point. If the \fCelse\fR
part were omitted, the value of \fCFlg\fR would be output only when it is \fC1\fR.
That is, given a conditional 
.IP "" 10
.ft C
if % G sub 1 % then % G sub 2 %
.ft R
.LP
if % G sub 1 % fails, then the entire conditional succeeds (although the
\fCthen\fR part is skipped).
.PP
Any of the constituent goals of a conditional may be composite (involve
more than one predicate).  For example, in the clause above, the
conditional could be (if the predicates \fCfoo1\fR and \fCfoo2\fR are also
defined):
.ls 1
.IP "" 10
.ft C
.nf
(if Flg = 0
     then foo1(X), write(0)
     else foo2(X), write(1)),
write(X)
.fill
.sp
.ls 2
.ft R
.LP
Notice that the parentheses around the conditional are required so that
the \fCwrite(X)\fR does not become incorporated into the \fCelse\fR part.
Now, suppose \fCFlg\fR is 0 so the \fCthen\fR part is selected.  Then the
goal becomes
.IP "" 10
\fCfoo1(X), write(0)\fR
.LP
If the subgoal \fCfoo1(X)\fR fails, then the entire conditional fails; if
it succeeds, then \fCwrite(0)\fR is evaluated and succeeds, and so the entire
conditional succeeds.  The situation is similar if \fCFlg\fR is \fC1\fR and the
\fCelse\fR part is taken.  Put succintly, once the goal following \fCif\fR has
been evaluated, the success or failure of the conditional rides on the
success or failure of either the \fCthen\fR goal or the \fCelse\fR goal,
whichever is selected.
.PP
Although the parentheses are not required around the constituent goals in
a conditional, their presence sometimes improves readability.  Tokio also
allows curly braces, \fC{ ... }\fR, to be used like parentheses.
.LP
For example, the last example could be written as
.ls 1
.IP "" 10
.ft C
.nf
(if { Flg = 0 }
    then { foo1(X), write(0) }
    else { foo2(X), write(1) } ),
write(X)
.fill
.sp
.ls 2
.ft R
.LP
Our convention shall be to enclose only composite goals within curly braces
and not to use parentheses for this purpose, although they may be used to
enclose an entire conditional.  (Note that curly braces may be used anywhere
to enclose a \(em usually composite \(em goal.)
.MH 3 "Nested Conditionals"
Conditionals may be nested in any fashion.  For example, the \fCthen\fR goal
may itself be a conditional:
.ls 1
.IP "" 10
.ft C
.nf
if %G sub 1%
    then if %G sub 2%
	    then %G sub 3%
	    else %G sub 4%
    else %G sub 5%
.fill
.sp
.ls 2
.ft R
.LP
Note that parentheses or braces are not needed, although this example is
clearer if written as
.ls 1
.IP "" 10
.ft C
.nf
if %G sub 1%
    then { if %G sub 2%
	    then %G sub 3%
	    else %G sub 4% }
    else %G sub 5%
.fill
.sp
.ls 2
.ft R
.LP
The dangling \fCelse\fR problem is resolved by associating an \fCelse\fR
with the nearest \fCif\fR.  Thus
.ls 1
.IP "" 10
.ft C
.nf
if %G sub 1%
   then 
   if %G sub 2%
   then %G sub 3%
   else %G sub 4%
.fill
.sp
.ls 2
.ft R
.LP
is parsed as 
.ls 1
.IP "" 10
.ft C
.nf
if %G sub 1%
    then { if %G sub 2%
	    then %G sub 3%
	    else %G sub 4% }
.fill
.sp
.ls 2
.ft R
.LP
Also, in the following, braces (or, alternatively, parentheses) are required
if the conditionalis to be parsed as shown:
.ls 1
.IP "" 10
.ft C
.nf
if %G sub 1%
    then { if %G sub 2%
	        then %G sub 3% }
    else %G sub 4% 
.fill
.sp
.ls 2
.ft R
.PP
Probably the most useful way to nest conditionals is within the \fCelse\fR
goals.  This produces a multiple-branch structure, as in the following:
.ls 1
.IP "" 10
.ft C
.nf
if %G sub 1% then
    %G sub 2%
else if %G sub 3% then
    %G sub 4%
      \(bu
      \(bu
      \(bu
else if %G sub n-1% then
     %G sub n%
else
     %G sub n+1%
.fill
.sp
.ls 2
.ft R
.LP
This conditional has %n over 2 ~+~ 1% branches (one of them being the
\fCelse\fR at the end).
.MH 3 "Conditionals and Backtracking"
The behavior of conditionals in the context of backtracking is straightward.
Recall that once it is determined whether the \fCthen\fR or the \fCelse\fR
is taken, the success or failure of the conditional as a whole rides on the
success or failure of the \fCthen\fR goal or the \fCelse\fR goal.  If
backtracking returns to the conditional, an attempt is made to resatisfy the
goal selected.  If this fails, then the entire conditional fails to be
resatisfied.  Note that no attempt is made to resatisfy the \fCif\fR goal.
.PP
To take an example, consider
.ls 1
.IP "" 10
.ft C
.nf
q(3).
q(2).
q(1).
t(X) :- length(3), g(X), #write(X),
	if X = 1 then
	    { write(a), write(b) }
	else if X = 2 then
	    { keep(write(c)), fin(write(c)) && write(d) }
	else
	    { write(e), @ @ write(f), #write(foo) }.
.fill
.sp
.ls 2
.ft R
.LP
In the branch taken if \fCX = 2\fR, we have written
.IP "" 10
\fCkeep(write(c)), fin(write(c))\fR
.LP
instead of simply
.IP "" 10
\fCwrite(c)\fR
.LP
so that, when backtracking advances the chop point, \fCwrite\fR is still
evaluated at the point where backtracking encountered the chop point.  If
only \fCwrite(c)\fR were used, the chop point would be advanced beyond
this point and no \fCwrite\fR would be evaluated at this point.
.PP
When the clause \fCt\fR is evaluated, subgoal \fCq(X)\fR matches the fact
\fCq(3)\fR in the database, so the third branch is taken.  This causes
\fCwrite(e)\fR to be evaluated at %t sub 0%, \fCwrite(f)\fR to be
evaluated at %t sub 2%, and \fCwrite(foo)\fR to be evaluated at all points
in the interval, namely, at %t sub 0%, %t sub 1%, %t sub 2%, and %t sub 3%.
In addition, in parallel with the conditional, \fCwrite(X)\fR is evaluated
at all points in the interval. The output, then, is:
.IP "" 10
\fCt0: 3 e foo
.ls 1
.IP "" 10
\fCt1: 3   foo
.IP "" 10
\fCt2: 3 f foo
.IP "" 10
\fCt3: 3   foo
.sp
.IP "" 10
\fCX = 3\fR
.ls 2
.LP
If we then force a failure at the top level, backtracking is initiated and
Tokio tries to resatisfy the branch taken, namely,
.IP "" 10
\fCwrite(e), @ @ write(f), #write(foo)\fR
.LP
Since the only predicate involved is \fCwrite\fR, there is no way this may be
resatisfied, so the entire conditional fails, and backtracking returns to the
subgoals before the conditional.
.PP
The only resatisfiable goal backtracking finds is \fCq(X)\fR.  This is now matched
with the fact \fCq(2)\fR in the database, and evaluation resumes in the usual
forward direction.  The conditional is encountered, and since \fCX\fR is \fC2\fR, Tokio
now selects the second branch, namely,
.IP "" 10
.ft C
keep(write(c)), fin(write(c)) && write(d)
.ft R
.LP
As always, the first subinterval is given length one initially, so \fCc\fR is
output at %t sub 0% and %t sub 1%, and \fId\fR is also output at %t sub 1%.  The
output to this point, from the time backtracking was initiated, is thus (recall
that the value of \fCX\fR is output at all times):
.IP "" 10
\fCb2:
.ls 1
.IP "" 10
\fCb1: 2 c
.IP "" 10
\fCt1: 2 c d
.IP "" 10
\fCt2: 2
.IP "" 10
\fCt3: 2
.sp
.IP "" 10
\fCX = 2\fR
.ls 2
.LP
Note that the time labeled "\fCb1:\fR" is actually %t sub 0%.
.PP
If backtracking is initiated again, tokio attempts to resatisfy the same
branch.  It does so by advancing the chop point from %t sub 1% to %t sub 2%.
To do this, it must go back to %t sub 1%, and then proceed forward anew.  The
new output is:
.IP "" 10
\fCb2:
.ls 1
.IP "" 10
\fCb1: c
.IP "" 10
\fCt2: 2 c d
.IP "" 10
\fCt3: 2
.sp
.IP "" 10
\fCX = 2\fR
.ls 2
.LP
(Note that only the \fCwrite(c)\fR, and not the \fCwrite(X)\fR, was evaluated at
%t sub 1%.)  Another backtrack will advance the chop point from %t sub 2% to
%t sub 3%:
.IP "" 10
\fCb2: c
.ls 1
.IP "" 10
\fCt3: 2 c d
.sp
.IP "" 10
\fCX = 2\fR
.ls 2
.MH 3 "Composite \fCif\fP Goals"
As mentioned before, any of the goals in a conditional (the \fCif\fR goal,
the \fCthen\fR goal, or the \fCelse\fR goal) may be composite; in fact, any
of them may be arbitrarily complex.  So far, we have seen examples of composite \fCthen\fR and \fCelse\fR goals.  We turn now to cases in which the \fCif\fR
goal is composite.  We first consider composite \fCif\fR goals involving
no temporal operators, and then we look at cases in which temporal operators
are involved.
.PP
The first thing to note is that a variable, say \fCX\fR, appearing in the \fCif\fR
goal is the same variable as an \fCX\fR appearing in the \fCthen\fR or \fCelse\fR
goal.  For example, suppose predicate \fCt\fR is defined by
.ls 1
.IP "" 10
.ft C
.nf
t :- if q(X)
       then write(X)
       else write('q(X) failed').
.fill
.sp
.ls 2
.ft R
.LP
Then, if \fCq(X)\fR succeeds with \fCX\fR bound to \fC1\fR, since the \fCX\fR in the \fCelse\fR goal is
the same \fCX\fR as the \fCX\fR in the \fCthen\fR goal, the value \fC1\fR will be output.
.PP
When a composite \fCif\fR goal involves no temporal operator, it is evaluated
like a composite Prolog goal with the exception of one feature to be mentioned
shortly.  In particular, backtracking along the current time axis within the
\fCif\fR goal proceeds as in Prolog.  As an example, suppose the database
contains
.IP "" 10
\fCq(3).
.ls 1
.IP "" 10
\fCq(2).
.IP "" 10
\fCq(1).
.sp
.IP "" 10
\fCp(1).
.IP "" 10
\fCp(2).
.sp
.IP "" 10
.nf
\fCt :- if q(X), p(X)
	 then write(yes)
	 else write(no).\fR
.ls 2
.fill
.LP
When the \fCt\fR goal is evaluated, the subgoal \fCq(X)\fR in the \fCif\fR goal
will succeed with \fCX\fR bound to \fC3\fR.  Then the \fCp(X)\fR subgoal fails, backtracking
returns to \fCq(X)\fR, which is resatisfied with \fCX\fR bound to \fC2\fR, and then a new evaluation
of \fCp(X)\fR succeeds.  Thus, the \fCthen\fR goal is selected, and \fCyes\fR to
output at %t sub 0%.
.PP
Now suppose the \fCif\fR goal in the above definition of \fCt\fR is changed
to
.IP "" 10
\fCq(X), p(Y), X = Y\fR
.LP
We would expect that first of all the \fCq(X)\fR subgoal would succeed with \fCX\fR bound to \fC3\fR,
then the \fCp(Y)\fR subgoal would succeed with \fCY\fR bound to \fC1\fR, and then
\fCX = Y\fR subgoal would fail, thus initiating backtracking.  What in fact
happens is that, after \fCq(X)\fR succeeds, Tokio looks for a fact \fCp(3)\fR
in the database (and fails).  That is, Tokio incorporates the \fCX = Y\fR
constraints directly into the variables of the other subgoals.  This is the
feature alluded to above in which a Tokio \fCif\fR goal involving no temporal
operator differs from a Prolog goal.
.PP
When the \fCif\fR goal contains temporal operators, its success or failure
at the first part of the interval (which we shall assume to be %t sub 0%)
alone determines whether the \fCthen\fR goal or the \fCelse\fR goal is selected,
but, if the \fCif\fR goal fails at some %t sub i%, \fCi\fR > 0, then the entire
conditional fails.  There is no backtracking into the past within the \fCif\fR
goal, although, as we have seen, there may be backtracking along the current
time-axis.  Thus, when the \fCif\fR goal involves
temporal operators and succeeds at %t sub 0% (so the \fCthen\fR goal
is selected), evaluation of the \fCif\fR goal at times %t sub i%, \fCi > 0\fR,
monitors the state of affairs as time progresses; if things do not transpire as
stated in the \fCif\fR goal, the \fCthen\fR goal is abandoned.
.PP
As an example, suppose the database contains
.IP "" 10
\fCq(2).
.ls 1
.IP "" 10
\fCq(1).
.sp
.IP "" 10
\fCp(1).
.IP "" 10
\fCp(3).
.IP "" 10
.nf
\fCt1 :- if @q(X), #write(X)
	 then #write(yes)
	 else #write(no).\fR
.fill
.sp
.ls 2
.LP
When \fCt1\fR is evaluated, the only subgoal derived from the \fCif\fR goal
that is evaluated at %t sub 0% is \fCwrite(X)\fR.  This succeeds, and so the
\fCthen\fR goal is selected.  Thus, at %t sub 0%, a value such as \fC_78\fR (indicating
an unbound variable) is output for \fCX\fR, and this is followed by a \fCyes\fR
output by the \fCthen\fR goal.  At %t sub 1%, the subgoal \fCq(X)\fR, derived
from the \fCif\fR goal, is evaluated and succeeds, with \fCX\fR bound to \fC2\fR.  Thus, \fC2\fR
is output by the \fCwrite(X)\fR derived from the \fCif\fR goal, and the \fCthen\fR
goal is permitted to proceed, and so outputs another \fCyes\fR.
.PP
Now suppose there are no \fCq\fR facts in the database, so the \fC@q(X)\fR
in the \fCif\fR goal fails.  Since this has no effect until %t sub 1%, the
situation remains unchanged at %t sub 0%; in particular, the \fCthen\fR
goal is still selected.  At %t sub 1%, \fCq(X)\fR fails, so the \fCwrite(X)\fR
is not evaluated, and the \fCthen\fR goal is abandoned, so \fCwrite(yes)\fR
is not evaluated.  Finally, the entire conditional fails with no attempt at
resatisfying \fCq(X)\fR.
.PP
Next, suppose we have the same database, but with the definition of \fCt2\fR
replaced with
.ls 1
.IP "" 10
.ft C
.nf
t2 :- if length(1), (q(X) && p(X)), #write(X)
	 then #write(yes)
	 else #write(no).
.fill
.sp
.ls 2
.ft R
.LP
When \fCt2\fR is evaluated, \fCq(X)\fR will succeed at %t sub 0% with \fCX\fR
bound to \fC2\fR.  Thus \fCwrite(X)\fR outputs \fC2\fR, the \fCthen\fR goal is selected,
and \fCwrite(yes)\fR outputs \fCyes\fR.  The chop point occurs at %t sub 1%.
Here \fCX\fR is still \fC2\fR, but the attempt to satisfy \fCp(X)\fR at %t sub 1%
fails.  Thus the entire conditional fails, and in particular, the \fCthen\fR
goal is abandoned.  Note that no attempt is made to backtrack into the past
to resatisfy \fCq(X)\fR at %t sub 0%.  If, on the other hand, the \fCif\fR
goal were
.IP "" 10
\fClength(2), (g(X) && @p(X)), #write(X)\fR
.LP
then the \fCif\fR goal would succeed at %t sub 1%, resulting in \fC2\fR (for \fCX\fR)
and \fCyes\fR being output.  At %t sub 2%, \fCX\fR would initially be
unbound, so \fCp(X)\fR would succeed with \fCX\fR bound to \fC1\fR.
.MH 2 "Iteration Across Time"
.MH 3 "Recursion with Temporal Operators"
Sometimes it is natural to combine recursion with temporal operators
to drive evaluation of Tokio predicates through time.  We content
ourselves with a simple example. Let
.ls 1
.IP "" 10
.ft C
.nf
loop(I) :- I < 4,
	     @I = I + 1
	 && loop(I).
loop(I).

t :- I = 0, loop(I), #write(I).
.fill
.sp
.ls 2
.ft R
.LP
Note that the subgoals in the first \fCloop\fR clause are associated as
.IP "" 10
\fC(I < 4, @I = I + 1) && loop(I)\fR
.LP
When \fCt\fR is evaluated, \fCI\fR at %t sub 0% gets the value \fC0\fR.  The
remaining subgoals, \fCloop(I)\fR and \fC#write(I)\fR, and evaluated in
parallel, so, at each time %t sub i%, \fCi \(>= 0\fR, the value
\fCloop\fR gives to \fCI\fR is output by \fCwrite\fR.  When \fCloop\fR
is evaluated at %t sub 0%, \fCI\fR is 0, so I < 4 succeeds, and
.IP "" 10
\fC@I = I + 1\fR
.LP
causes \fCI\fR to have the value 1 at %t sub 1%. The \fC&&\fR causes the 
recursive \fCloop(I)\fR subgoal to be evaluated at %t sub 1%.  At %t sub 1%,
then, \fCI\fR is \fC1\fR, so \fCI < 4\fR succeeds, \fCI\fR at %t sub 2% gets the value \fC2\fR, and
\fCloop(I)\fR is evaluated at %t sub 2%.  At %t sub 2%, \fCI\fR at %t sub 3% gets
\fC3\fR, and, at %t sub 3%, \fCI\fR at %t sub 4% gets the value \fC4\fR.  At %t sub 4%,
\fCI < 4\fR fails, so the first \fCloop\fR clause fails; hence the recursive
subgoal \fCloop(I)\fR in the \fCloop\fR clause as evaluated at %t sub 3%
(so the recursive subgoal is evaluated at %t sub 4% because of the \fC&&\fR)
is satisfied by the second \fCloop\fR clause in the database.  Since this
clause has no subgoals, nothing more is done, and the evaluation of \fCt\fR
succeeds.  The resulting output is :
.IP "" 10
\fCt0 : 0
.ls 1
.IP "" 10
\fCt1 : 1
.IP "" 10
\fCt2 : 2
.IP "" 10
\fCt3 : 3
.IP "" 10
\fCt4 : 4\fR
.ls 2
.PP
Now suppose we force the last subgoal in the evaluation just traced
to fail by typing a "\fC;\fR".  The last subgoal was satisfied by the second
\fCloop\fR clause in the database.  Since this clause has no subgoals, the
\fCloop\fR subgoal after the \fC&&\fR in the last call to the first
\fCloop\fR clause fails.  Backtracking first encounters the \fC&&\fR, so
we backtrack one time unit into the past, from %t sub 5% to %t sub 4%, and
advance the chop point from %t sub 4% to %t sub 5%.  The value of \fCI\fR
at %t sub 4% remains \fC4\fR.  Tokio reports this backtracking into the past
by outputting
.IP "" 10
\fCb4 : 4\fR
.LP
That is, we backtrack back to %t sub 4% (to advance the chop point), and as
execution proceeds forward, the \fCwrite\fR resulting from \fC#write(1)\fR is
the last thing evaluated before we move from %t sub 4% to %t sub 5%.  At
%t sub 5%, we must now satisfy the \fCloop(1)\fR subgoal after \fC&&\fR.  This
is first attempted by trying the first \fCloop\fR clause.  The first subgoal
in this is \fCI < 4\fR.  But now I has no value at %t sub 5%.  So when an attempt is made
to evaluate \fII < 4\fR, the system reports that an argument in an arithmetic 
expression is not a number, and bombs.
.PP
This problem is important because, when we define a predicate, we put
no constraint on the contexts in which it may be used.  In particular,
any predicate we define must make a reasonable response when encountered
by backtracking.  One reasonable way for the \fCloop\fR predicate to
behave in backtracking might be to extend the value of \fCI\fR at %t sub 4%
to %t sub 5%, and then carry on with the sequence as usual for subsequent times.
However, given the way \fCloop\fR is defined, this is not natural and cannot
be achieved in a straightforward fashion.  A more reasonable way for \fCloop\fR
to behave in backtracking is to throw away the last time and have the recursion
terminate one time point earlier, at %t sub 3% in our example.  The intuition
behind \fCloop\fR is that it gives \fCI\fR the value \fCi\fR at time
%t sub i% until \fCi\fR equals \fC4\fR.  If a value is propagated back to a \fCloop\fR
subgoal, \fCloop\fR in effect is asked to supply another solution, which we might
take to mean the next less committal solution.  We are claiming that the next less
committal solution is that which is identical to the original solution except that
it does not determine \fCI\fR at the last time point where the original
solution determined it.  What this alternative solution should not do, we
claim, is move any chop points,  The \fC&&\fR is included in \fCloop\fR
so that \fCloop\fR may drive time forward one point per recursion cycle.  If
chop points could be moved forward in time, \fCloop\fR would no longer drive
time in the same simple, uniform manner.
.PP
The way to fix the chop point so that they are always one time unit apart
is to include a \fClength(1)\fR subgoal before the \fC&&\fR in the first
\fCloop\fR clause. Recall that \fCskip\fR is the same as \fClength(1)\fR.
So our modified definition of \fCloop\fR is 
.ls 1
.IP "" 10
.ft C
.nf
loop(I):- I < 4,
              @I = I + 1, skip
       && loop(I),
loop(I).
.fill
.sp
.ls 2
.ft R
.LP
Suppose we again define \fCt\fR by
.IP "" 10
\fCt :- length(5), I = 0, loop(I), #write(I).\fR
.LP
Then evaluating \fCt\fR gives, as before, the output
.IP "" 10 
\fCt0: 0
.ls 1
.IP "" 10
\fCt1: 1
.IP "" 10
\fCt2: 2
.IP "" 10
\fCt3: 3
.IP "" 10
\fCt4: 4
.IP "" 10
\fCt5: _10\fR
.ls 2
.LP
where \fC_10\fR is some unbound variable. If we type '\fC;\fR' to force a backtrack,
then the loop subgoal after the \fC&&\fR in the last call to \fCloop\fR
fails. Since the chop point cannot be moved (because of the \fCskip\fR)
and none of the previous subgoals can be resatisfied, this call to \fCloop\fR 
fails. This means that the \fCloop\fR subgoal after the \fC&&\fR in the previous
call to \fCloop\fR  fails. But now this subgoal may be satisfied by the second
\fCloop\fR clause, which now terminates the recursion. Note that we have 
traversed backwards over one \fC&&\fR, moving from % t sub 5 % to % t sub 4 %,
and over a second \fC&&\fR, moving from % t sub 4 % to % t sub 3 %.
Resatisfying the last (in the backward direction) \fCloop\fR subgoal
we have just considered does not require backtracking over a further \fC&&\fR.
Thus we backtrack to % t sub 4 %, then to % t sub 3 %, where a \fCloop\fR 
subgoal is resatisfied by the nonrecursive clause and \fCwrite(I)\fR is
executed again, outputting \fC3\fR, and time proceeds forward again, but now with
no values for \fCI\fR, since the \fCloop\fR subgoal in \fCt\fR finished at 
% t sub 3 %:
.IP "" 10
\fCb4:
.ls 1
.IP "" 10
\fCb3: 3
.IP "" 10
\fCt4: _9
.IP "" 10
\fCt5: _10\fR
.ls 2
.PP
If we force another backtrack, we go back to % t sub 2 % and resatisfy with
the nonrecursive \fCloop\fR clause:
.IP "" 10
\fCb4:  
.ls 1
.IP "" 10
\fCb3: 
.IP "" 10
\fCb2: 2
.IP "" 10
\fCt3: _8
.IP "" 10
\fCt4: _9 
.IP "" 10
\fCt5: _10\fR
.ls 2
.LP
Another forced backtrack take us back to \fCt1\fR:
.IP "" 10
\fCb4: 
.ls 1
.IP "" 10
\fCb3:
.IP "" 10
\fCb2:
.IP "" 10
\fCb1: 1
.IP "" 10
\fCt2: _7
.IP "" 10
\fCt3: _8
.IP "" 10
\fCt4: _9
.IP "" 10
\fCt5: _10\fR
.ls 2
.LP
Another takes us to % t sub 0 %:
.IP "" 10
\fCb4:
.ls 1
.IP "" 10
\fCb3:
.IP "" 10
\fCb2:
.IP "" 10
\fCb1: 0
.IP "" 10
\fCt1: _6
.IP "" 10
\fCt2: _7  
.IP "" 10
\fCt3: _8 
.IP "" 10
\fCt4: _9 
.IP "" 10
\fCt5: _10\fR
.ls 2
.LP 
(The '\fC0\fR' should actually be next to a '% b sub 0 %:', not a '% b sub 1 %:';
recall that Tokio does not admit that it backtracks to % t sub 0 %).
At this point, we have backtracked back in time to the first call to \fCloop\fR
and the recursive \fCloop\fR subgoal after the \fC&&\fR in this call is
satisfied by the nonrecursive (the second) \fCloop\fR clause. If we force 
another failure, there is no other way for the recursive \fCloop\fR subgoal 
to succeed, and so the entire query fails.
.IP "" 10
\fCb4:
.ls 1
.IP "" 10
\fCb3:
.IP "" 10
\fCb2:
.IP "" 10
\fCb1: 
.IP "" 10
\fC-- fail --\fR
.ls 2
.MH 3 "\fCwhile\fP"
The general scheme illustrated by \fCloop\fR, where time is driven forward
by recursion after a \fC&&\fR and is halted when a condition is nolonger
satisfied, could be encoded as follows:
.ls 1
.IP "" 10
.ft C
.nf
loop(Cond, Body):- if Cond
		      then Body && loop(Cond, Body).
.fill
.sp
.ls 2
.ft R
.LP
In fact, Tokio has a \fCwhile\fR operator that does much the same as the 
more general \fCloop\fR. A goal of the form
.IP "" 10
\fCwhile C do B\fR
.LP
is parsed as
.IP "" 10
\fCwhile (C do B)\fR
.LP
In fact, \fCdo\fR itself is an infix operator, so the parse tree is
.IP "" 10
.KS 
.sp
.PS < fig45
.sp
.KE
.LP
\fCWhile\fR is defined as 
.ls 1
.IP "" 10
.ft C
.nf
(while Cond do Body):- if Cond
                          then Body && while Cond do Body
                          else empty.
.fill
.sp
.ls 2
.ft R
.LP
This differs from the definition we give of the general \fCloop\fR in that
it combines an \fCelse\fR clause: when Cond fails, this definition requires
that \fCempty\fR succeed. \fCEmpty\fR will succeed if the current time is
at the end of an interval. If the interval is closed, \fCempty\fR is already
true; if it is open-ended, \fCempty\fR may be made true. So \fCwhile\fR 
must finish at the end of an intervaland will close off the interval if it
is open-ended.
.MH 3 "\fCwhile\fP and Backtracking"
Unfortunately, \fCempty\fR is not properly implemented in the current version
of Tokio. A subgoal \fCempty\fR always succeeds and, when backtracking
encounters a subgoal \fCempty\fR, it goes into an infinite loop, advances
from one time to the next. Consequently, backtracking goes into the same
infinite loop when it encounters a \fCwhile\fR. Thus \fCwhile\fR should be
avoided. Nevertheless, we shall include a few additional remarks, hoping
that the bugs will soon be repaired.
.MH 3 "Nested \fCwhile\fP's and \fCif\fP's"
\fCwhile\fR has a precedance similar to that of \fCif\fR, so parentheses
are rarely needed within the condition or the body goals. Still, curly brackets
(\fC{...}\fR) surrounding these goals may improve readability. As with the goals
in a conditional, the condition and the body goals may be arbitrarily complex
and may include temporal operators. \fCWhile\fR structures may be nested in the 
obvious way. Thus,
.IP "" 10
\fCwhile C1 do while C2 do B\fR
.LP
is parsed as
.IP "" 10 
\fCwhile C1 do (while C2 do B)\fR
.LP
\fCWhile\fRs and conditionals may be nested together without much fear of 
violating syntax. Thus,
.IP "" 10 
\fCwhile C1 do if C2 then T else E\fR
.LP 
is parsed as 
.ls 1
.IP "" 10
.ft C
.nf
while C1
  (if C2
      then T
      else E
  )
.fill
.sp
.ls 2
.ft R
.LP
and
.IP "" 10 
\fCif C1 then while C2 do B1 else while C3 do B2\fR
.LP 
is parsed as 
.ls 1
.IP "" 10
.ft C
.nf
if C1
   then (while C2
            do B1
        )
   else (while C3 
            do B2
        ) 
.fill
.sp
.ls 2
.ft R
.MH 2 "Summary"
.CB "Static Variables"
.MH 1
.PP
In Prolog, \fCassert\fR is used to record a result reached in 
evaluating a clause so that it is available when other clauses are
later evaluated.  On the other hand, \fCretract\fR is used so that
an axiom (fact or rule) available when
one clause is evaluated is no longer in force when other clauses
are later evaluated.  The combination of \fCretract\fR and \fCassert\fR
may be used to modify the contents of the
database, that is, the set of axioms, in midcourse.  In general,
\fCassert\fR and \fCretract\fR are used for their side effects.  However,
\fCassert\fR and \fCretract\fR do not have their usual utility in Tokio.
This is because Tokio is compiled, that is, the contents of the database when
a Tokio program is executed is the output of the Tokio compiler.  If something
was not in the file given as input to the Tokio compiler, then it is
unknown to the compiled Tokio program.  Likewise, retracting
something at run-time does not do away with its image in the compiled code,
and so has no effect on run-time behavior.
.PP
Regarding the ability to make use of side effects, however, Tokio more than 
compensates for the loss of \fCassert\fR and \fCretract\fR by allowing global
and static variables.  These may often be thought of in analogy with
literals asserted into the database and modified by combinations of \fCretract\fR
and \fCassert\fR.  However, it is not so much the global and static
variables themselves that are of interest as it is their values.  Because of
this and because such variables serve as persistent stores for values, they are
similar to variables in imperative languages such as Pascal and FORTRAN.
.MH 2 "Assigning and Referencing Values"
.PP
We describe 
static variables here. 
The present implementation does not distinguish
global variables from static ones. A static variable retains its value until
explicitly changed; it thus behaves like storage. The 
operator \fC*\fR creates a static variable. The \fC:=\fR
operator is used to assign a value (to the right of \fC:=\fR)
to a static variable (to the left); thus for example, \fC*s := 1\fR
assigns the value \fC1\fR to the static variable \fC*s\fR.
Efficiency is improved if static variables are declared.
If %s sub 1%, %s sub 2%, and %s sub 3% are static variables, then 
they are declared as such with the fact (usually put at the top of the
program static([%s sub 1%, %s sub 2%, %s sub 3%])).
.PP
A static variable may not be used as an argument in a subgoal.
More exactly, suppose, for example, we have a clause with
head \fCfoo(s)\fR and suppose the subgoal \fCfoo(s)\fR
occurs somewhere in the body of another clause. Then, when
\fCfoo(*s)\fR is evaluated, \fCs\fR is bound to \fC*s\fR, and not
to the value of \fC*s\fR. Thus, in place of
.IP "" 10
\fCwrite(*s)\fR
.LP
one must use something like
.IP "" 10
\fCS = *s, write(S)\fR
.LP
Note that \fC=\fR is used to bind a logical (i.e. normal)
variable to the value of a static variable. It has no effect on
the value of the static variable. In particular, if \fC*s\fR has no
value, evaluation of \fC*s = 1\fR leaves \fC*s\fR with no value.
.PP
Consider the following program:
.IP "" 10
.ls 1
\fCt:- in && out.
.IP "" 10
\fCin:- *s := 1.
.IP "" 10
\fCout:- S = *s, write(S).\fR
.ls 2
.LP
When \fCt\fR is evaluated, \fCin\fR is evaluated at % t sub 0 %,
and so \fC*s\fR is assigned the value \fC1\fR at % t sub 0 %. Then
\fCout\fR is evaluated at %t sub 1 %, so \fCS\fR is bound to the value
of \fC*s\fR, namely, \fC1\fR, and \fC1\fR is output at %t sub 1 %. If \fCout\fR
were defined rather as
.IP "" 10
\fCout:- write(*s).\fR
.LP
then, at %t sub 1 %, \fC*s\fR, not \fC1\fR, would be output. Suppose the
definition of \fCout\fR were replaced by
.IP "" 10
\fCout:- S = *s, incr(S, S1), write(S1).\fR
.LP
Suppose \fCincr\fR is defined by
.IP "" 10
\fCincr(In, Out) :- Out = In + 1.\fR
.LP
Then, at %t sub 1 %, \fCS\fR, is bound to \fC1\fR (the value of \fC*s\fR),
evaluation of \fCincr(S, S1)\fR results in \fCS1\fR being bound to \fC2\fR, and
\fC2\fR is output. If \fCout\fR were defined rather as
.IP "" 10
\fCout:- incr(*s, S1), write(S1).\fR
.LP
then, at %t sub 1 %, the system would attempt to evaluate \fC*s + 1\fR, 
resulting in an error because \fC*s\fR (as opposed to its value) is not
numerical.
.PP
Even though a static variable may not be used as an argument in a
predicate, it may be an argument in an arithmetic expression (as long,
of course, as it has a numerical value).  Consider, for example, the
following program:
.ls 1
.IP "" 10
.ft C
.nf
t :- *s := 0, loop(5), #{ S = (s= *s), write(S)}.

loop(Limit) :- *s < Limit,
		   @(*s := *s + 1)
	       && loop(Limit).
loop(_).
.fill
.sp
.ls 2
.ft R
.LP
Tokio is able to evaluate the arithmetical expressions \fC*s < Limit\fR and
\fC*s + 1\fR.  Note in particular the assignment
.IP "" 10
\fC*s := *s + 1\fR
.LP
Thus, as in imperative language, a static variable may be updated to a value
that is a function of its current value.  Note how the value of \fC*s\fR is
identified in the output produced by \fCt\fR.  The goal \fCS = (s= *s)\fR
binds \fCS\fR to two elements: the atom \fCs=\fR and the value of \fC*s\fR.
Suppose the value of \fC*s\fR is \fC3\fR. Then the subgoal \fCwrite(S)\fR will
output \fCs=3\fR. The \fCloop\fR predicate here is like the \fCloop\fR
predicates we considered earlier: the first clause consists of a condition 
(\fC*s < Limit\fR), a body (\fC@(*s := *s + 1)\fR), and a recursive call to itself after
the chop. (The chop and recursive call combination drives the loop forward in
time.) The second \fCloop\fR clause allows a call to \fCloop\fR to succeed
when the condition in the first clause becomes false. Here the predicate \fCt\fR
initializes the static variable \fC*s\fR to \fC0\fR at %t sub 0%, calls \fCloop\fR
with \fCLimit\fR bound to \fC5\fR, and outputs the value of \fC*s\fR for all times. 
The body of \fCloop\fR increments \fC*s\fR in the next time so that each
recursive call of \fCloop\fR sees a value for \fC*s\fR one larger than that
seen by the current call. The result is that \fC*s\fR has the value \fCi\fR for
time %t sub i%, \fC0 \(<= i \(<= 5 = Limit\fR.
.MH 2 "Instantaneous vs. Temporal Assignment: \fC:=\fP and \fC<=\fP"
.PP
A static variable as updated by the instantaneous assignment operator, \fC:=\fR,
acts as an individual latch that can be read immediately by any predicate.
There is also a temporal assignment operator, \fC<=\fR. The effect of, say,
.IP "" 10
\fC*s <= 1\fR
.LP
appears at the end of the current interval. Thus a static variable as updated
by the temporal assignment operator acts as a common bus memory; the memory 
unit is considered a remote device. The same static variable may be assigned
values by using \fC:=\fR at one time and using \fC<=\fR at another.
.PP
Before we present our simple example of the use of the temporal assignment
operator, we must describe what happens when a static variable without a
value is referenced. Suppose \fC*s\fR has no value and the subgoal \fCS = *s\fR
is evaluated. Then Tokio will print the message
.IP "" 10
\fCReference not assigned value -- s1\fR
.LP
For example, suppose \fCt\fR is defined as 
.IP "" 10
\fCt :- (true && *s1 := 1), #(S = *s1, write(S)).\fR
.LP
Evaluation of \fCt\fR will result in the output
.IP "" 10
.ls 1
\fCt0:
.IP "" 10
\fCReference not assigned value -- s1
.IP "" 10
\fC_188
.IP "" 10
\fCt1:1\fR
.ls 2
.LP
The \fC_188\fR output at %t sub 0% represents the unbound variable \fCS\fR in 
\fCwrite(S)\fR. The reference to \fC*s1\fR that produced the message at
%t sub 0% is the reference in \fCS = *s1\fR.
.PP
Now, as an example of the use of the temporal assignment operator, consider
.IP
\fCt :- length(3), { length(2), *s1 <= 1 && true }, #{ S = *s1, write(S)}.\fR
.LP
When \fCt\fR is evaluated, the main interval of length three is chopped into
an initial interval of length two followed by an interval of length one. The
\fC*s1 <= 1\fR subgoal is evaluated in the first interval, at %t sub 0%, but
the assignment does not take effect until the end of this interval, at
the end of %t sub 1%. Thus the value 1 cannot be accessed as the value of
\fC*s1\fR until %t sub 2%. Thus, when \fCt\fR is evaluated, the following output
results:
.IP "" 10
.ls 1
\fCt0:
.IP "" 10
\fCReference not assigned value -- s1
.IP "" 10
.IP "" 10
\fCt1:
.IP "" 10
\fCReference not assigned value -- s1
.IP "" 10
.IP "" 10
\fCt2: 1\fR
.ls 2
.PP
Temporal assignment allows one to delay the change in the value of a
static variable when the future value is already known. Thus the current
value may be retrieved throughout the remainder of the present interval. In
the next interval, the new value is retrieved when the static variable is
accessed. Consider, for example, the following program:
.ls 1
.IP "" 10
.nf
.ft C
t :- length(4), #{ S = (s1= *s1, s2= *s2, s3= *s3), write(S)},
     {             (length(1), *s1 := 1)
             && (length(2), *s1 <= 2, @(*s2 := *s1 + 1, @(*s3 := *s1 + 2)))
             && length(1)
     }.
.fill
.sp
.ls 2
.ft R
.LP
When \fCt\fR is evaluated, the following subgoals are evaluated at the 
indicated time points:
.IP "" 10
.ls 1
\fCt0: *s1 := 1
.IP "" 10
\fCt1: *s1 <= 2
.IP "" 10
\fCt2: *s2 := *s1 + 1
.IP "" 10
\fCt3: *s3 := *s1 + 2
.IP "" 10
\fCt4: \(em nothing \(em\fR
.ls 2
.LP
Note that the present interval <%t sub 0% %t sub 1% %t sub 2% %t sub 3%
%t sub 4%> is divided into subintervals <%t sub 0% %t sub 1%>, <%t sub 1%
%t sub 2% %t sub 3%>, and <%t sub 3% %t sub 4%>.  Thus, because of 
\fC*s1 := 1\fR, \fC*s1\fR has the value \fC1\fR at the end of %t sub 0%. Because
of \fC*s1 <= 1\fR and the fact that %t sub 1% is a point in the interval
ending at %t sub 3%, \fC*s1\fR's value does not change to \fC2\fR until the end
of %t sub 3%. Thus the subgoals evaluated at %t sub 2% and %t sub 3% access
the value \fC1\fR for \fC*s1\fR. Thus \fC*s2\fR is assigned \fC2\fR at the end of %t sub 2%
and \fC*s3\fR is assigned \fC3\fR at %t sub 3%.
.PP
The instantaneous assignment operator \fC:=\fR causes assignement at the \fCend\fR
of the time point at which it is evaluated, after evaluation of any \fC=\fR
subgoals at that point. The output, therefore, lags one time point behind the
effects of instantaneous assignments. Thus the output when the \fCt\fR 
predicate defined above is evaluated is (where unassigned-variable messages
have been suppressed and \fC_1\fR, for example, indicates an unbound variable):
.IP "" 10
.ls 1
\fCt0: s1 = _1, s2 = _2, s3 = _3
.IP "" 10
\fCt1: s1 =  1, s2 = _4, s3 = _5
.IP "" 10
\fCt2: s1 =  1, s2 = _6, s3 = _7
.IP "" 10
\fCt3: s1 =  1, s2 =  2, s3 = _8
.IP "" 10
\fCt4: s1 =  2, s2 =  2, s3 =  3\fR
.ls 2
.PP
A static variable may be assigned more than one value at one time point.
In that case, the last value assigned is the value the variable has
after that point. For example, the sequence
.IP "" 10
\fC*s := 1, *s := 2\fR
.LP
will result in \fC*s\fR having the value \fC2\fR at the end of the current time point,
and
.IP "" 10
\fC*s <= 1, *s <= 2\fR
.LP
will result in \fC*s\fR having the value \fC2\fR at the end of the current interval.
If,
.IP "" 10
\fC*s <= 1, *s := 2\fR
.LP
is evaluated at the last point in an interval, then \fC*s\fR will have the 
value \fC1\fR at the end of the point and the interval. This is because a
temporal assignment always takes effect after an instantaeous assignment
evaluated at the same time.
.MH 2 "Relation between Static and Logical Variables"
.PP
If a normal variable is assigned to a static variable, and the
normal variable is then bound to a value at the same time point,
then the static variable gets this same value.  For example, evaluating
.IP "" 10
\fC*s := Z, Z = 1\fR
.LP
causes \fC1\fR to be stored in \fC*s\fR. However, an attempt to store a $t-list
in a static variable results in only the first element of the $t-list
being stored. For example, evaluating
.IP "" 10
\fCZ = 1, @ Z = 2, *s := Z\fR
.LP
results in 1 being stored in \fC*s\fR, even though the value \fCZ\fR is
\fC$t(1, $t(2, _))\fR. Thus, with respect to temporal variables, '\fC:=\fR'
behaves like '\fC=\fR' in that the unification is at the current time only, not (as
when a goal matches the head of a clause) over all time. If we later evaluate
.IP "" 10
\fCS = *s, #write(S)\fR
.LP
the value \fC1\fR will be output for the current and all subsequent times. The
operator '\fC:=\fR' is unlike '\fC=\fR', however, in that static variables cannot
be made to share. For example, if
.IP "" 10
\fC*s := [X, 2, 3]\fR
.LP
is evaluated, and then, in a different clause,
.IP "" 10
\fC[X, 2, 3] = *s, X = 1\fR
.LP
is evaluated, the first element in the list stored in \fC*s\fR remains
uninstantiated.
.MH 2 "Static-Variable Assignment and Backtracking"
.PP
Unlike \fCassert\fR and \fCretract\fR, the effects of instantaeous and
temporal assignments are undone by backtracking, whether the backtracking is
done in current time or into the past. Consider, for example:
.IP "" 10
.ls 1
\fCt:- *s := 1, fail.
.IP "" 10
\fCt:- S = *s, write(S).\fR
.ls 2
.LP
When \fCt\fR is evaluated, the first clause is chosen, so \fC*s\fR is
assigned a \fC1\fR. The \fCfail\fR causes the first clause to fail, so the
second clause is chosen, and the value of \fC*s\fR is bound to \fCS\fR
and output. Since backtracking over the \fC*s = 1\fR subgoal (which cannot be
resatisfied) undoes its effct, an unbound variable value is output.
Next consider:
.ls 1
.IP "" 10
.ft C
.nf
t :- length(2),
     {       *s <= 1,
       && skip
       && S = *s, write(S), fail
     }.
t :- length(2), #{S = *s, write(S)}.
.fill
.sp
.ls 2
.ft R
.LP
When \fCt\fR as thus defined is evaluated, the first clause is chosen. 
At % t sub 0 %, the \fC*s <= 1\fR subgoal is evaluated. This is done in the 
interval < %t sub 0 % % t sub 1 % >. Thus at % t sub 2 %, when
.IP "" 10
\fCS = *s, write(S), fail\fR
.LP
is evaluated, \fC*s\fR has the value \fC1\fR, which is output. But the \fCfail\fR is
encountered, which forces the system to backtrack into the past. At % t sub 2 %
and % t sub 1 %, no resatisfiable goals are found. So the system returns 
to %t sub 0 %. Since \fC*s <= 1\fR cannot be resatisfied, the second
clause is chosen. Evaluation then proceeds forward in time through %t sub 0 %,
% t sub 1 % and % t sub 2 %. At each point, the value of \fC*s\fR is output.
Since backtracking undoes the effect of \fC<=\fR, at each point, including
% t sub 2 %, an unbound variable value is output.
.MH 2 "Static Variables as Arrays"
.PP
Static variables may have arguments, and hence act like arrays. For example,
suppose \fCt\fR is defined by
.ls 1
.IP "" 10
.ft C
.nf
t :- init && out.
.sp
init :- *g(1,1) := 1, *g(1,2) := 2,
          *g(2,1) := 3, *g(2,2) := 4.
.sp
out :- G11 = *g(1,1), G12 = *g(1,2),
          G21 = *g(2,1), G22 = *g(2,2),
          write((G11,G12,G21,G22)).
.fill
.sp
.ls 2
.ft R
.LP
When \fCt\fR is evaluated, at % t sub 1 % Tokio will output
.IP "" 10
\fC1,2,3,4\fR
.LP
Here \fC*g\fR acts like a two-by-two array.
.PP
We may thus write programs that loop over the elements of arrays of several
dimensions. For example, consider:
.ls 1
.IP "" 10
.ft C
.nf
t(Rs, Cs) :-
	*cols := Cs, init(1, 1, Rs, Cs), nl,
	out(1, 1, Rs, Cs).

init(I, J1, In, Jn) :-
	I =< In, !,
	init1(I, J1, Jn), I1 = I + 1,
	init(I1, J1, In, Jn).

init(_,_,_,_).

init1(I, J1, Jn) :-
	J <= Jn, !,
	*g(I, J) := (I - 1) * *cols + J,
	J1 = J + 1,
	init1(I, J1, Jn).
init1(_,_,_). 

out(I, J, In, Jn) :- 
	I <= In, !,
	out1(I, J1, Jn), nl, I1 = I +1,
	out(I1, J1, In, Jn). 

out(_,_,_,_). 

out1(I, J, Jn) :-
	J <= Jn, !,
	K = *g(I,J), tab(3), write(k),
	J1 = J + 1,
	out1(I, J1, Jn).

out1(_,_,_).
.fill
.sp
.ls 2
.ft R
.LP
The program produces the following output (which we have prettied slightly
to align coulmns), when \fCt(4,6)\fR is evaluated:
.ls 1
.IP "" 10
.ft C
.nf
	t0:
	  1     2    3    4    5    6
	  7     8    9   10   11   12
	  13   14   15   16   17   18
	  19   20   21   22   23   24
	t1:
.fill
.sp
.ls 2
.ft R
.LP
\fCt(R\fRs, \fCC\fRs) computes in row-major form the integers from \fC1\fR to \fCRs*C\fRs and
stores these values in the \fCR\fRs-by-\fCC\fRs array \fC*g(I, J)\fR. The
first \fCC\fRs positive integers are stored in row 1, the second \fCC\fRs
are 
stored in row 2, etc. It then outputs the contents of \fI*g(I, J)\fR, one row
per output line. Predicate \fCt\fR first evaluates \fC*col\fRs \fC:=\fR \fCC\fRs
so that the number of columns is later available as the value of \fC*col\fRs.
It then evaluates \fCinit(1, 1, R\fRs\fC, C\fRs\fC)\fR, which stores values in array
\fC*g(I, J)\fR. Predicate \fCinit\fR loops over rows and evaluates \fCinit1(I, J1, Jn)\fR
for each row \fCI\fR, \fC1 \(<= I \(<= R\fRs. Predicate \fCinit1\fR, for
a given row \fCI\fR, loops over the columns \fCJ\fR, \fC1 \(<= J \(<= C\fRs. For
each column \fCJ\fR, it computes the value of \fC*g(I, J)\fR as
.IP "" 10
\fC*g(I, J) := (I - 1) * *cols + J\fR
.LP
The last thing \fCt\fR does is evaluate \fCout(1, 1, R\fRs\fC, C\fRs\fC)\fR, which
outputs the contents of the array.  Structually, \fCout\fR is like \fCinit\fR,
looping over rows and evaluating \fCout1\fR (and analogous to \fCinit1\fR) to loop
over columns. The sequence of subgoals in \fCout1\fR responsible for output
is
.IP "" 10
\fCK = *g(I, J), tab(3), write(K)\fR
.PP
It is difficult to make \fCt\fR as defined above more general. The best we can
do is write a predicate to compute array values, say
.IP "" 10
\fCf1(I, J, Res) :- Res = (I - 1) * *cols + J.\fR
.LP
Then, to compute array elements differently, one redefines \fCf1\fR. One is
tempted to add another argument to \fCt\fR, \fCinit\fR, and \fCinit1\fR, say
\fCFunc\fR, to be bound to the functor of the predicate computing array values.
The intent would be to use \fCuniv\fR to construct the subgoal computing the
array element:
.IP "" 10
\fCGoal =.. [Func, I, J, K], call(Goal), *g(I, J) := K\fR
.LP
The problem with this is that \fCGoal\fR is constructed at run-time and
the predicate whose functor, say \fCf1\fR, is bound to \fCFunc\fR is compiled, and so
is in a form different from the \fCf1\fR predicate originally written. For the
same reason, it is not possible to add an argument, say \fCArray\fR, and
construct an array-assignment goal such as
.IP "" 10
\fCGoal1 =.. [Array, I, J], Goal2 =.. [':=', Goal1, K], call(Goal2)\fR
.LP
Thus we must be satisfied with predetermined array name predicates for
computing element values. However, this does allow us to keep several
distinct global memories.
.PP
A static variable may be used with different numbers of indices. For example,
we could have
.IP "" 10
\fC*s(1) := 1, *s(1, 1) = 2\fR
.LP
An alternative to using array notation is to store a list (possibly of lists) in
a scalar static variable. Thus, instead of
.IP "" 10
\fC*s(1, 1) := 1, *s(1, 2) := 2, *s(2, 1) := 3, *s(2, 2) := 4, *s(3, 1) := 5, *s(3, 2) := 6\fR
.LP
we could use 
.IP "" 10
\fC*s := [[1, 2], [3, 4], [5, 6]]\fR
.LP
To output, for example, the element in the second row, first column, we would
use 
.IP "" 10 
\fC[_, [X, _], _] = *s, write(X)\fR 
.LP 
The structure used to implement arrays need not be lists. For example, we could use 
.IP "" 10 
\fC*s := ((1, 2), (3, 4), (5, 6))\fR 
.LP 
and then 
.IP "" 10 
\fC(_, (X, _), _) = *s, write(X)\fR 
.LP 
Hybrids between array and structure notation are possible. Thus, for what is conceptually a three-dimensional array, we could have 
.IP "" 10 
\fC*g(1, 2) := [a, b, c]\fR 
.LP 
and output one element with 
.IP "" 10
\fC[_, X, _] = *g(1, 2), write(X)\fR
.PP
The indices themselves may be structures, thus allowing a sort of associative
memory. Thus we could store distances, both by air and by car, between cities with
.ls 1
.IP "" 10
.ft C
.nf
*distance( air( detroit, miami)) := 1100,
*distance( car( detroit, miami)) := 1300,
*distance( air( detroit, boston)) := 700,
*distance( car( detroit, boston)) := 900
.fill
.sp
.ls 2
.ft R
.LP
To output the distance by car between Detroit and Miami, we would use
.IP "" 10
\fCD = *distance( car( detroit, miami)), write(D)\fR
.LP
Lists may be used as indices. Suppose, for example, we are simulating
a very simple computer with four-bit memory addresses and eight-bit memory
words; we represent a binary number by a list of \fC0\fR's and \fC1\fR's.  Then, to
store
the value \fC2\fR at address \fC2\fR, we would use
.IP "" 10
\fC*mem([0,0,1,0]) := [0,0,0,0,0,0,1,0]\fR
.LP
An index can even be another static variable. For example, to store the
contents of the data buffer register (DBR) at the address in memory
stored in the memory address register (MAR), we could use
.IP "" 10
\fC*mem(*mar) := *dbr\fR
.PP
When an assignment is made, an index may be a variable. This has the effect
of assigning the same value to an entire family of array cells. For example,
evaluation of
.IP "" 10
\fC*mem(0,_,1) := foo\fR
.LP
followed by evaluation of
.IP "" 10
\fCM1 = *mem(0,1,1), M10 = *mem(0,10,1), M = *mem(0,_,1), write((M1, M10, M))\fR
.LP
results in the output
.IP "" 10
\fCfoo, foo, foo\fR
.PP
The reverse technique, however, is not useful. That is, suppose values
are assigned to array elements whose indices are fully specified, for
example,
.IP "" 10
\fC*s(1) := 11, *s(2) := 12\fR
.LP
Then an array reference \fC*s(X)\fR will retrieve the last value assigned to
an array element of the form \fC*s(_)\fR. For example,
.IP "" 10
\fCW = *s(X)\fR
.LP
binds \fCW\fR to \fC12\fR, and
.IP "" 10
\fC11 = *s(X)\fR
.LP
fails since it attempts to unify \fC11\fR and \fC12\fR.
.PP
However, a related technique is useful. Suppose a partially instantiated
structure is assigned to a family of array cells by virtue of the fact
that a variable index is used, for example
.IP "" 10
\fC*s(1,_) := (a,_)\fR
.LP
The structure may be retrieved, uninstantiated parts may be instantiated in
various ways, and the results may be stored in members of the family of
array cells that originally contained the partially instantiated structure.
Given the above assignment, we may fill out the structure \fC(a, _)\fR
differently for elements \fC*s(1,1)\fR and \fC*s(1,2)\fR:
.IP "" 10
\fC(X,_) = *s(1,1), *s(1,1) := (X, b)\fR
.LP
and
.IP "" 10
\fC(X,_) = *s(1,2), *s(1,2) := (X, c)\fR
.LP 
This technique allows for progressive differentiation of array elements and
their contents.
.MH 2 "Summary"
.CB "Macros"
.MH 1
.PP
Tokio has a macro facility that allows functions and relations to be defined so
that uses of these functions and relations are expanded in line in the clauses in which
they appear. We here first discuss functions, and then turn to relations defined as macros.
.MH 2 "Defining and Applying Functions: \fC$function\fP"
.PP
A function definition is introduced by the keyword \fC$function\fR and is
terminated with a full stop. It has the form
.IP "" 10
.ls 1
\fC$function <expression in %X sub 1%, ..., %X sub n%> = <return value, Z> :-\fR
.IP "" 10
\fC                         <goal sequence in %X sub 1%, ..., %X sub n% determining Z>.\fR
.ls 2
.LP
Here the variables %X sub 1%, ..., %X sub n% are variables that may be thought of as
the formal parameters of the function. The variable \fCZ\fR gets bound to the 
function value. Normally, the expression to the left of the '\fC=\fR' is the function
name with the formal parameters as arguments, so the head of the defining clause
has the form
.IP "" 10
\fC<function name> (%X sub 1%, ..., %X sub n%) = Z\fR
.MH 3 "Function Applications that Return Values"
One way in which a function may be applied within a clause is as one term in
an equality expression:
.IP "" 10
\fC .... :- ..., <expression in %a sub 1%, ..., %a sub n%> = Z,...\fR
.LP
Here %a sub 1%, ..., %a sub 2% may be variables or constants. The most common
form for the expression to take is
.IP "" 10
\fC<function name> (%a sub 1%, ..., %a sub n%)\fR
.LP
For example, the following function increments its argument by one:
.IP "" 10
\fC$function incr(I) = I1  :-  I1 = I + 1.\fR
.LP
Suppose \fCincr\fR is applied in the definition of \fCt\fR:
.IP "" 10
\fCt(X) :- incr(X) = W, write(W).\fR
.LP
(Note that the order of \fCincr(X)\fR and \fCW\fR is immaterial.)
Then the compiler replaces \fCincr(X) = W\fR with its definition to give what
would have resulted if \fCt\fR had been defined by
.IP "" 10
\fCt(X) :- W = X + 1, write(W).\fR
.PP
As a second example, suppose function \fCfoo\fR is defined by 
.IP "" 10
\fC$function foo(I,J) = I1 :- g(I,X), h(J,Y), I1 = X + Y.\fR
.LP
We assume \fCg\fR and \fCh\fR are defined by their own clauses, say
.IP "" 10
.ls 1
\fCg(1,1).
.IP "" 10
\fCg(2,2).
.IP "" 10
.IP "" 10
\fCh(1,2).
.IP "" 10
\fCh(2,1).\fR
.ls 2
.LP
Now suppose \fCfoo\fR is used in
.IP "" 10
\fCt :- X = foo(1,2), write(X).\fR
.LP
Then the compiler uses the definition of \fCfoo\fR to expand \fCX = foo(1,3)\fR, in
effect giving
.IP "" 10
\fCt :- g(1,X1), h(2,Y), X = X1 + Y, write(X).\fR
.PP
Functions may also appear in arithmetical expressions, for example,
.IP "" 10
\fC3 + foo(1,1) * foo(2,2) > incr(2)\fR
.LP
Given the above definitions of \fCincr\fR and \fCfoo\fR, this is expanded to
.IP "" 10
.ls 1
\fCg(1,X1), h(1,Y1), I1 = X1 + Y1,
.IP "" 10
\fCg(2,X2), h(2,Y2), I2 = X2 + Y2,
.IP "" 10
\fCI3 = 2 + 1,
.IP "" 10
\fCI4 = 3 + I1 * I2,
.IP "" 10
\fCI4 > I3\fR
.ls 2
.LP
Again, a function expression may occur as the argument of a predicate or even
as the argument of another function. For example, 
.IP "" 10
\fCwrite(incr(foo(2,1)))\fR
.LP
is expanded to
.IP "" 10
\fCg(2,X), h(1,Y), I1 = X + Y, I2 = I1 + 1, write(I2)\fR
.PP
It is sometimes beneficial to declare an operator that is then given a
meaning in one or more function definitions. Consider, for example, the
following
.IP "" 10
.ls 1
\fC:- op(100, xfy, '::').
.IP "" 10
.IP "" 10
\fC$function  X::first  = U :-   X = (U,V,W).
.IP "" 10
\fC$function  X::second = V :-   X = (U,V,W).
.IP "" 10
\fC$function  X::third  = W :-   X = (U,V,W).\fR
.ls 2
.LP
Here three zero-ary functions, \fCfirst\fR, \fCsecond\fR, and \fCthird\fR, are
defined. They occur as the right operands of the infix operator \fC::\fR ; these
function definitions may thus be viewed as defining the meaning of \fC::\fR . Note
that the left operand of \fC::\fR is expected to be a structure of the form
\fC(U,V,W)\fR. If the left operand is not of this form, then an attempt to evaluate one
of the functions \fCfirst\fR, \fCsecond\fR, or \fCthird\fR results in failure.
Function \fCfirst\fR simply returns the first element in a structure of the
form \fC(U,V,W)\fR; \fCsecond\fR and \fCthird\fR return the second and third elements,
respectively.
.LP
Now consider the clause
.IP "" 10
\fCt :- A = (2,4,6), W = 2 * A::first + 3 * A::second - A::third, write(W).\fR
.LP
The Tokio compiler is smart enough to rewrite this (in light of the definitions
of \fCfirst\fR, \fCsecond\fR, and \fCthird\fR) as
.IP "" 10
\fCt :- W = 2 * 2 + 3 * 4 - 6, write(W).\fR
.PP
Predefined operators can also be exploited. Consider, for example,
.IP "" 10
.ls 1
\fC$function (if Cond then Yes else No) = Reply :-\fR
.IP "" 10
\fC                   if Cond then Yes = Reply else No = Reply.\fR
.ls 2
.LP
Suppose this functional expression is used in
.IP "" 10
\fCt :- g(1,X), g(2,Y), write(if Y>X then 1 else 0).\fR
.LP
(We assume that \fCg\fR is defined as above.) The compiler expands this to:
.ls 1
.IP "" 10
.ft C
.nf
t :- g(1,X), g(2,Y),
     {if Y > X then 1 = Reply else 0 = Reply},
     write(Reply).
.fill
.sp
.ls 2
.ft R
.MH 3 "Function Definitions as Conditional Equalities"
We have thus far thought of functions largely in terms of expressions that
are evaluated to produce return values. It should be kept in mind, however,
that the function facility in Tokio is a macro facility that expands expressions
in accordance with what may be viewed as conditional equations. For a function
definition
.IP "" 10
\fC$function LHS = RHS :- condition\fR
.LP
states that the left hand side (\fCLHS\fR) of the equation may be replaced by the
right hand side (\fCRHS\fR) if the goal \fCcondition\fR succeeds. Bindings made
to \fCLHS\fR are in force when \fCcondition\fR is evaluated, and bindings
established by this evaluation are in force when \fCRHS\fR replaces \fCLHS\fR.
Alternatively, if the function is applied as part of an equation,  it is possible
for \fCRHS\fR and \fCLHS\fR both to have bindings, since the head of the function
definition (i.e. the entire equality) then matches the equality constituting
the function application. Further bindings may then be imposed on either
\fCLHS\fR or \fCRHS\fR as a result of evaluating \fCcondition\fR.
.PP
As an example, suppose we have a relation \fCnth(N,List,Element)\fR, whose logical
reading is : \fCElement\fR is the \fIN\fRth element in list \fCList\fR (where
the head of \fCList\fR is considered the zeroth element). This may be defined
by 
.IP "" 10
.ls 1
\fCnth(0, [H|T], H) :- !.
.IP "" 10
\fCnth(N, [H|T], H1) :- N1 = N - 1, nth(N1,T,H1).\fR
.ls 2
.LP
Now, in general, if we have a relation \fCf\fR in \fIn\fR variables and,
for each tuple of values for the first \fIn-1\fR variables, there is at most
one value for the \fIn\fRth variable, then we may regard \fCf\fR as a function
in the first \fIn\fR-1 variables whose function value is the value of the
\fIn\fRth variable. The relation \fInth\fR meets these requirements, so it
makes sense to define
.IP "" 10
\fC$function nth(N,L) = E :- nth(N,L,E).\fR
.LP
Now notice that, in the definition of the relation \fCnth\fR, arithmetic is
performed on the first argument, so this argument must be an input argument.
Also, the second argument is most naturally used as an input argument, leaving
the third as the only natural output argument. Thus a typical use of the 
\fCfunction\fR \fCnth\fR would be, for example,
.IP "" 10
\fCnth(2,L) = E\fR
.LP
where \fCL\fR is bound to a list and \fCE\fR is unbound. This would be
translated into
.IP "" 10
\fCnth(2,L,E1), E1 = E\fR
.LP
and, when evaluated, would bind \fCE\fR to the value of the second element in
list \fCL\fR. But suppose the second element in \fCL\fR is an unbound variable
and \fCE\fR is bound to some value. Then the above would bind the second element
of \fCL\fR for this value. In this case,
.IP "" 10
\fCnth(2,L) = E\fR
.LP
would not fit the paradigm of a function expression that evaluates to a value,
to which \fCE\fR is then bound. Rather, it would conform to the more general
paradigm of unifying the two sides of an equation.
.MH 3 "Function Applications and Temporal Operators"
Finally, functions may be used together with temporal operators. As an example,
consider again the function \fCnth\fR discussed in the last paragraph, and suppose
we have
.IP "" 10
\fC@nth(2,L) = E\fR
.LP
This is expanded to 
.IP "" 10
\fCnth(2,L,E1), @E1 = E\fR
.LP
Suppose again that the second element of list \fCL\fR is an unbound variable
and that \fCE\fR is bound to a value. Then the effect of the above is to make the
value of the second element in \fCL\fR at the next time point equal to the current
value of \fCE\fR.
.MH 2 "Defining and Invoking Macro Relations: \fC$define\fP and \fC$clause\fP"
.PP
Definitions of relation macros are introduced by the keyword \fC$define\fR.
Relation macros may be used to save the expense of extra calls (as macros are
used in LISP).  They are also convenient in that relation macros, unlike normal
relations or predicates, may take static variables as arguments.
We illustrate this latter point after discussing how relation macros are defined
and used in general.
.MH 3 "Simple Form: \fC$define\fP without \fC$clause\fP"
In its simplest form, a relation macro definition consists of a single clause
introduced by \fC$define\fR, for example,
.IP "" 10
\fC$define sum(I1, I2, Out) :- Out = I1 + I2.\fR
.LP
Suppose this is used in the clause
.IP "" 10
\fCt1(X, Y) :-  sum(X, Y, Res), write(Res).\fR
.LP
Then the goal \fCsum(X, Y, Res)\fR is expanded inline according to the definition
of \fCsum\fR to give
.IP "" 10
\fCt1(X,Y) :-  Res = X + Y, write(Res).\fR
.LP
Again, if \fCsum\fR is used in
.IP "" 10
\fCt2 :-  sum(1, 2, R), write(R).\fR
.LP
then the goal \fCsum(1, 2, R)\fR is expanded inline to give
.IP "" 10
\fCt2 :- R = 1 + 2, write(R).\fR
.LP
Note that the Tokio compiler recognizes constants and does \fInot\fR introduce
intermediate variables to accommodate them.
.MH 3 "Special Relations Subsidiary to Macro Relations: \fC$clause\fP"
Only single-clause macro definitions are allowed with \fC$define\fR, as one
would expect since the definition supplies the code for inline expansions.
But suppose, for example, we wish \fCsum\fR to be written so that it signals
whether or not \fCI1 > I2\fR; suppose it writes a \fC1\fR if \fCI1 > I2\fR, and
writes a \fC0\fR otherwise. As a normal relation, then \fCsum\fR would be
defined as
.IP "" 10
\fCsum(I1, I2, Out) :- I1 > I2, !, write(1), nl, Out = I1 + I2.\fR
.ls 1
.IP "" 10
\fCsum(I1, I2, Out) :- write(0), Out = I1 + I2.\fR
.ls 2
.LP
We may write this as a macro by first of all factoring out what is common to these
two clauses; this gives the \fCsum\fR clause following \fC$define\fR:
.IP "" 10
\fC$define sum(I1, I2, Out) :- H, Out = I1 + I2.\fR
.LP
The \fCH\fR occupies the position where the code for the two clauses differ.
We define this code using the \fC$clause\fR keyword:
.IP "" 10
\fC$clause (H :- I1 > I2, !, write(1))
.ls 1
.IP "" 10
\fC$clause (H :- write(0)).\fR
.ls 2
.LP
In fact, the two \fC$clause\fR clauses are part of the \fC$define\fR
definition. When \fC$clause\fR is used, the clause following \fC$define\fR
must be enclosed in parentheses. Note that each clause introduced by a
\fC$clause\fR is also enclosed in parentheses. Any \fIvariable\fR (beginning
with a capital letter or a '\fC_\fR') name would do in place of \fCH\fR. Finally, only
one '\fB.\fR' should appear in the macro definition, and this at the very end,
after the last \fI$clause\fR clause. Thus the new definition of the macro
\fCsum\fR should be:
.IP "" 10
\fC$define (sum(I1, I2, Out) :- H, Out = I1 + I2)
.ls 1
.IP "" 10
\fC$clause (H :- I1 > I2, !, write(1))
.IP "" 10
\fC$clause (H :- write(0)).\fR
.ls 2
.PP
Suppose this newly defined \fCsum\fR is used in
.IP "" 10
\fCt1(X, Y) :- sum(X, Y, Res), write(Res).\fR
.LP
Then \fCsum\fR is expanded inline in \fCt1\fR to include a call to a relation
corresponding to \fCH\fR, but with a (peculiar) name, say \fC$0t\fR, selected by the
macro-expansion facility:
.IP "" 10
\fCt1(X, Y) :- $0t(X, Y), Res = X + Y, write(Res).\fR
.LP
The procedure \fC$0t\fR is defined to cover the \fCH\fR clauses for this use
of \fCsum\fR:
.IP "" 10
\fC$0t(U, V) :-  U > V, !, write(1).
.ls 1
.IP "" 10
\fC$0t(U, V) :- write(0).\fR
.ls 2
.LP
Suppose, on the other hand, \fCsum\fR is used with constant inputs in:
.IP "" 10
\fCt2 :-  sum(1, 2, R), write(R).\fR
.LP
Then the macro-expansion facility defines a different procedure, say \fC$1t\fR,
to cover the \fCH\fR clauses for this use of \fCsum\fR, and produces:
.IP "" 10
\fCt2 :-  $1t, R = 1 + 2, write(R).
.ls 1
.IP "" 10
\fC$1t :-  1 > 2, !, write(1).
.IP "" 10
\fC$1t :- write(0).\fR
.ls 2
.LP
Note that the constants \fC1\fR and \fC2\fR are hard-coded into the definition of
\fC$1t\fR. Also note that two \fC$1t\fR clauses, corresponding to the two
\fCH\fR clauses, are produced, even though the two together are equivalent
(because '\fC1 > 2\fR' is always false) to the last clause alone. In general, for
every occurence of \fCsum\fR in a normal Tokio program clause, the macro-expansion
facility defines a new procedure with a unique name to cover the clauses
introduced by \fC$clause\fR.
.MH 3 "Scope of Variables in Macro Relation Definitions"
Notice that, in the example above, the compiler was able to identify the
variables \fCI1\fR and \fCI2\fR in the first \fCH\fR clause with the variables \fCI1\fR
and \fCI2\fR in the definition of \fCsum\fR. When \fCsum\fR was used in \fCt1\fR
and \fCt2\fR, the compiler was also able to distinguish between the case in which the
actual arguments of \fCI1\fR and \fCI2\fR were variables (i.e. in \fCt1\fR)  and
the case in which they were constants (i.e. in \fCt2\fR). In the former case, to
cover the \fCH\fR clauses, it defined a procedure \fC$0t\fR with two arguments
corresponding to the two actual arguments. In the latter case, it defined a
zero-ary procedure \fC$1t\fR that had the constant actual arguments written into
it. In either case, the compiler had to identify \fCI1\fR and \fCI2\fR in the
first \fCH\fR clause with the \fCI1\fR and \fCI2\fR in the definition of \fCsum\fR.
In general, the compiler remembers the variable names in the head of a \fC$define\fR
clause. The same variable names occurring in a \fC$clause\fR clause of the
same definition are required to be bound to the same values. In the present case,
the variables in the head of the \fC$define\fR clause are \fCI1\fR, \fCI2\fR,
and \fCOut\fR. Of these, only \fCI1\fR and \fCI2\fR appear in a \fC$clause\fR
clause (specifically, the first). When the program clause \fCt1\fR is compiled,
\fCI1\fR and \fCI2\fR are associated with the variables \fCX\fR and \fCY\fR, 
respectively. Since \fCX\fR and \fCY\fR are variables, the procedure covering
the \fCH\fR clauses in this case, that is, \fC$0t\fR, must have two variable
arguments if it is to have access to the values associated with \fCI1(X)\fR
and \fCI2(Y)\fR. On the other hand, when the program clause \fCt2\fR is
compiled, \fCI1\fR and \fCI2\fR are associated with the constants \fC1\fR and \fC2\fR,
respectively. Then the procedure covering the \fCH\fR clauses in this case,
that is, \fC$1t\fR, need have no arguments since \fC1\fR and \fC2\fR can be written into it
at the appropriate places.
.PP
It is important to keep in mind that only the variables in the head of the
clause following \fC$define\fR are recognized in the clauses introduced by
\fC$clause\fR. For example, suppose we define
.IP "" 10
\fC$define (sum(I1, I2, Out) :- I3 = I1 + 1, H, Out = I1 + I2)\fR
.ls 1
.IP "" 10
\fC$clause (H :- I1 > I2, !, write(1), write(I3))
.IP "" 10
\fC$clause (H :- write(0)).\fR
.ls 2
.LP
Given the program clause
.IP "" 10
\fCt :- sum(2, 1, R), write(R).\fR
.LP
macro expansion produces
.IP "" 10
\fCt :- I3 = 1 + 2, $0t, R = 2 + 1, write(R).\fR
.ls 1
.IP "" 10
.IP "" 10
\fC$0t :- 2 > 1, write(1), write(X).
.IP "" 10
\fC$0t :- write(0).\fR
.ls 2
.LP
The first \fC$0t\fR clause contains a variable (called \fCX\fR here - any other
variable name would do) that does not occur as an argument and is not bound
in the clause. This variable is the image of the \fCI3\fR in the first \fCH\fR
clause and was not recognized as anything special because \fCI3\fR does not
occur in the head of \fCsum\fR.
.MH 3 "Constants in the Heads of Macro Clauses"
The head of the clause introduced by the \fC$define\fR may contain one or more
constants, for example
.IP "" 10
\fC$define sum(1, I1, I2, Out) :- Out = I1 + I2.\fR
.LP
Given the program clause
.IP "" 10
\fCt :-  sum(X, 1, 2, R), write(S), write(R).\fR
.LP
Macro expansion produces
.IP "" 10
\fCt :-  R = 1 + 2, write(1), write(R).\fR
.PP
A single macro relation may contain any number of special relations defined
using \fC$clause\fR. The \fC$clause\fR clauses all follow the \fC$define\fR
clause, and a '\fB.\fR' appears only once, after the last \fC$clause\fR clause.
For example, we could define
.IP "" 10
\fC$define (sum(I1, I2, Out) :- H, Out = I1 + I2, G)
.ls 1
.IP 
.IP "" 10
\fC$clause (H :- I1 > I2, !, write(1))
.IP "" 10
\fC$clause (H :- write(0)) 
.IP
.IP "" 10
\fC$clause (G :- I1 > 0, !, write(a))
.IP "" 10
\fC$clause (G :- write(b)).\fR
.ls 2
.LP
Given the program clause
.IP "" 10
\fCt :- sum(1, 2, R), write(R).\fR
.LP
macro expansion produces
.IP "" 10
\fCt :- $0t0, R = 1 + 2, $0t1.
.ls 1
.IP 
.IP "" 10
\fC$0t0 :- 1 > 2, !, write(1).
.IP "" 10
\fC$0t0 :- write(0).
.IP
.IP "" 10
\fC$0t1 :- 1 > 0, !, write(a).
.IP "" 10
\fC$0t1 :- write(b).\fR
.ls 2
.LP
As is evident from this example, no special provision is needed to handle
multiple special relations defined by \fC$clause\fR.
.MH 3 "Recursive Special Relations"
A special relation defined with \fC$clause\fR may be recursive, for example
.ls 1
.IP "" 10
.nf
.ft C
$define (foo :- write(start), nl, H)
$clause (H :- write('enter number'), read(N),
              if N < 5 then (true && H)
        ).
.fill
.sp
.ls 2
.ft R
.LP
Given the program clause
.IP "" 10
\fCt :- foo, fin(nl, write(end)).\fR
.LP
macro expansion produces
.IP "" 10
\fCt :- write(start), nl, $0t, fin(nl, write(end)).\fR
.ls 1
.IP 
.IP "" 10
\fC$0t :- write('enter number'), read(N),
.IP "" 19
\fCif N < 5 then (true && $0t).\fR
.ls 2
.LP
As long as the members entered are less than \fC5\fR, \fC$0t\fR will chop the current
interval and call itself at the next time point.
.MH 3 "Variable vs. Constant Names as Special Relation Names"
Notice that, when the name of a special relation defined with \fC$clause\fR
begins with an uppercase letter or underscore (and so is a valid variable name),
and as long as the special relation needs access to the values of only the
variables in the head of the macro relation, then there is no need for such
a special relation to have arguments. In fact, an attempt to define such a
special relation with arguments is considered a syntax error. However, there
are times when we would like values of non-head variables to be communicated
to special relations defined with \fC$clause\fR. In that case, the name of the special
relation must begin with a lowercase letter (like a normal program relation or
predicate name) and, as long as the names of the variables in the head of
the macro relation do not occur in the special relation, all communication
is through the arguments (just as with a normal program relation). For example,
consider
.IP "" 10
\fC$define (sum(I1, I2, Out) :- I3 = I1 + 1, h(I1, I2, I3), Out = I1 + I2)
.ls 1
.IP "" 10
.IP "" 10
\fC$clause (h(X, Y, Z) :- X > Y, !, write(1), write(Z))
.IP "" 10
\fC$clause (h(_, _, _) :- write(0)).\fR
.ls 2
.LP
Then the program clause
.IP "" 10
\fCt1 :- sum(2, 3, R), write(R).\fR
.LP
is expanded to 
.IP "" 10
\fCt1 :- I3 = 2 + 1, h(2, 3, I3), R = 2 + 3, write(R).\fR
.ls 1
.IP 
.IP "" 10
\fCh(X, Y, Z) :- X > Y, !, write(1), write(Z).
.IP "" 10
\fCh(_, _, _) :- write(0).\fR
.ls 2
.LP
Notice that the definition of \fCh\fR is unchanged by the macro expansion
and that the constants in the definition of \fCt1\fR have been written into
the \fCh(2,3,R)\fR goal. In fact, there is no difference between defining \fCh\fR
as a special relation in the definition of the macro relation \fCsum\fR and
defining \fCh\fR as a normal program clause. In either case, an \fCh\fR
goal is included in the expansion of \fCsum(2, 3, R)\fR, and (perhaps surprisingly) 
the \fCh\fR relation is available to any clause in the program.
.PP
However, if the a variable occurring in the head of the macro relation
also occurs in the body of a lowercase special relation, then the appropriate 
value is written in place of the occurrence of the variable when the macro is expanded.
For example, consider
.IP "" 10
\fC$define (sum(I1, I2, Out) :- I3 = I1 + 1, h(I3), Out = I1 + I2)
.ls 1
.IP "" 10
.IP "" 10
\fC$clause (h(Z) :- I1 > I2, !, write(1), write(Z))
.IP "" 10
\fC$clause (h(_) :- write(0)).\fR
.ls 2
.LP
Then the program clause
.IP "" 10
\fCt1 :- sum(2, 3, R), write(R).\fR
.LP
is expanded to
.IP "" 10
\fCt1 :- I3 = 2 + 1, h(I3), R = 2 + 3, write(R).
.ls 1
.IP
.IP "" 10
\fCh(Z) :- 2 > 3, !, write(1), write(Z).
.IP "" 10
\fCh(_) :- write(0).\fR
.ls 2
.LP
Here we may think of the scope of \fCI3\fR (or any variable in the head of
the macro relation) as the entire macro definition, including the \fC$clause\fR
clauses.
.PP
The extended scope of a variable in a macro relation's head causes problems
if the same variable name is used for a variable in the head of a special
relation clause. For the occurrences of this variable in the body of the
special relation clause are treated as occurrences of the variable in the
head, not of the special relation clause, but of the macro relation. Suppose, for
example, we intend to write a macro relation to compute the factorial of
a natural number, and we define:
.IP  "" 10
\fC$define (fact(N) :- fact(N, F), write(F))
.ls 1
.IP
.IP "" 10
\fC$clause (fact(N, F) :- N =< 0, !, F = 1)
.IP "" 10
\fC$clause (fact(N, F) :- N1 = M - 1, fact(N1, F1), F = N * F1).\fR
.ls 2
.LP
Then the program clause
.IP "" 10
\fCt :- fact(3).\fR
.LP
is expanded to 
.IP "" 10
\fCt :- fact(3, F), write(F).
.ls 1
.IP "" 10
\fCfact(N, F) :- 3 =< 0, !, F = 1.
.IP "" 10
\fCfact(N, F) :- N1 = 3 - 1, fact(N1, F1), F = 3 * F1.\fR
.ls 2
.LP
Notice that all occurrences of \fCN\fR in the bodies of the
special relation clauses have been replaced by \fC3\fR. If \fCt\fR is evaluated,
a non-terminating recursion will result since the first special clause
always fails. This problem is avoided if \fCN\fR in the special relation
clauses is renamed, say to \fCM\fR. Note, however, that none of the
variables in the clause defining the 2-ary \fCfact\fR relation is intended
to have a scope extending beyond the clause in which it occurs. Thus the
safest and best thing to do in this case and all similar cases is define \fCfact\fR
as a normal program relation.
.PP
Another problem with a lowercase special relation is that its definition
is written into the database everytime the associated macro relation is
expanded. This results in redundant definitions. Although correct behavior
is not jeopardized, this result is obviously undesirable.
.PP
A final problem with a lowercase special relation is that, once the
associated macro relation is expanded, its definition is indistinguishable
from, and may clash with, the definition of a normal program relation. Consider,
for example,
.IP "" 10
\fC$define (foo :- write(1), foo1)
.ls 1
.IP "" 10
\fC$clause (foo1 :- write(2)).
.IP 
.IP "" 10
\fCfoo1 :- write(3).
.IP
.IP "" 10
\fCt :- foo, foo1.\fR
.ls 2
.LP
When the \fCfoo\fR macro is expanded, this program becomes
.IP "" 10
\fCt :- write(1), foo1.\fR
.ls 1
.IP
.IP "" 10
\fCfoo1 :- write(3).
.IP "" 10
\fCfoo1 :- write(2).\fR
.ls 2
.LP
Obviously the \fCfoo1\fR clause derived from the special relation can
never be executed. In such cases, where the special relation needs no
argument, it is best to use an uppercase special relation. Then,
when the macro relation is expanded, a weird name (such as \fC$0t\fR)
is used for the special relation, thus nearly (as long as the programmer
does not use the same weird names) eliminating the possibility of name clashes.
.PP
There are thus three choices for special relations: use an uppercase special
relation, use a lowercase special relation, or use a normal program relation
instead of a special relation. An uppercase special relation should be used
when variables whose scope is the entire macro definition \(em that is, 
variables appearing in the macro relation's head \(em are used and the values
of variables in the body of the macro relation are not needed \(em so no
arguments are needed for the special relation. A normal, not special, relation
should be used when no variable has a scope beyond the clause in which it occurs.
And a lowercase special relation should be used when some variables in the 
relation clauses have normal and some have extended scope.
.MH 3 "Macro Relation Goals with Static Variable Arguments"
The most important use of macro relations is to allow for goals in which static
variables occur. Recall that a static variable may not appear as an
argument in a goal whose functor is a system-defined relation or a normal
user-defined relation. For example, evaluating \fCwrite(*u)\fR would cause
\fC*u\fR itself, not the value of \fC*u\fR, to be output. To produce concise,
readable code, however, we could define
.IP "" 10
\fC$define Output(X) :- Y = X, write(Y).\fR
.LP
Suppose our program also includes
.IP "" 10
\fCt :- *u := 2, output(*u).\fR
.LP
Then, after macro expansion, our program is
.IP "" 10
\fCt :- *u := 2, Y = *u, write(Y).\fR
.LP
It is generally good practice to define macro relations to manipulate the
values of static variables.
.MH 2 "Summary"
.TC
