On the Jacopini Technique

The general concern of the Jacopini technique is the question: ``Is it consistent to extend a given lambda calculus with certain equations?'' The technique was introduced by Jacopini in 1975 in his proof that in the untyped lambda calculus $\Omega$ is easy, i.e., $\Omega$ can be assumed equal to any other (closed) term without violating the consistency of the lambda calculus. The presentations of the Jacopini technique that are known from the literature are difficult to understand and hard to generalise. In this paper we generalise the Jacopini technique for arbitrary lambda calculi. We introduce the concept of proof-replaceability by which the structure of the technique is simplified considerably. We illustrate the simplicity and generality of our formulation of the technique with some examples. We apply the Jacopini technique to the $\lambda\mu$-calculus, and we prove a general theorem concerning the consistency of extensions of the $\lambda\mu$-calculus of a certain form. Many well known examples (e.g., the easi- ness of $\Omega$) are immediate consequences of this general theorem.