Publication details

Saarland University Computer Science

One binary Horn clause is enough

P. Devienne, P. Lebegue, J.C. Routier, Jörg Würtz

Symposium on Theoretical Aspects of Computer Science, pp. 21--32, Springer-Verlag, February 1994

This paper proposes an equivalent form of the famous Böhm-Jacopini theorem for declarative languages. C. Böhm and G. Jacopini proved that all programming can be done with at most one single while-do. That result is cited as a mathematical justification for structured programming. A similar result can be shown for declarative programming. Indeed the simplest class of recursive programs in Horn clause languages can be defined by the following scheme:

 A1 <-.
 A2 <- A3.  
 <- A4.
 
that is: forall x1...xm (A1 /\ (A2 \/ ~A3) /\ ~A4) where Ai are positive first-order literals. This class is shown here to be as expressive as Turing machines and all simpler classes would be trivial. The proof is based on a remarkable and not enough known codification of any computable function by unpredictable iterations proposed by. Then, we prove effectively by logical transformations that all conjunctive formulas of Horn clauses can be translated into an equivalent conjuctive 4-formula (as above). Some consequences are presented in several contexts (mathematical logic, unification modulo a set of axioms, compilation techniques and other program patterns).

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009