6
$\begingroup$

I'm trying to sort out in my mind the different ways of assigning semantics to a programming language. There are two main methodologies: operational semantics and denotational semantics (I asked a previous question on the relationship between the two).

It seems to me that an operational semantics is the same as defining a dynamics for the language - that is, defining how programs are evaluated. I know two different ways of doing this: equational and structural.

A structural dynamics defines evaluation via a system of transition rules (I believe beta reductions are the canonical example). An equational dynamics only specifies reductions indirectly, by defining when one expression is equal to another. (I'm going through the trouble of defining these terms because I am uncertain how standard the terminology is).

But I can't figure out why both systems are needed. I personally prefer structural dynamics, but it feels very subjective. What are the advantages and disadvantages between the two systems?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
8
$\begingroup$

What you call "equational dynamics" is not actually an operational semantics, it's an equational theory. As you note, equations by themselves do not tell us how to run programs. However, they are needed because we want to express the idea of program equivalence. For instance, an optimizer replaces a piece of code with an equivalent piece of code (which is hopefully more efficient). But what does "equivalent" mean here?

We can use observational equivalence: two programs are equivalent if we can make exactly the same observations about them. In other words, they behave the same way. This kind of equivalence is defined using operational semantics.

An alternative is to start by prescribing equivalences. We want certain programs to be equivalent, usually because we have some mathematical understanding of how things are supposed to work. For instance $\beta$-reduction $(\lambda x . e_1) e_2 = e_1[e_2/x]$ is an equation which expresses the mathematical meaning of $\lambda$-abstraction. In practice is is often easier to come up with equations than with an operational semantics. (For instance, when Matija Pretnar and I worked on Eff, we knew exactly what the equations were because we were actullay trying to turn equational theories into a programming language. Also, when Alonzo Church came up with the $\lambda$-calculus he wrote down equations that expressed the mathematical properties of functions and function application.) The problem then is to find an operational semantics which respects the equations, but at the same time does not introduce (too many) observational equivalences that are not implied by the equations.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for your answer. I had in mind the "prescriptive" equations, not observational equivalence, which I am not too familiar with. From your last sentence, it sounds like you're implying that observational equivalence is stronger than equational theories, i.e. it is able to tell more programs apart. Is this always the case? Also, where do eta reductions fit into the picture? To me, it seems like eta reductions are just a form of equational reasoning, i.e. the equality between $m$ and $\lambda x. mx$. $\endgroup$
    – gardenhead
    Oct 8, 2016 at 14:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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