Simona Ronchi Della Rocca and Luca Paolini. The parametric lambda-calculus: a metamodel for computation. Computer Science - Monograph. Springer-Verlag, 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 | http ]

Back