.ND
.de PT
..
.nr HM 1.5c
.nr FM 2c
.pl 30c
.nr PO 0.5i
.nr LL 7.1i
.TL
Tokio: Logic Programming Language Based on
Temporal Logic
and Its Compilation to Prolog
.AU
M.Fujita*, S. Kono**, H.Tanaka**, T.Moto-oka**
.AI
* FUJITSU LABORATORIES LTD.
** Department of Electronic Engineering, University of Tokyo
.ls 1.5
.AB
Tokio is a temporal logic programming language.
It is a sophisticated extension of Prolog intended
for specification of concurrent
programs.
Its basic execution is a resolution of Linear Time Temporal Logic [1].
Tokio also has an extension that can execute Interval Temporal Logic [2].
The resolution consists of three parts. These are:
unification of temporal variables,
reduction including temporal operators, and controlling intervals.
We developed a Tokio compiler in Prolog.
.AE
.NH
Temporal logic from the point of view of logic programming
.PP
We have been studying hardware specification in a logic programming language [3].
Logic programming has many attractive points.
.IP *
Program validity is directly related to logical consequence.
.IP *
Unification serves as a powerful connection between procedures.
.IP *
It is easy to extract parallelism from a program.
.LP
However, logic programming is rather idealistic.
In general, declarative meaning,
which is the meaning of a logical formula, is somewhat independent
of procedural meaning.
Algorithm implementations are not described in detail in
Prolog. For example, consider the difference between a loop and
a recursion.
Both repetitions have self-reference
pointers for execution. The difference is that
a recursion creates new environments in each cycle time, while
a loop does not.
In traditional languages, stack and frame are used explicitly.
.PP
For example, the loop is the one form of repetition available in Fortran.
On the other hand, there is no loop in Prolog. This is because
Prolog variables
have no state, i.e. single assignment in nature. In order to make a
loop meaningful, new variables must be created at each repetition.
For this reason, loops cannot be directly expressed in Prolog.
Needless to say, repeat-fail-loops destroy the relationship between declarative
meanings and procedural meanings.
.PP
In logic programming, the order of execution is not strictly specified.
Although this freedom is
suitable for getting high concurrency from original program,
detailed descriptions with full specification of complex timing are difficult.
.PP
Temporal logic is a promising tool
for the design and description of hardware.
A loop is represented using the state of a variable, and
both parallelism and sequentiality are easily described using
temporal operators.
There are many kinds of temporal logic.
Here we use two of them: Linear Time Temporal Logic (LTTL) [1] and
Interval Temporal Logic (ITL) [2].
We have been used LTTL for hardware description [3].
Many researchers use propositional logic,
because it has a decision procedure [4].
However, the compact descriptions of first order temporal logic
make it desirable.
Moszkowski developed a language called Tempura based on ITL,
and implemented in lisp [5].
We here present a temporal logic programming language
called Tokio based on a resolution of
LTTL. Tokio Logic is an extension of LTTL containing
some temporal operators of ITL.
Tokio can be considered a logic programming version of Tempura.
.PP
Tokio is used primarily for hardware specification and simulation.
Tokio is expressive and executable enough for hardware description.
Execution of Tokio is not efficient in itself.
Tokio consumes a lot of memory in backtracking and a lot of time in
unification of temporal logic variables.
Like other languages, fast, efficient execution
is of primary importance.
However, a much more important issue is to establish a method of translating
Tokio to a real implementation (i.e. silicon compiler).
We anticipate the output of the compiler to be Register
Transfer Level hardware description language, or some other practical concurrent
languages such as GHC [7].
Tokio supports simulation of early-time-specification,
which is an important hierarchal design tool.
Our final goal is logic circuit synthesis using Tokio.
.PP
In the rest of this chapter, we briefly introduce LTTL and ITL.
In chapter 2, we discuss the basic execution mechanism of Tokio.
The execution of Tokio consists of three parts:
unification of temporal variable, reduction including temporal
operators and an extension with ITL's operators.
In chapter 3, we presents a sample hardware description.
The example is a hardware sorter for a database machine [6].
The technique of compiling Tokio to Prolog is described in chapter 4.
In the last chapter, we discuss the relation among GHC [7],
Tempura, T-Prolog [15] and Tokio.
.NH 2
Linear Time Temporal Logic
.PP
Tokio is based on Linear Time Temporal Logic (LTTL).
LTTL is based on discrete time concepts, i.e. it has a minimum unit of time.
Variable and predicate meanings are determined for each state, i.e. instants
in time.
Therefore, variables may have many values depending on the time at
which they are evaluated.
There are three major temporal operators in LTTL:
.B "next or @,"
.B always
and
.B until.
.LP
First we discuss the
.B @
operator. @P means P is true at the next state, i.e. next clock period.
.DS
.sp 5
Fig. 1 @P next operator
.br
.DE
There are two kinds of equality in Tokio.
The first kind of equality is an identity.
This type of equality means two values are equal in all states.
This is also called temporal equality.
The other kind of equality is single state equality, that is,
the two variables' values
are equal only at the present instant and not necessarily equal
in future states (Fig. 2).
.DS
.sp 5
Fig. 2 Reference to Next Time Value
.DE
The syntax of Tokio is very similar to that of DEC-10 Prolog [8].
Words beginning with a capital letter are variables. In (1),
.B =
symbolizes single state equality. The two X's denote the same variable.
These two X's are equal in all states.
The value of X at present is equal to the value of X in the next state.
.IP
@X = X (1)
.PP
The next major operator is the
.B always
operator.
.B Always
describes a predicate that is true in all states (Fig.3).
.DS
.sp 5
Fig. 3 #P Always Operator
.DE
Instead of the square notation used in [1], we symbolize
.B always
with
.B #.
.B #
is defined recursively using the
.B next
operator. This operator is a little different from the
.B @
operator. However as far as LTTL concerned, two operators are same.
.IP
#P :- P,next(#P). (2)
.LP
.B "':-'",
.B "','"
and
.B "'.'"
indicate
implication, conjunction, and termination, respectively.
In Tokio, a clause is an axiom,
i.e. it is true for all states.
.LP
Finally we introduce the
.B until
operator.
.IP
p until q (3)
.LP
This means that p is true for all states until the state in which
q becomes true (Fig.4).
.DS
.sp 5
Fig. 4 P until Q
.DE
.B Until
can also be defined using the
.B @
operator.
.IP
P until Q :- Q,!. (4)
P until Q :- P,@(P until Q).
.LP
Note that the cut operator of first clause indicates negation of Q in
a second clause.
In order to satisfy the close world assumption, Q must not have temporal
operator and undefined variables when this operator is evaluated.
Tokio can be extented to handle Interval Temporal Logic.
In the following section, we briefly review ITL.
.NH 2
Interval temporal logic
.LP
Interval temporal logic (ITL) was developed by B. Moszkowski [2].
In this logic, variable and predicate meanings are determined
for each interval.
An interval is a continuous finite sequence of states.
In this section, five operators are introduced:
.B chop,
.B length,
.B halt,
.B fin
and
.B keep.
.PP
The
.B chop
operator is a binary operator. This operator splits an interval
into two parts.
.B '&&'
symbolizes the
.B chop
operator.
.B ';'
expresses the chop operator used in [2],
however, since
.B ';'
denotes the
.B or
operator in Prolog, we use
.B '&&'
to avoid confusion.
.IP
P && Q (5)
.LP
The meaning of (5) is related to three intervals.
Consider an interval I,
diveded into two consecutive parts: Ip represents the former portion, and
Iq, the later.
If P is true during Ip,
and Q is true during Iq, then (5) is true during I (Fig.5).
.DS
.sp 5
Fig. 5 p && q
.DE
.PP
The
.B length
operator specifies the length of an interval (Fig.6).
.DS
.sp 5
Fig. 6 length 5
.DE
The length of an interval
is the number of states contained in the interval minus one.
.IP
p :- length(5). (6)
.LP
In (6), p is true on the interval which has 6 states.
Length must be a nonnegative integer. Using
.B chop
and
.B length,
the
.B next
operator in ITL can be defined as follows (7).
.DS
.sp 5
Fig. 7 @ operator in ITL
.DE
.IP
@P <-> length(1) && P (7)
.LP
This type of
.B next
is called
.B strong
in [5], because if the interval length is 0 then @P is false.
In the other word,
this operator extends an interval.
An interval whose length is 0 is called
.B empty.
In the case of the LTTL
.B next
operator, it is succeeded even in an empty intervals.
The
.B next
operator is independent of the interval.
.IP
next(P) <-> length(1) && P (8)
or next(P) <-> empty
.LP
This kind of
.B next
is called
.B weak.
The conditional statement which is related to
.B empty
requires special
treatment in Tokio. The following three statements are important.
.IP
halt(P) <-> #(P->empty, not(P)->not(empty)).
fin(P) <-> #(empty->P). (9)
keep(P) <-> #(not(empty)->P).
.LP
The
.B halt(P)
statement means that the interval length is determined by
the formula P.
.B Keep(P)
means P is true for all states except the one at the end of the interval.
.B Fin(P)
means P is true only in the final state of the interval.
.NH 2
Tokio combines LTTL and ITL
.PP
LTTL can easily describe concurrency using conjunctions; however,
sequentiality is not so easily described.
ITL's
.B chop
operator is superior
to LTTL's
.B until
operator for the description of sequentiality.
.B "p && q"
simply means that q will be executed after the termination of p.
On the other hand,
.B "p until q"
means that p is true until q holds. This
statement does not specify the termination of p.
.PP
The key concepts describing the relationship between ITL and LTTL are
.B local
and
.B interval
variables [10].
.B Local
means ITL expressions that do not depend on when an interval ends.
In another words, meanings of
.B local
variables or predicates
are decided in the first time (state) of the interval.
LTTL concepts are all translated into
.B local
concepts in ITL.
In order to introduce the
.B chop
operator to Tokio, we use interval
variables corresponding to each Tokio clause.
These variables are all LTTL variables and they are generated by
existential quantifiers.
Tokio Variables have different meaning from ITL variables,
because interval variables are only associated with clauses.
This means that all the variables in Tokio are
.B local.
.IP
p :- q && r. .... Ip
q. .... Iq (10)
r. .... Ir
.LP
Ip, Iq and Ir are all interval variables. Each variable
represents its corresponding interval.
The
.B Chop
operator generates the intervals
Iq and Ir from Ip using an existential quantifier.
This corresponds to splitting an interval into two parts.
.NH 2
An extension of Horn clause for temporal logic
.PP
The Horn clause is a restricted form of logic formula. It consists of
two parts: head and body.
.IP
head :- body. (11)
.LP
This means that the head is implied by the body.
Variables in a head are all universally
quantified and variables in a body are all existentially quantified.
A head must be an atomic predicate.
Roughly speaking, a Tokio Horn clause is a Horn clause including
temporal operator in its body.
.PP
In Tokio, there are some restrictions.
To avoid a circularly structured temporal variable, the
.B @
function
is only allowed in the expression
.B =.
The primitive temporal operators such as
.B next
or
.B chop
operator
are not allowed in the head of Horn clause.
.NH
Resolution of Tokio
.PP
The execution of Tokio is a kind of resolution of LTTL.
Unification and reduction generate a model incrementally.
In LTTL, the model is generated for each state.
It is also necessary to unify temporal variables.
.IP *
Reduction on multi-state model
.IP *
Unification on temporal variable
.LP
Our Tokio also has an ITL extension.
Generation of interval variable is the third execution unit.
.IP *
Generation of interval variables
.LP
There are the three main execution units of Tokio.
.NH 2
Reduction to the future
.PP
If there are no temporal operators, the reduction of Tokio is identical to
that of Prolog. A predicate including the
.B next
operator defines another state.
These predicates are enqueued with the environment corresponding to
the next state, and will be reduced later.
Queuing is necessary to execute Tokio formula in the proper temporal order.
We call this property a
.B healthy
execution.
On the other hand, the execution order of a predicate referring to the
same state need not be specified. In order to execute system predicates
or numeric calculations, the execution order must be determined by
the data dependency.
.PP
Tokio executes the predicates corresponding to a given
state in the same way as Prolog does.
This is only a practical solution. In this manner Tokio includes Prolog
in itself. In Tokio there are two kind of reduction: Prolog-wise reduction and
time-wise reduction (Fig. 8).
.DS
.sp 6
Fig. 8 Two way reduction
.DE
.IP
?-@ @write(3),@write(2),write(0),write(1). (12)
0123
yes
.LP
.B '?-'
means a goal in Tokio. Notice that the
.B next
statement is executed after the current state.
.NH 2
Unifier for temporal logic variable
.PP
A Tokio variable assumes many different values.
These values are generated incrementally as time advances.
Unification is a basic operation for accessing these values.
Unification consists of two primitives.
.IP 1)
to select current state value and successive state values.
.LP
This is very much like car and cdr.
.IP 2)
to unify all the values of successive states.
.LP
The former type of unification is performed by an
.B =
and
.B @.
The later type of unification is executed in a head of clause.
Consider a simple counter in Tokio.
.IP
counter(X) :- #(@X=X+1). (13)
?- X=0,counter(X),#write(X),length(3).
0123
yes
.LP
Counter increments the value of X in each state.
The variable X in the goal is unified in all states with variable X in
the counter clause. On the other hand, in the definition of counter
.B =
predicates unifies the next state of variable X and the incremented
value of variable X in the current state.
.NH 2
Interval generator using interval variable
.PP
The interval variables in Tokio consists of two parts in our
implementation. These are the ending time of the interval, and
the flag of interval completion.
This flag is generated in each
time clock. Some ITL operators use this flag directly; for
example, the
.B fin
and
.B keep
operators are not executed until this
flag is determined. Tokio has a waiting queue for the
.B fin
and
.B keep
operators.
.PP
The interval variable is generated only by a
.B chop
operator.
The consistency of the interval length is checked in every
state. The length of an inner interval must be less or equal
than the length of an outer interval.
.PP
One feature of Tokio is automatic interval length tuning.
Tokio use a simple strategy for interval determination:
the shortest possible interval is selected. Tokio tries to cut off the interval
which does not have length specification. Controlling the
interval length is performed by backtracking.
This mechanism is known to useful in goal oriented simulation [15].
If there is a maximum interval length,
Tokio can generate all the necessary length combination of the intervals.
This is very useful when it is necessary to join processes.
.IP
qs(X) :- split(X,H,L) && qs(H),qs(L). (14)
.LP
(14) is a part of quick sort. First
.B qs
splits a list X into
two parts: H and L, and then performs
.B qs
for each part.
Because length of parts may be different, two
.B qs
may use different lengths of time.
In the predicate
.B split,
using a temporal operator such as temporal assignment
which is not dependent on
the length of interval,
.B qs
can be written in a form which is not depended on
interval length. In such a case, the length of
.B qs
is automatically tuned and each
.B qs
has the same interval length.
.NH
Hardware description in Tokio
.PP
In this section, a sample description of a pipeline merge sorter
is presented.
The pipeline merge sorter is a component of the relational database
machine GRACE [6]. A sorter prototype was already
available.
The pipelining details are described in Tokio.
.NH 2
Pipeline merge sorter in Tokio
.PP
Fig.10 is a sample description of a pipelineed merge sort.
.KF
.sp 4.2i
Fig. 9 Organization of Pipeline Merge Sorter
.sp
.KE
.KF
.nf
.in 0.5i
test :- Strdata = [10,20,5,100,1,6,2,3],
datagen(Strdata, Data),
pipe(Data, Out),
length(18),
#write(Out).
% Data Generator
datagen([],[]).
datagen([H|T],Out) :-
Out = [H],
@T = T, @datagen(T,Out).
% Pipeline Merge Sorter
pipe(I0,Out) :-
I1 = [], I2 = [], Out = [],
proc_start(I0,I1, 2,1),
proc_start(I1,I2, 4,2),
proc_start(I2,Out,8,4).
% Processor Unit
proc_start(I,O,P,PP) :-
X = [], Y = [], Z = [], T = 1,
#proc(I,O,X,Y,Z,T,P,PP).
proc(I,O,X,Y,Z,T,P,PP) :- X=[],Y=[],I=[],!,
@X=X, @Y=Y, @Z=Z, @O=[], @T=1.
proc(I,O,X,Y,Z,T,P,PP) :-
load(I,O,X,Y,Yn,Z,Zn,T,P,PP),
merge(I,O,X,Y,Yn,Z,Zn,T,P,PP).
load(I,O,X,Y,Yn,Z,Zn,T,P,PP) :- T=