The lambda-calculus was invented by Church in the 1930s with the purpose of supplying a logical foundation for logic and mathematics. Its use by Kleene as a coding for computable functions makes it the first programming language, in an abstract sense, exactly as the Turing machine can be considered the first computer machine. The lambda-calculus has quite a simple syntax (with just three formation rules for terms) and a simple operational semantics (with just one operation, substitution), and so it is a very basic setting for studying computation properties. The first contact between lambda-calculus and real programming languages was in the years 1956-1960, when McCarthy developed the LISP programming language, inspired from lambda-calculus, which is the first ``functional'' programming language, i.e., where functions are first-class citizens. But the use of lambda-calculus as an abstract paradigm for programming languages started later as the work of three important scientists: Strachey, Landin and Bøhm. Strachey used the lambda-notation as a descriptive tool to represent functional features in programming when he posed the basis for a formal semantics of programming languages. Landin formalized the idea that the semantics of a programming language can be given by translating it into a simpler language that is easier to understand. He identified such a target language in lambda-calculus and experimented with this idea by giving a complete translation of ALGOL60 into lambda-calculus. Moreover, he declared that a programming language is nothing more than lambda-calculus plus some ``syntactic sugar''. Bøhm was the first to use lambda-calculus as an effective programming language, defining, with Gross, the CUCH language, which is a mixture of lambda-calculus and the Curry combinators language, and showing how to represent in it the most common data structures. But, until the end of the 1960s, lambda-calculus suffered from the lack of a formal semantics. In fact, while it was possible to codify in it all the computable functions, the meaning of a generic lambda-term not related to this coding was unclear. The attempt to interpret lambda-terms as set-theoretic functions failed, since it would have been necessary to interpret it into a set D isomorphic to the set of functions from D to D, which is impossible since the two spaces always have different cardinality. Scott solved the problem by interpreting lambda-calculus in a lattice isomorphic to the space of its continuous functions, thus giving it a clear mathematical interpretation. So the technique of interpretation by translation, first developed by Landin, became a standard tool to study the denotational semantics of programming languages; almost all textbooks in denotational semantics follow this approach. But there was a gap between lambda-calculus and the real functional programming languages. The majority of real functional languages have a ``call-by-value'' parameter passing policy, i.e., parameters are evaluated before being passed to a function, while the reduction rule of lambda-calculus reflects a ``call-by-name'' policy, i.e., a policy where parameters are passed without being evaluated. In the folklore there was the idea that a call-by-value behaviour could be mimicked in lambda-calculus just by defining a suitable reduction strategy. Plotkin proved that this intuition was wrong and that lambda-calculus is intrinsically call-by-name. So, in order to describe the call-by-value evaluation, he proposed a different calculus, which has the same syntax as lambda-calculus, but a different reduction rule. The aim of this book is to introduce both the call-by-name and the call-by-value lambda-calculi and to study their syntactical and semantical properties, on which their status of paradigmatic programming languages is based. In order to study them in a uniform way we present a new calculus, the lambda-Delta-calculus, whose reduction rule is parametric with respect to a subset Delta of terms (called the set of input values) that enjoy some suitable conditions.Different choices of Delta allow us to define different languages, in particular the two lambda-calculus variants we are speaking about. The most interesting feature of lambda-Delta-calculus is that it is possible to prove important properties (like confluence) for a large class of languages in just one step. We think that lambda-Delta-calculus can be seen as the foundation of functional programming.

The Parametric Lambda-Calculus: a Metamodel for Computation

RONCHI DELLA ROCCA, Simonetta;PAOLINI, LUCA LUIGI
2004-01-01

Abstract

The lambda-calculus was invented by Church in the 1930s with the purpose of supplying a logical foundation for logic and mathematics. Its use by Kleene as a coding for computable functions makes it the first programming language, in an abstract sense, exactly as the Turing machine can be considered the first computer machine. The lambda-calculus has quite a simple syntax (with just three formation rules for terms) and a simple operational semantics (with just one operation, substitution), and so it is a very basic setting for studying computation properties. The first contact between lambda-calculus and real programming languages was in the years 1956-1960, when McCarthy developed the LISP programming language, inspired from lambda-calculus, which is the first ``functional'' programming language, i.e., where functions are first-class citizens. But the use of lambda-calculus as an abstract paradigm for programming languages started later as the work of three important scientists: Strachey, Landin and Bøhm. Strachey used the lambda-notation as a descriptive tool to represent functional features in programming when he posed the basis for a formal semantics of programming languages. Landin formalized the idea that the semantics of a programming language can be given by translating it into a simpler language that is easier to understand. He identified such a target language in lambda-calculus and experimented with this idea by giving a complete translation of ALGOL60 into lambda-calculus. Moreover, he declared that a programming language is nothing more than lambda-calculus plus some ``syntactic sugar''. Bøhm was the first to use lambda-calculus as an effective programming language, defining, with Gross, the CUCH language, which is a mixture of lambda-calculus and the Curry combinators language, and showing how to represent in it the most common data structures. But, until the end of the 1960s, lambda-calculus suffered from the lack of a formal semantics. In fact, while it was possible to codify in it all the computable functions, the meaning of a generic lambda-term not related to this coding was unclear. The attempt to interpret lambda-terms as set-theoretic functions failed, since it would have been necessary to interpret it into a set D isomorphic to the set of functions from D to D, which is impossible since the two spaces always have different cardinality. Scott solved the problem by interpreting lambda-calculus in a lattice isomorphic to the space of its continuous functions, thus giving it a clear mathematical interpretation. So the technique of interpretation by translation, first developed by Landin, became a standard tool to study the denotational semantics of programming languages; almost all textbooks in denotational semantics follow this approach. But there was a gap between lambda-calculus and the real functional programming languages. The majority of real functional languages have a ``call-by-value'' parameter passing policy, i.e., parameters are evaluated before being passed to a function, while the reduction rule of lambda-calculus reflects a ``call-by-name'' policy, i.e., a policy where parameters are passed without being evaluated. In the folklore there was the idea that a call-by-value behaviour could be mimicked in lambda-calculus just by defining a suitable reduction strategy. Plotkin proved that this intuition was wrong and that lambda-calculus is intrinsically call-by-name. So, in order to describe the call-by-value evaluation, he proposed a different calculus, which has the same syntax as lambda-calculus, but a different reduction rule. The aim of this book is to introduce both the call-by-name and the call-by-value lambda-calculi and to study their syntactical and semantical properties, on which their status of paradigmatic programming languages is based. In order to study them in a uniform way we present a new calculus, the lambda-Delta-calculus, whose reduction rule is parametric with respect to a subset Delta of terms (called the set of input values) that enjoy some suitable conditions.Different choices of Delta allow us to define different languages, in particular the two lambda-calculus variants we are speaking about. The most interesting feature of lambda-Delta-calculus is that it is possible to prove important properties (like confluence) for a large class of languages in just one step. We think that lambda-Delta-calculus can be seen as the foundation of functional programming.
2004
Springer-Verlag
1
252
9783540200321
http://www.di.unito.it/~paolini/
http://www.di.unito.it/~ronchi/
http://www.springer.com/computer/foundations/book/978-3-540-20032-1
parametric lambda-calculus; operational and denotational semantics; parameter passing; intersection types and logical models
S. RONCHI DELLA ROCCA; L. PAOLINI
File in questo prodotto:
File Dimensione Formato  
The Parametric Lambda Calculus - BOOK 2004 ori.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 4.67 MB
Formato Adobe PDF
4.67 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/16319
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact