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: 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