[FOM] Brouwer on mathematical operations: operationalism in mathematics

[Vaughan Pratt]

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