On the Jacopini Technique

    Research output: Contribution to journalArticleAcademicpeer-review

    8 Citations (Scopus)
    36 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Pages (from-to)101-123
    Number of pages23
    JournalInformation and computation
    Volume138
    Issue number2
    DOIs
    Publication statusPublished - Nov 1997

    Fingerprint Dive into the research topics of 'On the Jacopini Technique'. Together they form a unique fingerprint.

    Cite this