Simona Ronchi Della Rocca and Luca Paolini
The Parametric Lambda-Calculus: a
Metamodel for Computation
Texts in Theoretical Computer Science: An EATCS Series
Springer-Verlag, Berlin, 2004
Ed. Ingeborg Mayer
The book is divided in four parts.
The first part is
devoted to the study of the syntax of
lambda-Delta-calculus. Some syntactical properties,
like confluence and standardization, can be studied for
the whole Delta class. Other properties, like
solvability and separability, cannot be treated in an
uniform way, and they are therefore introduced
separately for different instances of Delta.
In the
second part the operational semantics of
lambda-Delta-calculus is studied. The notion of
operational semantics can be given in a parametric way,
by supplying not only a set of input values but also a
set of output values Theta, enjoying some very natural
properties. A universal reduction machine is defined,
parametric into both Delta and Theta, enjoying a sort
of correctness property in the sense that, if a term
can be reduced to an output value, then the machine
stops, returning a term operationally equivalent to it.
Then four particular reduction machines are presented,
three for the call-by-name lambda-calculus and one for
the call-by-value lambda-calculus, thereby four
operational behaviours that are particularly
interesting for modelling programming languages.
Moreover, the notion of extensionality is revised,
giving a new parametric definition that depends on the
operational semantics we want to consider.
The third
part is devoted to denotational semantics. The general
notion of model of lambdaDelta-calculus is defined,
and then the more restrictive and useful notion of
filter model, based on intersection types, is given.
Then four particular filter models are presented, each
one correct with respect to one of the operational
semantics studied in the previous part. For two of them
completeness is also proved. The other two models are
incomplete: we prove that there are no filter models
enjoying the completeness property with respect to
given operational semantics, and we build two complete
models by using a technique based on intersection
types. Moreover, the relation between filter models and
Scott's model is given.
The fourth part deals with
the computational power of lambda-Delta-calculus. It is
well known that lambda-calculus is Turing complete, in
both its call-by-name and call-by-value variants, i.e.
it has the power of the computable functions. Here we
prove something more, namely that each one of the
reduction machines we present in the third part of this
book can be used for computing all the computable
functions.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43