Director strings as combinators

Kennaway, J. R. and Sleep, M. R. (1988) Director strings as combinators. ACM Transactions on Programming Languages and Systems, 10 (4). pp. 602-626. ISSN 0164-0925

Full text not available from this repository. (Request a copy)

Abstract

A simple calculus (the Director String Calculus-DSC) for expressing abstractions is introduced, which captures the essence of the “long reach” combinators introduced by Turner. We present abstraction rules that preserve the applicative structure of the original lambda term, and that cannot increase the number of subterms in the translation. A translated lambda term can be reduced according to the evaluation rules of DSC. If this terminates with a DSC normal form, this can be translated into a lambda term using rules presented below. We call this process of abstracting a lambda term, reducing to normal form in the space of DSC terms, and translating back to a lambda term an implementation. We show that our implementation of the lambda calculus is correct: For lambda terms with a normal form that contains no lambdas (ground terms), the implementation is shown to yield a lambda calculus normal form. For lambda terms whose normal forms represent functions, it is shown that the implementation yields lambda terms that are beta-convertible in zero or more steps to the normal form of the original lambda term. In this sense, our implementation involves weak reduction according to Hindley et al. [9].

Item Type:	Article
Faculty \ School:	Faculty of Science > School of Computing Sciences
Depositing User:	Vishal Gautam
Date Deposited:	08 Mar 2011 10:55
Last Modified:	24 Sep 2024 10:36
URI:	https://ueaeprints.uea.ac.uk/id/eprint/23346
DOI:	10.1145/48022.48026

Actions (login required)

View Item