On the Jacopini Technique


Kuper, Jan (1997) On the Jacopini Technique. Information and Computation, 138 (2). pp. 101-123. ISSN 0890-5401

open access
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 Ω is easy, i.e., Ω 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 λµ-calculus, and we
prove a general theorem concerning the consistency of extensions of the
λµ-calculus of a certain form. Many well known examples (e.g., the easi-
ness of Ω) are immediate consequences of this general theorem.
Item Type:Article
Copyright:© 1997 Elsevier Science
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/17988
Official URL:https://doi.org/10.1006/inco.1997.2655
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 118507