Volume 6: January - December 1996

Issue 1: 1996


Partial applicative theories and explicit substitutions

  • Partial applicative theories and explicit substitutions
  • 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 are a 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.

    Keywords: Explicit mathematics, logic of partial terms, partial [lambda] calculus, partial combinatory logic, explicit substitutions.

    Pages: 57 - 79

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    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