On the Jacopini Technique
Kuper, Jan (1997) On the Jacopini Technique. Information and Computation, 138 (2). pp. 101123. ISSN 08905401

PDF
475kB 
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 proofreplaceability 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 
Repository Staff Only: item control page
Metis ID: 118507