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).