[FOM] Brouwer on mathematical operations: operationalism in mathematics
Vaughan Pratt
pratt at cs.stanford.edu
Mon Dec 29 03:21:04 EST 2008
Thomas, I'm very much looking forward to your book. Although I worked
out the main ideas underlying dynamic logic in April 1974, a year before
the journal TCS began publication, hopefully that doesn't disqualify me
as one of the "surviving TCS people" you referred to. Here's more
detail than you probably want as to what makes my strong focus on
denotational semantics take precedence over any interest I might have
ever had in operational "semantics," whatever that means.
As a freshly minted Ph.D. and soon-to-be MIT faculty in 1972 focusing on
algorithms and combinatorics (but with many side hobbies that I then
considered unsuited to the light of publication), my first exposure to
the mysteries of operational semantics was at the Annual ACM Conference
for 1972, where Turing Award recipient Edsger Dijkstra praised "The
Humble Programmer" and John Reynolds spoke on "Definitional interpreters
for higher-order programming languages." A decade later Gordon Plotkin
produced "A Structural Approach to Operational Semantics," DAIMI FN-19,
Aarhus U., 1981 (the "Aarhus Notes"). Retrospective views of both
authors on their seminal contributions are titled respectively
"Definitional Interpreters Revisited," in Higher-Order and Symbolic
Computation 11:4 355-361 (1998), and "The Origins of Structural
Operational Semantics," in Journal of Logic and Algebraic Programming,
60/61, 3-15 (2004).
I confess to having had a hard time with operational semantics from the
get-go. While I understood Reynolds' 1972 talk perfectly at some
arithmetic level, having written both compilers and interpreters myself
and pondered their meaning, I was unable to relate to it as a research
contribution of any kind. My development of dynamic logic two years
later, as part of an MIT course on logics of programs following on the
heels of courses by Oxford's Joe Stoy (visiting MIT for 18 months to
wean us off the Vienna Definition Language) and earlier Jack Dennis and
Jack Wozencraft, was carried out entirely in the denotational tradition.
Had it not been, I would not have seen the point of publishing it, as
Floyd's and Hoare's axiomatic approaches to program verification seemed
to serve the needs of programmers perfectly well without the distraction
of semantics.
(I mean "denotational semantics" in the broad sense of model theory; in
those days the term tended to be identified with what was sometimes
called Scottery and is nowadays referred to as domain theory, even
though Scott himself had the broad sense in mind when using the term.)
The need I felt was unmet was the sort of model theory for program
verification that had long since been taken as a *sine qua non* of first
order logic. While this need didn't strike me as terribly high on any
computer scientist's list of druthers, after mulling it over for two
years I tentatively presented the concept at FOCS'76 (along with a paper
on synchronizing faulty processes coauthored with Ron Rivest, who had
that summer with S and A, all at MIT, invented RSA but not in time for
that FOCS). Nowadays people view my paper as combining Kripke
structures and regular expressions in a natural way, but my own take on
it was as the first serious attempt at a model theory for Floyd-Hoare
logic (whence my title "Semantical Considerations on Floyd-Hoare Logic").
To my surprise there were a few in the FOCS audience who actually did
appreciate the model theory in my paper, in particular Richard Ladner at
the University of Washington, who along with Michael Fischer worked out
the propositional counterpart of my first order setup during the
following six months. Others taking an interest around that time
included of course my student David Harel, as well as Michael Paterson,
Rohit Parikh, Albert Meyer, Krister Segerberg, Dov Gabbay, Fran Berman,
Karl Abrahamson, Dexter Kozen, and others I'm blanking on just now.
Being more of an algorithmist than a logician at heart, I quickly
switched my allegiance from first to zeroth order on account of its
relatively feasible computational complexity, while David Harel went on
to produce a thesis (graduating from MIT in two years and taking up a
postdoc at IBM Yorktown Heights) and then a book on the original first
order version.
Between 1976 and 1980 I worried from time to time about whether
operational semantics was something definable with the precision of
denotational semantics. I kept coming back to the notion that
operational semantics was a misnomer: there were only operational
*methods*, whose meaning was defined precisely by denotational semantics.
Today I would say that an operational approach qualifies as a semantics
when it can be set up as some sort of free algebra or cofree coalgebra.
While I'm sure many are quite at home with the idea that a
definitional interpreter can be a semantics, I expect I will go to my
grave still unable to see things this way.
> Category theory is thoroughly operationalist in conception
The difference between ZF set theory and category theory is that the
former is based on a binary relation of membership, the latter on a
partial binary operation of composition. Whatever qualifies the latter
as operational for you should surely qualify ZF as equally operational.
> and
> much of the thinking in theoretical computer science is operationalist.
> They don't use the word, but that's what it is. All the Abstract-Data-Type
> stuff is operationalist.
We're urgently in need of a definition of "operationalist" at this
point. To me abstract data types are entirely denotational, and were
formulated with that as the objective.
> Operationalism in physics has a bad reputation.
Perhaps my inability to accept operational methods as furnishing a
semantics comes from my earlier training as a theoretical physicist.
> It's very striking
> that not of the philosophers who take an interest in philosophy of
> mathematics ever consider operationalist views of mathematics. I suspect if
> they looked more closely at what they call *structuralism* they would
> discover that quite a lot of what they think is structuralism is actually
> operationalism.
Without more attention to definition this line of thought is unlikely to
lead to any sort of a consensus as to what is actually being claimed here.
Vaughan Pratt
More information about the FOM
mailing list