# When would one use equational dynamics?

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?

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.
• 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$. – gardenhead Oct 8 '16 at 14:07