Preface
Why Another Book on Category Theory?
In the past ten years, several books have been published on category the-
ory either by computer scientists or having computer scientists as a target
audience (e.g. [6, 12, 22, 89, 105], to which a precious collection of little
gems [90] and the chapter cum book [91] should be added). Isn't the
working computer scientist spoilt with choice?
Although each of the above mentioned books presents an approach of its
own, there is one aspect in common in their view of computer science: the
analogy between arrows (morphisms) and (classes of) computations. This
"type-theoretic" or "functional" approach corresponds to a view of com-
puter science as a science of computation, i.e. a discipline concerned with
the study of computational phenomena where the focus is on the nature
and organisation of computations.
However, there is another view of computer science where the focus is,
instead, on the development of computer programs or systems. This is the
approach that supports, for instance, software engineering. From this point
of view, arrows do not capture computational phenomena, or abstractions
thereof,
but instead relationships between programs, or abstractions of
programs, that arise in the development of computer systems, for instance,
refinement of higher-level specifications into executable programs [100,
104],
and superposition of new features over existing systems [72].
Not surprisingly, this same difference in the points of view can be found
when logic is taken as a mathematical domain for formalising aspects of
computer science. The "computations as proofs" paradigm is the one that
corresponds to the "classical" application of category theory. Terms of the
logic correspond to objects in a category of programs whose morphisms
capture (partial) computations. From a logical point of view, the perspec-
tive that we take in this book is not centred on terms but on theories as
system specifications. Morphisms then capture what in logic is known as
"interpretations between theories", the cornerstone for the formalisation of
refinement in program development and other operations on specifications
and system designs [17, 82, 103, 104].
Category theory can also be presented as the branch of mathematics
that, par excellence, addresses "structure". As the introduction will try to
sfplds2015-04-14非常好的书，内容很好
