[Prev][Next][Index][Thread]
Domains and Lambda Calculi (book announcement)
Book announcement:
DOMAINS AND LAMBDA CALCULI
by Roberto AMADIO and Pierre-Louis CURIEN
Cambridge Tracts in Theoretical Computer Science 46,
ISBN 0-521-62277-8, Cambridge University Press
We are pleased to announce that the book is now available.
Order informations can be found at
http://www.cup.cam.ac.uk/Scripts/webbook.asp?isbn=0521622778
and for North-America at
http://www.cup.org/Titles/62/0521622778.html
You will find enclosed the Table of Contents and an abridged Preface.
Truly,
Roberto Amadio and Pierre-Louis Curien
------------------------------------------------------------------------
Table of Contents
Preface, Notation
1 Continuity and computability
1.1 Directed completeness and algebraicity
1.2 Dcpo's as topological spaces
1.3 Computability and continuity
1.4 Constructions on dcpo's
1.5 Toy denotational semantics
1.6 Continuation semantics
2 Syntactic theory of the lambda-calculus
2.1 Untyped lambda-calculus
2.2 The labelled lambda-calculus
2.3 Syntactic continuity
2.4 The syntactic sequentiality theorem
3 D-infinity models and intersection types
3.1 Lambda-models
3.2 Properties of D-infinity models
3.3 Filter models
3.4 Some D-infinity models as filter models
3.5 More on intersection types
4 Interpretation of lambda-Calculi in CCC's
4.1 Simply typed lambda-calculus
4.2 Cartesian closed categories
4.3 Interpretation of lambda-calculi
4.4 From CCC's to lambda-theories and back
4.5 Logical relations
4.6 Interpretation of the untyped lambda-calculus
5 CCC's of Algebraic Dcpo's
5.1 Continuous dcpo's
5.2 Bifinite domains and L-domains
5.3 Full sub-CCC's of Acpo
5.4 Full sub-CCC's of Adcpo
5.5 Completeness of well-ordered lub's
6 The Language PCF
6.1 The lambda Y-calculus
6.2 Fixpoint induction
6.3 The programming language PCF
6.4 The full abstraction problem for PCF
6.5 Towards sequentiality
6.6 PCF Bohm trees
7 Domain equations
7.1 Domain equations
7.2 Predicate equations
7.3 Universal domains
7.4 Representation
8 Values and computations
8.1 Representing computations as monads
8.2 Call-by-value and partial morphisms
8.3 Environment machines
8.4 A FA model for a parallel lambda-calculus
8.5 Control operators and CPS translation
9 Powerdomains
9.1 Monads of powerdomains
9.2 CCS
9.3 Interpretation of CCS
10 Stone duality
10.1 Topological spaces and locales
10.2 The duality for algebraic dcpo's
10.3 Stone spaces
10.4 Stone duality for profinite dcpo's
10.5 Scott domains in logical form
10.6 Bifinite domains in logical form
11 Dependent and second order types
11.1 Domain theoretical constructions
11.2 Dependent and second order types
11.3 Types as retractions
11.4 System LF
11.5 System F
12 Stability
12.1 Conditionally multiplicative functions
12.2 Stable functions
12.3 dI-domains and event structures
12.4 Stable bifinite domains
12.5 Connected glb's
12.6 Continuous L-domains
13 Towards linear logic
13.1 Coherence spaces
13.2 Categorical interpretation of linear logic
13.3 Hypercoherences and strong stability
13.4 Bistructures
13.5 Chu spaces and continuity
14 Sequentiality
14.1 Sequential functions
14.2 Sequential algorithms
14.3 Algorithms as strategies
14.4 Full abstraction for PCF + catch
15 Domains and realizability
15.1 A universe of realizable sets
15.2 Interpretation of system F
15.3 Interpretation of type assignment
15.4 Partiality and separation in per
15.5 Complete per's
15.6 Extensional per's
15.7 Per's over D-infinity
15.8 Interpretation of subtyping
16 Functions and processes
16.1 pi-calculus
16.2 A concurrent functional language
16.3 Adequacy
App 1 Summary of recursion theory
A 1.1 Partial recursive functions
A 1.2 Recursively enumerable sets
A 1.3 The Rice-Shapiro theorem
App 2 Summary of category theory
A 2.1 Basic definitions
A 2.2 Limits
A 2.3 Functors and natural transformations
A 2.4 Universal morphisms and adjunctions
A 2.5 Adjoints and limits
A 2.6 Equivalences and reflections
A 2.7 Cartesian closed categories
A 2.8 Monads
Bibliography, Index
----------------------------------------------------------
PREFACE (abridged)
Denotational semantics is concerned with the mathematical meaning of
programming languages. Programs are to be interpreted in categories
with structure by which we mean initially sets and functions, and
later, suitable topological spaces and continuous functions. The main
goals of this branch of computer science are, in our belief:
* To provide rigorous definitions that abstract away from
implementation details, and that can serve as an implementation
independent reference.
* To provide mathematical tools for proving properties of programs: as
in logic, semantic models are guides in designing sound proof rules,
that can then be used in automated proof-checkers like LCF.
Historically the first goal came first. In the sixties Strachey was
writing semantic equations involving recursively defined data types
without knowing if they had mathematical solutions. Scott provided the
mathematical framework, and advocated its use in a formal proof system
called LCF. Thus denotational semantics has from the beginning been
applied to the two goals.
In this book we aim to present in an elementary and unified way the
theory of certain topological spaces, best presented as order
theoretical structures, that have proved to be useful in the modelling
of various families of typed lambda-calculi considered as core
programming languages and as meta-languages for denotational
semantics. This theory is now known as Domain Theory, and has been
founded as a subject by Scott and Plotkin.
The notion of continuity used in domain theory finds its origin in
recursion theory. Here the works of Platek and Ershov come to mind: in
Stanford and Novosibirsk, independently, they both exploited the
continuity properties of recursive functionals to build a theory of
higher order recursive functions. Recursion theory is implicit in the
basics of domain theory, but becomes again explicit when effective
domains are considered.
The topic is indebted to lattice theory and topology for ideas and
techniques, however the aims are different. We look for theories that
can be usefully applied to programming languages (and
logic). Therefore a certain number of complications arise that are not
usually considered. Just to name a few:
* The topologies we are interested in satisfy only a weak separation
axiom (T_0). This stands in sharp contrast with classical topology
based on T_2, or Hausdorff spaces, but it relates to the subject of
pointless topology.
* In applications it is difficult to justify the existence of a
greatest element, hence the theory is developed without assuming the
existence of arbitrary lub's, that is, we will not work with complete
lattices.
* There are several models of computation, certainly an important
distinction is the possibility of computing in parallel or in series,
hence the development of various notions of continuous, stable, and
sequential morphisms.
* There is a distinction between an explicitly typed program and its
untyped run time representation, hence the connection with
realizability interpretations.
One of our main concerns will be to establish links between
mathematical structures and more syntactic approaches to semantics,
often referred to as operational semantics. The distinction of
operational vs. denotational is reminiscent of the distinction between
`function as extension, or as a graph' (say, of a partial recursive
function) and `function as a rule, is not an english word or as an
algorithm' (say, the specification of a Turing machine). The qualities
of a denotational semantics can be measured in the way it matches an
independently defined operational semantics. Conversely, an
operational semantics, like any formal system, can be `blessed' by
soundness or even completeness results with respect to some
denotational semantics.
We shall therefore describe operational semantics as well as
denotational semantics. In our experience it is essential to insist
on these two complementary views in order to motivate computer
scientists to do some mathematics and in order to interest
mathematicians in structures that are somehow unfamiliar and far away
from the traditional core of mathematics.
A description of the contents of each chapter follows. Unless stated
otherwise we do not claim any novelty for the material presented here.
Chapter 1 introduces the first concepts in domain theory and
denotational semantics: directed complete partial orders,
algebraicity, and Scott topology. A basic link between Scott
continuity and computability (the Myhill-Shepherdson theorem) is
established. As an application, the denotational semantics of two
simple imperative languages are presented, and are shown to be
equivalent to their formal operational semantics.
Chapter 2 introduces the untyped lambda-calculus}. We establish
several of the fundamental theorems of lambda-calculus using a
labelling technique due to Le'vy. In this way we prove the
Church-Rosser property, the standardization theorem, and the finite
developments theorem. The same technique also yields the strong
normalization property for the simply typed lambda-calculus. Finally,
we show the syntactic continuity theorem (a further evidence of the
role of continuity in the semantics of programming languages) and the
sequentiality theorem, which motivates the semantic study of
sequentiality.
Chapter 3 is a case study of the fundamental domain equation D=D->D,
which provides models of the untyped lambda-calculus. We detail the
construction of the D-infinity models, obtained as suitable
limits. The chapter is also a case study of Stone duality: the
D-infinity models can also be constructed out of certain theories of
`types', or functional characters.
Chapter 4 is an introduction to the interpretation of simply typed and
untyped lambda-calculi in categories. In particular we develop the
categorical models of simply typed and type free lambda-calculus and
illustrate the techniques needed to prove the soundness and
completeness of the related interpretations.
Chapter 5 gives a complete presentation of the problem of classifying
the largest cartesian closed categories of algebraic directed complete
partial orders and continuous morphisms, which was solved by Jung,
following earlier work by Smyth. Two important classes of algebraic
cpo's come out of this study: bifinite domains, and L-domains.
Chapter 6 presents the language PCF of Scott-Plotkin-Milner. This is a
simply typed lambda-calculus extended with fixpoints and arithmetic
operators. For this calculus we discuss the full abstraction problem,
or the problem of the correspondence between denotational and
operational semantics.
Chapter 7 presents the basic apparatus for the solution of domain
equations. It also includes material on the construction of universal
domains, and on the representation of domains by projections.
Chapter 8 studies lambda-calculi endowed with a reduction strategy
that stops at lambda-abstractions. We analyse in particular a
call-by-value lambda-calculus and a lambda-calculus with control
operators. We introduce the semantic aspects of these calculi via a
unifying framework proposed by Moggi and based on the idea of
computation-as-monad.
Chapter 9 concentrates on the construction of powerdomains (loosely
speaking a powerset construction in domain theory) and their
applications to the semantics of non-deterministic and concurrent
computations. On the denotational side we develop the theory of
Plotkin's convex powerdomain. On the syntactic side we introduce a
process calculus (Milner's CCS) and its operational semantics based on
the notion of bisimulation. We interpret CCS using a domain equation
which involves the convex powerdomain and relate the denotational
semantics to the operational one.
Chapter 10 presents Stone duality (originally the correspondence
between Boolean algebras and certain topological spaces), applied to
domains. Algebraic domains can be reconstructed from their compact
elements, or from the opens of their Scott topology, which can be
viewed as observable properties. Elements are then certain kinds of
filters of properties. This idea can be exploited to the point of
presenting domain theory in logical form, as advocated by Martin-Lo"f
(a program which was carried out systematically by Abramsky).
Chapter 11 introduces the problem of the categorical interpretation of
a typed lambda-calculus with dependent and second order types along
the lines established in chapter 4. We first develop some guidelines
in a categorical framework, and then we apply them to the specific
cases of categories of complete partial orders and Scott domains. Two
popular fragments of this typed lambda-calculus are considered in
greater detail: the system LF of dependent types, and the system F of
polymorphic types.
Chapter 12 presents another theory of domains based on the notion of
stable morphism. Stability was introduced by Berry, as an
approximation of the sequential behaviour of lambda-calculus. The
definition of a stable function formalizes the property that there is
always a minimum part of a given input needed to reach a given finite
output. We develop the theory along the lines of chapters 1 and 3: we
study stability on meet cpo's, dI-domains and event structures (and
coherence spaces), stable bifinite domains (with an application to the
construction of a retraction of all retractions), and continuous
L-domains.
Chapter 13 is devoted to linear logic. The simplest framework for
stability, coherence spaces, led Girard to the discovery of a new
resource-sensitive logic. In linear logic, hypotheses, or data are
consumed exactly once, and multiple uses (including no use) are
re-introduced by explicit connectives. Linear logic has a rich model
theory. We present only a few models: the stable model, Ehrhard's
hypercoherence model (which is closer to capturing sequential
behaviour), and Winskel's bistructures model (which combines the
continuous and the stable models). Also continuity can be recast in
the light of linear logic, as shown by Lamarche.
Chapter 14 addresses the semantic notion of sequentiality, which
is aimed at capturing sequential computation, as opposed to inherently
parallel computation. We start with Kahn-Plotkin sequential functions,
which do not lead to a cartesian closed category. But sequential
algorithms, which are pairs (function, computation strategy) yield a
model of PCF. They actually model, and are fully abstract for an
extension of PCF with a control operator catch. Sequential
algorithms lend themselves to a game interpretation. On the other
hand, a term model of PCF, from which a fully abstract model of PCF
is obtained by a quotient, can also be described in a
syntax-independent way using games. Games semantics therefore appear
as a powerful unifying framework, which is largely undeveloped at the
time this book is written.
Chapter 15 is an elementary introduction to the ideas of synthetic
domain theory via the category of partial equivalence relations
(per's). The category of per's is a useful tool in semantics; we
exhibit an interpretation of system F, of a type assignment system,
and of a subtyping system. Towards the interpretation of recursion we
introduce various reflective subcategories of per's. In this context
we prove a generalized Myhill-Shepherdson theorem.
Chapter 16 discusses some connections between the functional and
concurrent computational paradigms. As a main tool for this
comparison we introduce the basics of pi-calculus theory, a rather
economical extension of Milner's CCS. We show that this calculus is
sufficiently expressive to adequately encode a call-by-value
lambda-calculus enriched with parallel composition and synchronization
operators.
Two appendices provide the basic material on recursion theory and
category theory.
------------------------------------------------------------