SUO: *Date 24 Mar 2002 -- Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
SUO WG Members,
I am opening up a discussion of "Program Semantics" on the Ontology Sublist,
using the groundbreaking work "Algebraic Approaches to Program Semantics" by
Ernest G. Manes & Michael A. Arbib. One of the happier features of this text
for our immediate objectives is its demonstration of category theory being put
to work on concrete material applications in computer science, arising out of
what is by now a long-standing and fairly standard tradition of research and
development work on "category theory applied to computation and control".
By way of invitation, I copy the Preface here:
| Algebraic Approaches to Program Semantics
|
| Preface
|
| In the 1930's, mathematical logicians studied the notion
| of "effective computability" using such notions as recursive
| functions, lambda calculus, and Turing machines. The 1940's saw
| the construction of the first electronic computers, and the next 20
| years saw the evolution of higher-level programming languages in which
| programs could be written in a convenient fashion independent (thanks to
| compilers and interpreters) of the architecture of any specific machine.
| The development of such languages led in turn to the general analysis of
| questions of 'syntax', structuring strings of symbols which could count
| as legal programs, and 'semantics', determining the "meaning" of a
| program, for example, as the function it computes in transforming
| input data to output results. An important approach to semantics,
| pioneered by Floyd, Hoare, and Wirth, is called 'assertion' semantics:
| given a 'specification' of which assertions ('preconditions') on input data
| should guarantee that the results satisfy desired assertions ('postconditions') on
| output data, one seeks a logical proof that the program satisfies its specification.
| An alternative approach, pioneered by Scott and Strachey, is called 'denotational'
| semantics: it offers algebraic techniques for characterizing the denotation
| of (i.e., the function computed by) a program -- the properties of the
| program can then be checked by direct comparison of the denotation
| with the specification.
|
| This book is an introduction to denotational semantics.
| More specifically, we introduce the reader to two approaches to
| denotational semantics: the 'order semantics' of Scott and Strachey
| and our own 'partially additive semantics'. Moreover, we show how each
| approach may be applied both to the specification of the semantics of programs,
| including recursive programs, and to the specification of new data types from old.
| There has been a growing acceptance that 'category theory', a branch of abstract
| algebra, provides a perspicuous general setting for all these topics, and for
| many other algebraic approaches to program semantics as well. Thus, an
| important aim of this book is to interweave the study of semantics
| with a completely self-contained introduction to a useful core
| of category theory, fully motivated by basic concepts of
| computer science.
|
| Ernest G. Manes & Michael A. Arbib,
|'Algebraic Approaches to Program Semantics',
| Springer-Verlag, New York, NY, 1986.
And here is the thread so far:
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Program Semantics
01. http://suo.ieee.org/ontology/msg03884.html
02. http://suo.ieee.org/ontology/msg03885.html
03. http://suo.ieee.org/ontology/msg03886.html
04. http://suo.ieee.org/ontology/msg03887.html
05. http://suo.ieee.org/ontology/msg03890.html
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