ONT Re: Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 31
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. An Introduction to Category Theory
|
| Going beyond the partial functions and multifunctions
| already considered, one might invent other useful notions
| of the input/output function from X to Y. In addition to the
| need to consider X, Y as "data structures", there are theoretical
| approaches to semantics in which all X, Y must carry further structure.
| Rather than embark on the misguided task of presenting an exhaustive list
| of present and future possibilities, we introduce 'categories' as a framework
| for semantics which possess so little structure that most models of semantics
| can be represented this way. Surprisingly, what structure remains can be
| extensively developed and there is a great deal to say.
|
| Category theory per se is tangential to this book. We discuss only a few
| topics which bear directly on our analysis of the "semantic category".
| In Section 2.1 we introduce the notion of a category which provides
| the bare bones of abstraction of the semantics of composition.
| Section 2.2 introduces the useful organizing principle of
| duality and relates it to isomorphisms and to initial and
| terminal objects. Isomorphism is self-dual and initial
| is dual to terminal. The uniqueness of initial objects
| has important instantiations in semantics, such as the
| uniqueness of a sequence defined by simple recursion.
| Zero objects are simultaneously initial and terminal
| and generalize the empty set in Pfn. To round out
| this introduction to category theory we present,
| in Section 2.3, the notion of product and the
| dual concept of coproduct which both find
| frequent applications throughout the book.
|
| With this we have all the category theory needed
| for our study of program semantics in Chapter 3.
| Further category theory is developed in Chapter 4
| as motivated by the issues raised by attempting to
| describe assertion semantics in a semantic category.
|
| When we turn to the study of data types in Part 3
| we shall need to call on further concepts from
| category theory -- functors, limits, and
| algebraic theories.
|
| The concepts in this chapter are quite abstract
| and may seem so even to readers with experience
| in pure mathematics. We encourage patience!
| Familiarity with the language will grow and
| the approach should come to seem increasingly
| natural with the applications to semantics in
| subsequent chapters.
|
| Manes & Arbib, AAPS, pages 38-39.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