6 ms·

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: h

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-substitution-denotational-big-step-small-step/ 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.

anonymousDan 17y 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?
- fadmmatt 17y 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.

anonymousDan 17y 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?

fadmmatt 17y 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.