Browse Prior Art Database

Highlights of the History of the Lambda-Calculus

IP.com Disclosure Number: IPCOM000129456D
Original Publication Date: 1984-Oct-01
Included in the Prior Art Database: 2005-Oct-06
Document File: 20 page(s) / 93K

Publishing Venue

Software Patent Institute

Related People

J. BARKLEY ROSSER: AUTHOR [+2]

Abstract

This paper gives an account of both the lambda-calculus and its close relative, the combinatory calculus, and explains why they are of such importance for computer software. The account includes the shortest and simplest proof of the Church-F1osser theorem, which appeared in a limited printing in August 1982. It includes a model of the combinatory calculus, also available in 1982 in a limited printing. In the last half-dozen years, some revolutionary new ideas for programming have appeared, involving the very fundamentals of the lambda-calculus and the combinatory calculus. A short introduction is given for a couple of these new ideas.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 6% of the total text.

Page 1 of 20

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Copyright ©; 1984 by the American Federation of Information Processing Societies, Inc. Used with permission.

Highlights of the History of the Lambda-Calculus

J. BARKLEY ROSSER

  (Image Omitted: © 1984 by the American Federation of Information Processing Societies, Inc. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the AFIPS copyright notice and the title of the publication and its date appear, and notice is given that the copying is by permission of the American Federation of Information Processing Societies, Inc. To copy otherwise, or to republish, requires specific permission. Adapted with permission from a paper presented at the 1982 ACM Symposium on LISP and Functional Programming. ~1982, Association for Computing Machinery, Inc. Sponsored by the United States Army under Contract No. DAAG29-

80-C-0041. Author's Address: Mathematics Research Center, University of Wisconsin, 610 Walnut Street, Madison, WI 53705. © 1984 AFIPS 01 64-1 239/84/040337-349

Highlights of the History of the Lambda-Calculus

J. BARKLEY ROSSER .00/00)

This paper gives an account of both the lambda-calculus and its close relative, the combinatory calculus, and explains why they are of such importance for computer software. The account includes the shortest and simplest proof of the Church-F1osser theorem, which appeared in a limited printing in August 1982. It includes a model of the combinatory calculus, also available in 1982 in a limited printing. In the last half-dozen years, some revolutionary new ideas for programming have appeared, involving the very fundamentals of the lambda-calculus and the combinatory calculus. A short introduction is given for a couple of these new ideas.

Categories and Subject Descriptors: F. 1.1 [Computation by Abstract Devices]: Models of Computation -- computability theory; F.4. 1 [Mathematical Logic and Formal Languages]: Mathematical Logic -- lambda-calculus and related systems; K.2 [History of Computing] -- people, software General Terms: Theory Additional Key Words and Phrases: combinatory calculus, Turing machines, foundations of programming, Church's thesis

(Image Omitted: "Kleene-ness is next to Godel-ness")

1. Early Beginnings

The lambda-calculus originated in order to study functions more carefully. In 1893 Frege observed (see van Heijenoort 1967, p. 355) that it suffices to restrict attention to functions of a single argument. Suppose we wish a function to apply to A and B to produce their sum, A + B. Let [NB: math has not been copy edited] be a function, of a single argument, that when applied to A alone produces a new function, again of a single argument, whose value is A + B when applied to B alone. Note that [NB: math has not been copy edited] is not applied simultaneously to A and B, but successively to A and then B; application to A alone...