Article Free Access Share on A Metalanguage for interactive proof in LCF Authors: M. Gordon University of Edinburgh University of EdinburghView Profile , R. Milner University of Edinburgh University of EdinburghView Profile , L. Morris Syracuse University Syracuse UniversityView Profile , M. Newey Australian National University Australian National UniversityView Profile , C. Wadsworth University of Edinburgh University of EdinburghView Profile Authors Info & Claims POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languagesJanuary 1978Pages 119–130https://doi.org/10.1145/512760.512773Published:01 January 1978Publication History 55citation684DownloadsMetricsTotal Citations55Total Downloads684Last 12 Months96Last 6 weeks5 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

This paper gives the technical details and proofs for the notion of approximate reduction introduced in an earlier paper. The main theorem asserts that every lambda expression determines a set of approximate normal forms of which it is the limit in the lambda calculus models discovered by Scott in 1969. The proof of this theorem rests on the introduction of a notion of type assignments for the lambda calculus corresponding to the projections present in Scott’s models; the proof is then achieved by a series of lemmas providing connections between the type-free lambda calculus and calculations with these type assignments. As motivation for these semantic properties, we derive also some relations between the computational behavior of lambda expressions and their approximate normal forms, and we establish a syntactic analogue of the general considerations motivating the continuity of functions in Scott’s lattice theoretic approach.

A prominent feature of the lattice-theoretic approach to the theory of computation due to D. Scott is the construction of solutions for isomorphic domain equations. One of the simplest of these is a domain isomorphic to the space of all continuous functions from itself to itself, providing the first “mathematical” model for the lambda-calculus of Church and Curry. However, solutions of such domain equations are not unique; in particular, the lambda-calculus has many models. So the question arises as to which one should choose for computational purposes. We consider the relation between equivalence of meaning in Scott's models and the usual notions of conversion and reduction. By extending the lambda-calculus to allow approximate (i.e., partially specified) expressions and approximate reductions, we show that every expression determines a set of approximate normal forms of which it is the limit in Scott’s model. Two immediate corollaries give a characterization of those expressions whose value is the least element of the model and further justification for the result that various lambda-calculus fixed-point combinators are all equal to the lattice-theoretic least fixed-point operator. We show also that this leads to a characterization of equivalence which has a natural counterpart for other languages; specifically, expressions have the same meaning in Scott’s model just when either can serve in place of the other in any “program” without altering its “global” properties.