T. Strahm Institut fur Informatik und angewandte Mathematik, Universitat Bern Langgassstrasse 51, CH-3012 Bern, Switzerland.
Systems based on theories with partial self-application are relevant to the formalization of constructive mathematics and as a logical basis for functional programming languages. In the literature they are either presented in the form of partial combinatory logic or the partial [lambda] calculus, and sometimes these two approaches are erroneously considered to be equivalent. In this paper we address some defects of the partial [lambda] calculus as a constructive framework for partial functions. In particular, the partial [lambda] calculus is not embeddable into partial combinatory logic and it lacks the standard recursion-theoretic model. The main reason is a concept of substitution, which is not consistent with a strongly intensional point of view. We design a weakening of the partial [lambda] calculus, which can be embedded into partial combinatory logic. As a consequence, the natural numbers with partial recursive function application
area model of our system. The novel point will be the use of explicit substitutions, which have previously been studied in the literature in connection with the implementation of functional programming languages. Explicit mathematics, logic of partial terms, partial [lambda] calculus, partial combinatory logic, explicit substitutions.
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Last updated 29 Mar 96
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1996