Re: SUO: *Date 24 Mar 2002 -- Program Semantics
Hi, Jon,
M. Arbib has done much in formal languages, theory of computation, for
quite some time. Note that denotational semantics is really
model-theoretic semantics. Scott and Strachey's text (circa 1977) opened
the field up a bit for mainstream computer science. Montague (1968,
etc.) opened the field up a bit for formal semantics in linguistics --
before which there wasn't much in the way of formal semantics, by the
way. Category theory is a very general useful tool. It however needs
applications at much lower levels of abstraction in general, so I am
interested in this text just for that purpose (applications mostly are
still pretty theoretical, in my knowledge: type theory, denotational
semantics of programming languages, program specification, etc.) I hope
the IFF can bring it down to a reasonable "ontology" level (which itself
is probably fairly abstract for most of the human race).
Leo
Jon Awbrey wrote:
>
> ¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>
> 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
>
> ¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
--
_____________________________________________
Dr. Leo Obrst The MITRE Corporation
mailto:lobrst@mitre.org Intelligent Information Management/Exploitation
Voice: 703-883-6770 7515 Colshire Drive, M/S W640
Fax: 703-883-1379 McLean, VA 22102-7508, USA