Armchair philosophy

I was reading recently a fun paper by Wesley Phoa, Should computer scientists read Derrida? [pdf]. I was attracted by what seemed to me a preposterous title, being quite sure the paper is a parody. Instead, I found myself confronted with a serious, beautifully written and thoughtful paper.

I will not comment on the paper itself because it deserves to be commented on seriously. I’ll just say that although I liked it quite a lot and although I recommend it as an excellent and thought-provoking read, I didn’t quite agree with its conclusions. Yet I was intrigued by the question. So I’ll have a go at giving a different answer.

First, we need to frame the entire history of semantics of programming languages in a blog post and then lets see how we can fit Derrida in there. We need to start with logic, of course.

There are two kinds of semantics (to use JY Girard’s terminology): essentialist and existentialist. I disclose that I am 10% essentialist and 90% existentialist, so that the reader can calibrate my account taking personal bias into consideration.

Essentialists take after Tarski and aim to understand language by expressing meaning into a meta-language. So that the proposition the grass is green is true if the grass is indeed green. The meaning of grass is ‘grass’, of is is ‘is’, etc. To the uninitiated this may seem funny, but it is serious business. In formal logic symbols get involved, so it seems less silly. The proposition A∧B is true if A is true and B is true, so the meaning of “” is ‘and’.

In programming languages this approach is the oldest, and is called “Scott-Strachey” semantics according to the two influential researchers who promoted it. It is also called ‘denotational’ (because symbols ‘denote’ their meaning) or ‘mathematical’ (because the meaning is expressed mathematically). To map symbols into meaning it is conventional to use fat square brackets 〚  and 〛.

So what is the meaning of the ‘2+2‘? It is 〚2+2〛 = 〚2〛 + 〚2= 2 + 2 = 4. Students are sometimes baffled by this interpretation even though we do our best to try to make things clearer by using different fonts to separate object and meta-language. (Because this blog is written in a meta-meta-language I need to use even more fonts.) It is easy to laugh at this and some do by calling it, maliciously, ‘renotational pedantics’. Well, much of it perhaps is, but not all of it. It is really interesting and subtle when ascribing meaning to types, i.e. things like 〚intint〛 which can be read as ‘what are the functions from ints to ints describable by some programming language’.

In programming language semantics, and in semantics in general, the paramount question is that of equivalence: two programs are equivalent if they can be interchanged to no observable effect. In an essentialist semantics A is equivalent to B if 〚A〛=〚B〛. This justifies the name quite well, since A and B are ‘essentially’ the same because their meanings are equal. Above we have a proof that 2+2 is equivalent to 4, because 〚2+2〛 =〚4〛= 4.

Essentialism has come under some fierce criticism. Wittgenstein, a promoter of it, famously reneged it. Famous contemporary logicians JY Girard (The Blind Spot) and J Hintikka (Principles of Mathematics Revisited) both attack it viciously (and amusingly) because of its need for a meta-language: what is the meaning of the meta-language? “Matrioshka-turtles” is what Girard calls the hierarchy of language, meta-language, meta-meta-language, etc. — it goes all the way down to the foundations of logic, language and mathematics.

Existentialism takes a different approach: language is self-contained and we should study its dynamics in its own right. Wittgenstein uses the concept of ‘language games‘ both to understand the properties of language (which are still called ‘meaning’ although the non-essentialist reading of ‘meaning’ is a bit confusing) and to explain how language arises. For some reason existentialist approaches to meaning always end up in games. Lorenzen used games to give a model theory of logic and Gentzen used games to explain proof theory. Proving something to be true means winning a debate. When something is true a winning strategy for the debate-game exists.

In programming languages the first existentialist semantics was operational semantics, which describes meaning of language in terms of itself, by means of syntactic transformations. It is intuitive and incredibly useful, but it is quite simplistic. Most importantly, it does not give a good treatment of equivalence of programs. It can only formalise the definition of equivalence: A and B are equivalent if for all language-contexts C[-] such that C[A] and C[B] are executable programs, C[A] and C[B] produce the same result. It is not a very useful definition, as induction over contexts is so complicated as to be useless.

Something very nice about programming language semanticists is that we’re not dogmatic. The battles over ‘which one is better’, denotational (essentialist) or operational (existentialist), were non-existent, largely restrained to friendly pub chats. In fact one of the first great open problems was how to show that the two are technically equivalent (the technical term is ‘fully abstract’ for a denotational model which captures operational equivalence perfectly). Milner, who coined the term, also showed how an essentialist (denotational) semantics can be constructed (where the word ‘constructed’ is not necessarily meant constructively) out of an existentialist (operational) semantics. I am not sure how aware philosophers of language are of this construction, because its implications are momentous. It establishes the primacy of existentialist semantics and reduces essentialist semantics to a mathematical convenience (publishing a research paper on programming language semantics without a proof of ‘adequacy’ is a serious challenge).

