Hacker News new | ask | show | jobs
by fadmmatt 5950 days ago
If you're wondering what things like "operational" and "denotational" mean and what they look like in code, I created this article for my compilers students:

http://matt.might.net/articles/writing-an-interpreter-substi...

Short version:

* A denotational semantics is a function M : Program -> (Value -> Value) that maps a program to a mathematical function.

* An operational semantics is a relation (=>) between consecutive machine states. That is, if state => state' holds, then the machine transitions from state to state'.

* The relation in a "big-step" operational semantics need not be decidable. Big-step relations are usually recursive.

* The relation in a "small-step" operational semantics must be decidable.

* When you implement a transition relation, =>, it's usually implemented as a function. That is, if you have a relation R \subseteq State x State, you can encode this as a "transfer function" f : State -> 2^State.
1 comments
anonymousDan 5950 days ago
* Does the transfer function not need to take some input other than the state?

* Can you convert a denotational semantics to an operational semantics (and vice versa)? Is there any value in doing this?

link
fadmmatt 5950 days ago
* Does the transfer function not need to take some input other than the state?

It depends on how you're encoding things. You might want to supply the I in I/O as an extra parameter to the transfer function.

Or, you could kick off the execution with the state containing a (possibly infinite) sequence representing all of the I/O events it will encounter during execution.

For the most part, transfer functions operate on just states.

* Can you convert a denotational semantics to an operational semantics (and vice versa)? Is there any value in doing this?

Yes, Olivier Danvy has a strong research program in this area. He has a battery of techniques that allow you to (almost) mechanically calculate one kind of semantics from another.

In many cases, calculating an operational semantics from a denotational semantics is the easiest way to prove their equivalence.

link