Date: Wed 20 May
Time: 15.00
Place: room 214

Speaker: Jan Hruza (Charles Univ., Prague)
Title: Binarization of Logic Programs and Partial Evaluation

Abstract. 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 [1982] 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 [1986] 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 binary program. 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.