Proof is by translation into con … for any interpretation of the primitive constant and operator symbols. We thus dene lambda-calculus … LAMBDA-CALCULUS SCHEMATA 265 A lambda-calculus … This is a pre publication version of a paper that app eared in LISP AND SYMBOLIC COMPUTATION: An International Journal, 6,259{288,1993 c1993 Kluwer Academic Publishers {Manufactured in The Netherlands Lambda-Calculus Schemata MICHAELJ. FISCHER y(scher-michael@cs.yale.edu) Department of Computer Science Yale University Box 2158YaleStation New Haven, …

A formal treatment of Hewitt’s question requires away of comparing the expressive power of programming languages. People have the intuitive feeling that some languages are\more powerful”than others. However, most realistic programming languages are universal in the sense that they can simulate Turing machines and hence can compute any partial recursive function. Because of this, attempts to classify real languages according to the functions they can compute inevitably fail, for whatever one language can do, so can another (by simulating the rst). This dilemma, in which ar- gumentsabout relative expressive power become stuck in simulations, and all apparent distinctionsbet ween languagesevap orate under close scrutiny, is known as the \Turingtarpit”and is amajorobstacle towards the de- velopmentofa comparative theory of programming languages. Schemata oeraway out of the dilemma. A schema is a program in which primitive data and operations are leftunspecied, and two schemata are considered equivalent only if they compute the same result no matter how their constants and basic operators are interpreted. This precludes many of the enco ding tricks that lead to the Turingtarpit, and schemata of various kinds can and dodier inexpressive pow er when denedinthis way. Program schemata (also called program schemes), were introduced by Ianov[15]and subsequently studied by many others (see[6,17,26,27,32]). Recursive program schemes, which allow the recursivedenition of functions, were also studied[14,28,36]. The lambda-calculus schemata of this paper are natural extensions of recursive schemes, obtained through the addition of full lambda abstraction. Go od surveys of the state of schema- tologyin 1973 are provided by Chandra[3]and Manna[18]. Ibecameintrigued with Hewitt’squestionand eventually solved it in thearmativeby reformulating the question as one about lambda-calculus schemata and then sho wing how to translate any lambda-calculus schema into one that would work correctly under a shallow-access implementation. Since the LISPCONS operator can be represented asalambdaform using Church-encoding of pairs[4], it is possible to translate any LISP program into a lambda-calculus schema which is equivalent to the original program when interpreted over the domain of S-expressions. In the translated program, CONS is only used to construct the S-expression that is thenal result of computation. (See Section 6.) If the original LISP program is atomic-valued, then CONS is not used at all. In the process of solving this problem, I rediscovered the notion of con tinuation and invented a transformation for converting an arbitrary expression into continuation-passing style (CPS), although I didn’t callitthatatthe time. The rst reference to CPS of which I am now aware is a 1966 paper by van Wijngaarden[37]. CPS was also independently discovered by several others over the next several years[19,23,24,30,35]. Reynolds[31]

Download Lambda-Calculus Schemata.Pdf