Milner’s construction is not very useful (which takes nothing away from its importance) so finding more palatable mathematical models is still important, and proving ‘full abstraction’ is the ultimate technical challenge. This turned out to be very hard, but it was eventually done (for many languages), also using the ‘game semantics‘ I mentioned above.

Curiously, in programming language semantics games were introduced as a denotational (essentialist!) semantics: a program denotes a strategy rather than an operational (existentialist) semantics. In fact, some technical aspects of the first game models [see Inf. Comp. 163(2)] made PL Curien (and others) complain that game models were too much like Milner’s construction of a denotational semantics out of an operational semantics [link].

Again, this full abstraction result was not the intended goal: we wanted a fully abstract model of PCF for short. But Loader’s later result settled the question negatively: he showed that the observational equivalence for PCF is not effective. As a matter of fact, the game-theoretic models of PCF given in 1994 by Abramsky, Jagadeesan, and Malacaria (AJM), and by Hyland and Ong (H0) offer syntax-free presentations of term-models, and the fully abstract model of PCF is obtained from them by a rather brutal quotient, called “extensional collapse”, which gives little more information than Milner’s original term model construction of the fully abstract model.

However, these technical issues were only manifest in the PCF model and most subsequent models, starting with Abramsky and McCusker model of Algol were syntax-free, complaint-free, fully abstract models.

Still, this is somewhat of an anomaly, at least historically and I think methodologically. Things were, however, set right by J Rathke and A Jeffrey who came up with a neat combination of operational and game semantics which they called ‘trace semantics‘. P Levy renamed this to ‘operational game semantics’, although I think for historical reasons it would be nice if it was all called just ‘game semantics’. Unlike vanilla operational semantics, operational game semantics offers a neat treatment of equivalence. Two programs A and B are equivalent if whatever ‘move’ one can make in its interaction with the environment the other can match it (the technical term is ‘bisimilar’). Also, unlike vanilla game semantics operational game semantics doesn’t really need the operational semantics.

What about Derrida then?

Broadly speaking, Derrida makes a critique (called deconstruction) of existing approaches to understanding language and logic on the basis that they ‘ignore the context’:

… [deconstruction is] the effort to take this limitless context into account, to pay the sharpest and broadest attention possible to context, and thus to an incessant movement of recontextualisation. The phrase … ‘there is nothing outside the text’, means nothing else: there is nothing outside the context.

This is obviously a statement exaggerated for rhetoric effect, but it’s not silly. In understanding language, context is indeed essential. In understanding formal logic, however, I don’t see how context plays a role, because the context is known. It is sort-of the point of formalisation to do away with the difficult questions that context raises. How about programming then? Is context important? Yes, it is. I’ve been saying this for a while, including on this blog. Realistic programming languages exist in a complex and uncontrollable context. Take these two little programs in simplified C-like languages.

int f() { int x = 0; g(); return x; } 
versus
int f() { g(); return 0; }

Are they equivalent? We don’t know what g() is. Importantly, we don’t know if it’s even a C function (C has a foreign function interface). If g() was “civilised”, then the two are equivalent because a civilised function g() has no access to local variable x. However, g() may be uncivilised and poke through the stack and change x. It’s not hard to write such a g() and hackers write uncivilised functions all the time.

This may seem like a hopeless problem, but it’s not. In fact, operational game semantics can model this situation very well. I call it system-level semantics, and it’s game semantics with a twist. In game semantics we model program+environment as a game with rules, which embody certain assumptions on the behaviour of the environment. In a system-level semantics the game has no rules, but it has knowledge. The environment is an omnipotent but not omniscient god, sort-of like Zeus. We can hide things from it. This is the same principle with which the Dolev-Yao attacker model in protocol security operates.

This does not necessarily lead to chaos, just like Derrida’s deconstruction need not degenerate in relativism:

… to the extent to which it … is itself rooted in a given context, … [deconstruction] does not renounce … the “values” that are dominant in this context (for example, that of truth, etc).

The point is that any enforcement of properties are up to the program and cannot rely on the context. In a game, the program should be able to beat any opponent-context, not just those behaving in a certain way (just like a security protocol).

A system-level semantics of C can be given where local variables are not hidden (a la gcc), and in such a semantics the two programs above are not equivalent. But a system-level semantics of C can also be given where local variables are hidden (e.g. via memory randomisation), which makes the two programs equivalent in any context. In a civilised context both semantics would be equivalent, but in an unrestricted context they are different.

So should computer scientists read Derrida? No. However, like Derrida urges, they should worry more about context.

About Dan Ghica

Reader in Semantics of Programming Languages // University of Birmingham // https://twitter.com/danghica // https://www.facebook.com/dan.ghica
This entry was posted in game semantics, system level semantics. Bookmark the permalink.

