Operational vs. Denotational Semantics

Spent a little time this afternoon discussing several topics with LB and SR. One topic we touched on was our continuing efforts to understand the distinction between denotational and operational semantics - I continue to be surprised at just how hard it's proving to nail down the precise distinction.

Looking at the various scrawls on my whiteboard that are the only physical remnants of what was a fascinating discussion, I gave some more thought to the distinction, and I believe it can be described thus:

Operational : M ( P ) |= σ -> σ'
Denotational : M ( P ) |= κ -> P'

ie. In Operational semantics the meaning of a program is a transition function on a virtual machine.
in Denotational semantics the meaning of a program is a mapping from an initial basis to a new (simplified) program.

Now this is confused by most operational semantics being "small-step", where the meaning is defined via structural recursion on the abstract grammar:

M ( ρ ) |- σ -> M (ρ') σ' { the meaning of an AST production is a transition function from an initial VM state to the meaning of a (simplified) production applied to a new VM state. }

Which end up looking very similar to denotational semantics as denotational semantics are normally defined via structural recursion.

But even for the similarity there remains the core distinction (as I understand it) - Denotational Semantics are defined in terms of a reduction-semantics from program+basis to a simplified program (although normally a program in a different, mathematically tractable language such as the lambda-calculus) whereas Operational Semantics are defined in terms of a transition-semantics from a program+initial-state to a new state (although normally a state extended with function-values defined in a mathematically tractable language such as the lambda-calculus).

Now of course Interpreter Semantics is a whole different kettle of fish, and of course leaves you facing the 'turtle problem' - you can try for 'turtles all the way down' if you like, but once you hit the metal you've pretty much lost the point of a semantics in the first place. I must admit admiring the way ECMAscript handled it - an interpreter semantics in SML, which has an operational semantics of its own avoiding the problem.