Wed 20 May
Jan Hruza (Charles Univ., Prague)
Binarization of Logic Programs and Partial Evaluation
Binary clauses are Horn clauses which have one atom in the head and at
most one atom in the body. Such clauses appear quite naturally when
simulating computations of a Turing machine by a logic program.
It seems that Tarnlund was the first to introduce the concept of binary
clauses. Sebel=A1k and Stepanek  constructed logic programs for
recursive functions. It turned out that these programs were stratifiable.
Moreover, it was possible to transform every such program to a binary
logic program computing the same function, the length of computations of
the resulting binary program being the same on every input. However, the
transformation was closely tied to the language of successor arithmetic.
Then it was natural to ask whether it is possible to transform every
logic program to an equivalent binary program.
Maher  gave an affirmative answer to this problem. His solution
introduces for the first time the typical ingredients, namely, replacing
atomic formulas by terms and clauses by list of terms. His transformation
giving stratfiable binary programs that use two implicite stacks.
Stepankova & Stepanek (1989) simplified this construction and the
resulting programs are stratified and use one stack only.
Another transformation to binary programs was described by Sato an
Tamaki (1989) . It uses classification of input - output arguments and
techniques based on unfolding and folding and continuation .
Tarau and Boyer (1990) introduced so called elementary programs as a
generalization of binary programs.
They describe some simple transformations of metaprograms to binary
programs based on the observation that the semantics of definite
metaprograms can be reduced to the semantics of a definite program.
Continuations in the resulting programs can be then treated as
metavariables. Essentially the same transformation is described by Demoen
(1992), along with an "incremental" variant of it. Some other
transformations are given applicable to the resulting binary programs.
They keep their binary character and improve their computational
properties during compilation. Namely, it is shown that partial evaluation
of the binary program, combined with deletion of unnecessary variables and
a low level source code transformation can result in a more efficient
We shall show that the transformations due to Stepankova=A0 and Stepanek,
Tarau and Boyer and Demoen are computationally equivalent. As a
consequence of that, the additional transformations due to Demoen
are applicable to the results of the above transformations and exhibit
the same effects.
On the other hand, the transformation due to Maher exihibits a different
computational behaviour. The search space of the resulting binary program
is being searched essentially in a breadth-first manner, and,
consequently, the partial evaluation does not give reasonable results.
Binarization also found applications in the fields of PROLOG
implementation, transformation to tail-recursive predicates and even
mobile code. These applications will be shortly discussed.