11 Responses to Armchair philosophy

  1. Uday Reddy says:

    So, you are saying, basically, that logic is boring and functional programming boring. But you know better. Imperative programming blows your mind off!

    • Prakash Panangaden says:

      What are you trying to say here? There is nothing outside the text, but in this case there is nothing inside the text.
      Cheers
      Prakash

      • Uday Reddy says:

        I was responding to the point of “renotational pedantics”. If you take a language that very very closely reflects its intrinsic meaning, then defining its “meaning” doesn’t say anything significant. Hence the idea comes about that denotational semantics is “renotational pendantics”.

        But when you get to languages that are sufficiently rich and deep, understanding their “meaning” involves enormous amount of effort. Their denotational semantics is in no way “pedantics.” Rather, it is theory-building of the kind done in, say, Physics. I have a feeling that mathematics itself is largely theory-building of this kind. But mathematicians don’t bother to explain what they are building theories of. So, the outsiders don’t understand what they are doing. Computer Science should aspire to be Physics, not linguistics or philosophy.

      • Uday Reddy says:

        To make the connection with Physics concrete, here is a simple view. (The full treatment will need its own blog post.)

        A program is a machine that has a behaviour. Semantics builds a theory of programs for predicting that behaviour, so that we can use it in building the machines. I am entirely happy to have many theories of programs, each of which might give its own insights or suit people of different tastes.

        The point of games semantics is self-evident. Its strengths and weaknesses are also clear on a moment’s thought. I don’t see how Wittgenstein or Derrida will make a difference to this.

      • Dan Ghica says:

        It is not self-evident. We have three kinds of semantics (operational, denotational, games) which are coming from different philosophical traditions. They address the same problem, specifying machine behaviour via programs, but they do it in very different ways. Is it really so clear what the strengths and weaknesses of each approach is? I very much doubt it.

      • Uday Reddy says:

        Reply to Dan:

        No, I don’t see operational semantics and denotational semantics as addressing the same problem. Operational semantics “specifies” the behaviour of complete programs, as you say. As a programmer, I don’t need it at all because I can run the programs on a computer and see for myself what their behaviour is. On the other hand, denotational semantics predicts the behaviour, not only of complete programs, but individual program components under all possible contexts (you must like that word!). As a programmer, I can use denotational semantics for reasoning, whereas operational semantics on its own is completely useless. The two are as different as night and day.

      • Dan Ghica says:

        Obviously, our views of semantics are quite different.

  2. I completely agree with the critique of “renotational pedantics”. It’s all too easy to end up with rules such as

    [[ if B then C1 else C2 ]] = cond ([[B]], [[C1]], [[C2]])

    where cond is the function defined by

    cond ([[B]], [[C1]], [[C2]])
    = [[C1]] if [[B] = true
    = [[C2]] else

    This double renotation has told us nothing other than “if” is “if”, “then” is “then” and “else” is “else” – which is exactly why the language designer chose those keywords.

    But denotational semantics as we know it has a much subtler role in that the notations and denotations can be rather different in nature. In the Scott-Strachey semantics the denotations are points of a topological space, and in the point-free version as worked out in detail in Abramsky’s thesis, they become models of an observational theory. Thus we see two different levels of observation: the coder and the computer have access to the source code, but the user doesn’t. Topologically, the user’s run-time information about the code is restricted to open properties.

    For example, the points of [[ int -> int ]] are explained in terms of observations for individual function calls: supply an argument and observe a result. The semantics is not simply “->” is “->”, since the topological “->” (for function spaces) is non-trivial. One has to work hard to find a suitable cartesian closed category of spaces and show how -> works with respect to the presenting structure.

    “Observation” here is a simple precursor to more general ideas of interaction – there was already some of this in the idea of observing a function by supplying an argument and observing the result. In Dan’s example, you see how the semantics depends on the interactional power of the environment (the function g), for example whether it can manipulate the stack or not.

    To summarize, the need for an explanation as semantics arises from this disparity in observational or interactional power. It may well be that pure topology is too limited to deal with general interactions, but it is still offering an explanation deeper than renotational pedantics.

    • Dan Ghica says:

      I agree, and I hope what I said in the post did not seem in contradiction with what Steve said.

      But, as I said, actually I don’t think the “renotational pedantics” criticism is entirely fair (it’s funny though). The fat brackets go from text to math and we could call it a coincidence that the meta language is so similar in parts with the object language. There are still big essential differences, e.g. interpretations of modalities or quantifiers, which are nontrivial.

  3. Mike Gordon says:

    Any thoughts on how Ketan Mulmuley’s work fits into your story
    (http://dl.acm.org/citation.cfm?id=1398512.1398551)?

    • Dan Ghica says:

      I didn’t know the paper! It seems strangely forgotten, it has very few citations (at least on Google scholar). I definitely need to have a look at it.

Leave a Reply

Your email address will not be published. Required fields are marked *

*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>