19
$\begingroup$

In Anthony Aaby's "Introduction to Programming Languages" section on Semantics, he makes the following observation:

Much of the work in the semantics of programming languages is motivated by the problems encountered in trying to construct and understand imperative programs---programs with assignment commands. Since the assignment command reassigns values to variables, the assignment can have unexpected effects in distant portions of the program.

This strikes me as a remarkable admission, that allowing side effects would motivate a major part of the work in semantics.

How does the existence of side effects in a programming language impact the ability to map a program to a computational model? Are there approaches to managing state that can improve this process while still allowing side effects?

$\endgroup$
  • $\begingroup$ Should this be tagged as a soft-question? Since "much of the work in semantics [...] is motivated by [side-effects]", surely you can't expect a short and rigorous answer. $\endgroup$ – Radu GRIGore Aug 27 '10 at 10:06
  • 1
    $\begingroup$ @Radu: On MO, this would probably be tagged [big-picture], which mostly are not [soft-question] or CW there. $\endgroup$ – Charles Stewart Aug 27 '10 at 10:33
  • $\begingroup$ The tag big-picture is even better. I forgot about it. $\endgroup$ – Radu GRIGore Aug 27 '10 at 10:51
  • $\begingroup$ Good suggestion; I added the tag. $\endgroup$ – Shane Aug 27 '10 at 11:39
18
$\begingroup$

Building on Charles's answer, the main difficulty in the theory of programming languages is that the natural notion of equivalence of programs is typically not strict equality either in the most straightforward mathematical semantics you can give, or in the underlying machine model. For example, consider the following bit of Java-like code:

Object x = new Object();
Object y = new Object();
... some more code ...

So this program creates an object and names it x, and then creates a second object named y, and then continues executing some more code. Now, suppose that a programmer decides to flip the order of allocation of these two objects:

Object y = new Object();
Object x = new Object();
... some more code ...

Now, ask the question: does this refactoring change the behavior of the program? On the one hand, on the underlying machine, x and y will be allocated at different locations in the two runs of the program. So in this sense, the program behaves differently.

But in a Java-like language, you can only test references for equality, and not for order, so this is a difference that the "some more code" cannot observe. As a result, most programmers will expect that reversing the order will make no difference to the final answer, and most compiler writers expect to be able to perform reorderings and optimizations on this basis. (On the other hand, in a C-like language, you can compare pointers for ordering, by casting them to integers first, and so this reordering does not necessarily preserve observable behavior.)

One of the central questions of semantics is to answer the question of when two programs are observably equivalent. Since our notion of observation depends on the features of the programming language, we end up with a definition like "two programs are equivalent when no client program can compute different answers based on receiving those programs as inputs." The quantification over all client programs is what makes this question difficult -- it seems like you end up having to say something about all possible client programs to say something about two particular pieces of code.

The trick with denotational semantics is to give a mathematical interpretation that lets you avoid this universal quantification -- you say that the meaning of a piece of code is some mathematical value, and you compare them by checking to see if they're mathematically equal or not. This is local (ie, compositional), and does not involve quantification over all possible clients. (You do need to show that the denotational semantics implies contextual equivalence for it to be sound, of course. When it is complete -- when denotational equality is exactly the same as contextual equivalence, we say the semantics is "fully abstract".)

But means that you need to ensure that the denotational semantics validates those equivalences. So for this example, if you wanted to give a denotational semantics for this Java-like language, you need to ensure not just that calling new takes a heap and gives you back a new heap with the newly-created object, but that the meaning of the program is invariant same under all permutations of the input heap. This can involve quite complex mathematical structures (eg, in this case working in a category which ensures everything works modulo a suitable permutation group).

$\endgroup$
  • $\begingroup$ "two programs are equivalent when no client program can compute different answers based on receiving those programs as inputs." I'm confused by this. If you have a program X and a client program Y, then I take it to mean that Y 'calls into' X. But then you seem to say that Y reads the text of X as input, in which case I'd hardly call Y a 'client' of X. Could you please clarify? $\endgroup$ – Radu GRIGore Aug 27 '10 at 10:20
  • 1
    $\begingroup$ By "client of X", I just mean the same as "program context", which is just a "larger program which contains X as a subterm". $\endgroup$ – Neel Krishnaswami Aug 27 '10 at 21:52
  • $\begingroup$ So you use 'X is a client of Y' interchangeably with 'X reads Y as input' because you think of X as a lambda applied to Y? It makes sense, but it's a little twisted when you talk about Java. :) $\endgroup$ – Radu GRIGore Aug 31 '10 at 9:00
  • 1
    $\begingroup$ @RaduGRIGore: program context means something else. You are reading correctly the post, but if X reads the source code of Y as input (which is how I interpret the post), you can distinguish every two syntactically different programs; instead if Y is a lambda function on X, you can distinguish too few programs. Neel's comment about "program context" is the correct definition: a program context Y is a program with a hole in its AST, where you can place (meaningfully) two different program fragments X1 and X2. $\endgroup$ – Blaisorblade Apr 30 '12 at 17:28
  • $\begingroup$ @NeelKrishnaswami: could you maybe clarify what you mean in the post? You can just continue using your example and talk about a program where you can insert one or the other fragment. $\endgroup$ – Blaisorblade Apr 30 '12 at 17:30
12
$\begingroup$

