Back to University of Twente portal
On the Jacopini Technique
Kuper, Jan (1997) On the Jacopini Technique. Information and Computation, 138 (2). pp. 101-123. ISSN 0890-5401
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 464Kb |
| 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 |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/17988 |
| Official URL: | http://dx.doi.org/10.1006/inco.1997.2655 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
Metis ID: 118507