SUO: *Date 25 Mar 2002 -- Program Semantics
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
3 short notes and/or queries about program semantics --
leo, yes, arbib's little book 'brains, machines, mathematics' was
my first brush with this whole busy-beaver-ness, and is still the
best intro to a 'hood full of just such lambda-critical points as
those choice 3. and strachey is one of the most cherished books
on my shelf, if it were not for our need of some nuts and bolts --
bolts in the sense of categorically imperative arrows, of course --
in category theory, i would have started there first. maybe later.
john, as someone who is used to saying "chomsky-schützenberger"
in a single breath, i may classify linguists and computicians
a bit differently than your survey suggests, but never mind
that now, as there is work to do. but just as a matter of
fussy historical interest, i would appreciate it if you
gave me the reference where you ever saw chomsky use
the phrase "autonomous syntax", as he himself says
that he always said "independence of syntax" and
that specifically in the mathematical sense, say,
analogous to "orthogonal" -- and i would really
like to know someday how this story got started.
http://cs.anu.edu.au/publications/eljc/Volume_3/Html/v3i1f1.html
poc, 'tis true, those who know what being is can get right to ontology,
while those who still need a clue must purgate a while in epistemology,
by a legion of other names, "logic", "semiotic", or "theory of inquiry".
our charge and our charter do, of course, give us the deed to ontology,
but when you see a crew picking up picks and axioms and heading off to
the mountains to "dig for oil", like they say, well, you will tend to
classify them as bluffers or duffers or disney characters, and you'll
be itching to get back to your workbench and your drafting board to
work on "method" before you even think of trying to get down to
the "substance" of which this "reel buoy" is defictively made.
hi ho,
jon
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
> ¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
>
> 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
> 06. http://suo.ieee.org/ontology/msg03895.html
> 07. http://suo.ieee.org/ontology/msg03896.html
> 08. http://suo.ieee.org/ontology/msg03898.html
>
> ¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