One binary horn clause is enough

Abstract

This paper proposes an equivalent form of the famous Böhm-Jacopini theorem for declarative languages. C. Böhm and G. Jacopini [1] proved that all programming can be done with at most one single whiledo. 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:

where

$$\left\{ {\begin{array}{*{20}c}{\mathcal{A}_1 \leftarrow .} \\{\mathcal{A}_2 \leftarrow } \\{ \leftarrow \mathcal{A}_4 } \\\end{array} } \right.\mathcal{A}_3 . that is \forall x_1 \cdot \cdot \cdot \forall x_m \left[ {\mathcal{A}_1 \wedge \left( {\mathcal{A}_2 \vee \neg \mathcal{A}_3 } \right) \wedge \neg \mathcal{A}_4 } \right]$$

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 [5]. 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).