There are of course ways of dealing with effects in (denotational) semantics. For example, we can use Eugenio Moggi's idea that computational effects are monads (this idea has also been used in the design of Haskell). One of the problems with this is that monads are hard to combine. Gordon Plotkin and John Power suggested a refinement of Moggi's monads to Lawvere theories, or algebraic theories as they are also called, which encompasses algebraic effects (most common effects are algebraic, such as state, I/O, non-determinism, but continuations are not). For a comprehensive treatment, see Matija Pretnar's thesis.

I should also mention the possible worlds semantics for local state, developed by Frank Oles and John Reynolds (sorry, can't find a better link, this stuff is from 1982), which predates Moggi's monads. They used categories of presheaves to provide a semantics of an algol-like language which correctly modeled many aspects of local state (but not all of them, I think the model allowed snapback, but maybe my memory serves me wrong).

$\endgroup$
  • 1
    $\begingroup$ Yes, the functor category semantics didn't validate all of the Meyer-Sieber equivalences. Peter O'Hearn and Robert Tennant developed a parametric version of the functor-category semantics in the mid-90s which (IIRC) got all of the Meyer-Sieber examples, but I don't know if it was fully abstract or not. $\endgroup$ – Neel Krishnaswami Aug 29 '10 at 9:32
  • $\begingroup$ O'Hearn and Tennent model is not fully abstract. That is discussed in the paper itself. But the refinement by O'Hearn and Reynolds using linear lambda calculus is fully abstract up to second-order. It breaks for third-order, examples being the equivalences studied by Ahmed, Dreyer, Birkedal et al. $\endgroup$ – Uday Reddy Feb 28 '12 at 21:38
12
$\begingroup$

Matthias Felleisen presented a compelling solution to the side effects problem in semantics in his series on "Syntactic Theories of Control and State."

That line of work resulted in the CESK machine, a simple abstract machine framework capable of concisely modeling functional, object-oriented, imperative and even logic languages. The CESK framework handles not just side effects, but also "complex" control constructs like exceptions, continuations, laziness and even threads.

The CESK machine, and small-step operational semantics more broadly, have been the de facto standard in programming language theory for about two decades.

In short, a CESK machine is a small-step machine with four components to describe every machine state: the control string (a generalization of the program counter), the environment, a store (also called the heap) and the current continuation.

The environment maps variables to addresses; the store maps addresses to values.

This makes it straightforward to model mutable variables: just change the value at its address.

It also makes it easy to model pointers and dynamic allocation: just make store addresses first-class values.

In a similar fashion, first-class continuations result from making them addressable values.

$\endgroup$
6
$\begingroup$

How does the existence of side effects in a programming language impact the ability to map a program to a computational model?

It doesn't necessarily make it difficult, but it does impose restrictions on the way the semantics of larger expressions can be constructed out of smaller ones. It can interact very badly with certain other programming constructs, for instance, if one wants to give a Scott-style denotational semantics for a language allowing assignment of higher-order functions to global references.

It is not simply side effects like state that cause the trouble. Simple imperative languages such as Dijkstra's guarded command language have these kinds of side effects, and have nice semantics. Trouble arises with extensions of the lambda-calculus with the kind of operational semantics expected of programming languages even in the absence of side effects: the earliest, Plotkin's PCF, was given denotational models relatively early, but the semantics were not fully abstract, meaning that the denotational semantics was overly general, not exactly corresponding to their operational semantics. PCF finally recieved a fully abstract denotational semantics in the late 1980s with game semantics, which is not at all like Scott's order-theoretic semantics. Concurrency still has not received a fully adequate denotational treatment.

Many question the importance of this kind of semantics. We can always provide some kind of operational semantics, even if that "semantics" is just the program source and the names of some machines that have compiled and run the program: for this reason Strachey condemned operational semantics. But Plotkin's structural operation semantics has shown how operational semantics can be separated from machine models, and Pitt's work has shown how such semantics can support similar reasoning about programs and programming languages to denotational semantics. Thus operational semantics is a viable alternative to denotational semantics, and have been applied with success to a substantial number of programming languages such as Standard ML.

Are there approaches to managing state that can improve this process while still allowing side effects?

To some extent, difficulties providing semantics correspond to the difficulty of providing powerful programming languages that behave in the way one would expect. Pragmatically motivated design decisions —such as avoiding the use of global state together with concurrency, typically through message-passing concurrency— make it easier to provide semantics.

$\endgroup$
  • $\begingroup$ Scott's PCF does not have state and neither is it Scott's, is it?See en.wikipedia.org/wiki/… $\endgroup$ – Andrej Bauer Aug 30 '10 at 18:57
  • $\begingroup$ @Andrej: Err, quite, given that Luke Ong supervised my D.Phil, I should not make that mistake. I posted a teaser-summary of Milner's PCF and Scott's LCF that is more ... succint than WP's as an LtU story: lambda-the-ultimate.org/node/2196 It occurs to me that you might have access to the missing Scott (1969) manuscript... $\endgroup$ – Charles Stewart Aug 31 '10 at 11:47
  • $\begingroup$ That would be Plotkin's PCF, I think :-) I can try to get hold of the manuscript, but I don't actually have it. $\endgroup$ – Andrej Bauer Aug 31 '10 at 13:18
  • $\begingroup$ But the point remains that PCF doesn't have state. What "reason" are you saying that Strachey to condemn operational semantics? It wasn't apparent to me. The last paragraph contradicts what you said earlier, viz., guarded commands have nice semantics but PCF doesn't! $\endgroup$ – Uday Reddy Feb 28 '12 at 19:26
  • $\begingroup$ @Andrej, Uday: I've fixed my post, less than three years later. $\endgroup$ – Charles Stewart May 16 '13 at 8:08

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.