Lambda the Ultimate

In any case, I can't recommend DrScheme and PLT-Redex highly enough in exploring programming-language semantics.

On edit: I found this interesting paragraph in Building Interpreters With Rewriting Strategies:

There are different styles of operational semantics. In natural semantics supported by the CENTAUR system an expression is directly related to its value, possibly through the use of recursive invocations of the evaluation relation. In rewriting semantics, supported by many systems including ASF+SDF and ELAN, an expression is normalized by successive applications of reduction rules, which define a, generally small, modification of an expression. In the approach of syntactic theories, supported for example by the SL language, a set of reduction rules is extended with evaluation contexts that limit the positions in which reduction rules can be applied. Thus, evaluation contexts overcome a limitation of pure rewriting based semantics. Exhaustive application of reduction rules is usually not an adequate description of the semantics of a language. Therefore, the gap between evaluation strategy and rewriting strategy (provided by the rewriting engine) is usually filled by explicitly specifying an evaluation function instead of using pure rewrite rules.

Your Felleisen semantics isn't quite right, you have to also include the rule for actually applying an abstraction:

C[(Lx. e) v] → C[e[x := v]]

But otherwise you've got the right idea: you split rules from "search" rules that don't do anything but find the place where evaluation really ought to take place (Pierce's E-App1 and E-App2 rules) and the rules that actually take an evaluation step (Pierce's E-AppAbs); the former are factored into the definition of evaluation contexts and the latter become reduction rules.

The style Pierce uses is sometimes called "Plotkin-style small-step operational semantics" and Felleisen's is called "Felleisen-style context-sensitive reduction semantics." The advantage of the Felleisen style is that it's slightly more compact and highlights the actual evaluation rules as opposed to the search rules, and also (somewhat more importantly) it gives a name to the context that can be important in, for instance, giving semantics to call/cc. The Wright and Felleisen paper "A Syntactic Approach to Type Soundness" is probably a good place to start reading.

Anyway, a side question: how did you find that tech report? It's my master's thesis; my advisor and I put it in tech report form just because we wanted to cite it in another paper and we never did anything to publicize it and yet somehow several people seem to have found it, so I'm curious as to what's drawing people to it. (Incidentally, the first half of that paper was published in RTA 2004 and the second half is being published in the 2005 Scheme Workshop. Those papers are probably better things to look at for most purposes.)

There is a vague association in mind to some interesting work by Connor McBride The Derivative of a Regular Type is its Type of One-Hole Contexts.

I'm sure I've heard Graham Hutton mention a connection between small step and big step semantics via the 'zipper' functions talked about in the paper. They are the functions that plug in the contents of a hole (anti-derivative).

I'm not sure if a semantics in the style of calculus could be called simpler |:^) but something definately worth exploring.

So where do action semantics fit into the picture? From what I understand the purpose of action semantics is to move in the direction of using an abstract semantic notation to actually build computer executable systems (rather than using a notation for descriptive purpose).


I've read the claim (can't remember where) that just as context free grammer (BNF) is often used to produce actual parsers, action semantics can be used to generate actual compilers (which produce parse trees, do static type checking and implement relevant runtime services (garbage collection?))...any thoughts on that?