<p>I want to give an <em>exact</em> specification of the meaning of my programming language. I know how to write an interpreter for it, but:</p>
<ul>
<li>I don't want to require people to read the interpreter code to learn my language's semantics.</li>
<li>I want a single definitive resource for the semantics of my language. Maybe other people want to make an interpreter. It would be better to have a definitive document than require them to test the behaviour of their interpreter against mine.</li>
<li>The specification could be written in a natural language like English, but natural languages are imprecise. And if we <em>can</em> make English precise enough, it usually becomes very hard to read.</li>
<li>I want to write in a way that is widely understood.</li>
<li>I want to prove properties about my language.</li>
</ul>
<p>I'm looking for something that, at a high-level, specifies the step-by-step execution of my language in a similar way to how an interpreter would be written. How do I do this?</p>

<language-design><semantics>
How can I specify a programming language step-by-step more formally than by providing a reference interpreter?
CC BY-SA 4.0
2023-12-11T08:56:24.643Z
*"And if we can make English precise enough, it usually becomes very hard to read."* - that's probably true also of programming languages. The more general a language becomes in the concepts it is capable of expressing, and the more precisely the language expresses them, then the harder to read it becomes. Because natural language is expected to be fully general (that is, capable of accomodating anything at all we want to talk about), and because it cannot be unusable, then a certain amount of its precision is encoded in the context of use and in the cultural common sense of the reader. (1/2)
Steve
CC BY-SA 4.0
2023-12-11T08:56:41.367Z
The implication of this is that a working natural language does not just consist of expressed words and grammatical structures - rather, it consists also of an ecosystem of people who have a reproducible knowledge of what the expressed part of the language means, whose knowledge of what the language means is reproduced separately from any single reading (i.e. there are no self-contained texts which fully describe their own meaning), and who make sense of what they read by combining what they read with what they already know. (2/2)
Steve
CC BY-SA 4.0
2023-12-11T17:01:34.700Z
IIRC, "denotational semantics" was created to serve this purpose.
Barmar
CC BY-SA 4.0
2023-12-11T17:08:38.123Z
@Barmar Since I am asking about the behavior of an interpreter, this is more a question about *operational* semantics. A denotational semantics often abstracts over those details (which is certainly good in some cases, but not what I'm looking for here). There are some forms of denotational semantics which *do* capture this level of operational detail (for instance game semantics), but an operational semantics fundamentally *must* capture these details while a denotational semantics might not (and often does not).
David Young
CC BY-SA 4.0
2023-12-11T18:28:44.097Z
I don't think I can easily ask people this, unfortunately, but: Why the close votes? I would like to improve my question if possible!
David Young
CC BY-SA 4.0
2023-12-11T21:27:03.327Z
The question is now on SE's "hot networks questions" (HNQ) list... You may want to clarify what is "meaning of a language"  (I have no idea what it means... good thing I'm not into computer languages) before a lot of people get confused. Also "widely known" compared to answer is not really as "widely" as you may imply... consider picking better conditions there too while [edit].
Alexei Levenkov
CC BY-SA 4.0
2023-12-11T21:42:26.957Z
@AlexeiLevenkov Hmm, interesting. My intention with "meaning of a language" is to make it more friendly than "semantics of a language." You should take the phrase pretty literally: for each language feature, what does that feature mean in the sense "what is it intended to cause the computer to do?" The only words I can think of so far are "meaning" or "semantics". Can you think of any other possibilities?
David Young
CC BY-SA 4.0
2023-12-11T21:48:46.030Z
@DavidYoung I think "this is more a question about operational semantics" in one of your comments is far more useful for title and unlikely to be misunderstood compared to "meaning" (which for me is more suitable for philosophical discussion similar to "meaning of life").
Alexei Levenkov
CC BY-SA 4.0
2023-12-11T21:59:35.303Z
@AlexeiLevenkov I partially agree. On the other hand, I was hoping to bring in people who might not typically click on a question about "whatever operational semantics is"... After all, I think these are the main people that wouldn't already know about it! I thought the word "formally" helped, somewhat. I'm hoping to popularize these ideas among people outside academia. They're extremely well known in the academic study of programming languages (which is really what I mean when I say "widely known"), but not so much outside that. It's an extremely flexible way to organize certain kinds of info
David Young
CC BY-SA 4.0
2023-12-11T22:42:00.447Z
"I'm hoping to popularize these ideas among people outside academia." - have you seen your answer :) ? (I hope someone is able to read past first heading... unlike me)
Alexei Levenkov
CC BY-SA 4.0
2023-12-11T22:47:15.597Z
@AlexeiLevenkov Aw, that's exactly what I was hoping to avoid! The actual concept itself is far, *far* simpler than actually writing code! Someday, I'm going to put some videos together where I actually show how this relates to a real interpreter. As pragmatic as possible. Probably with some live-coding. And maybe I'll also make a web-based, interactive thing that will let you step through a program to show you how these derivations are made and how the rules work. Hmm
David Young
CC BY-SA 4.0
2023-12-12T09:26:13.457Z
https://webassembly.github.io/spec/core/ is the specification of WASM in the style proposed here and could serve as a more complex example.
Christian Lindig
CC BY-SA 4.0
2023-12-12T17:58:39.220Z
I've made an edit which I think makes some of the phrasing clearer; feel free to revert it, or any parts of it, if you think there is no improvement. To be honest I think this question could only be asked like this by someone who already knows what operational semantics are, but the Q&A is probably useful for people who wouldn't have put the question exactly this way themselves.
kaya3
CC BY-SA 4.0
2023-12-12T18:49:34.467Z
I don't think this should be closed. This is a good question with a useful answer.
CPlus
CC BY-SA 4.0
2023-12-13T09:12:37.553Z
I greatly appreciate this question & answer. The close votes were a shame.
apropos
CC BY-SA 4.0
2023-12-16T21:24:17.603Z
@AlexeiLevenkov I have replaced the first code block with a short English description including examples. The intention of that part is to explain the syntax of a very small calculator-like language that does arithmetic. Hopefully this is better communicated now! I think the original description was the only thing that I did not really explain in the answer. So, the answer should now be entirely self-contained.
David Young
CC BY-SA 4.0
2023-12-28T21:41:39.527Z
I mention WASM above. This IFCP keynote talks about the difficulty and process to define a language formally and how to increase trust in that formalization.  https://youtu.be/Lb45xIcqGjg?si=Br60_2LRraef1TaM
Christian Lindig
CC BY-SA 4.0
2024-01-10T04:09:11.970Z
Have you read the ECMAScript specification, and if yes, what's your opinion on that style? We tried to get a balance between readability and precision. There was an attempt to write the whole spec in an executable metalanguage but that didn't really catch on.
Eric Lippert
CC BY-SA 4.0
2024-01-21T14:51:18.110Z
@EricLippert Skimming through it, it looks good to me! I expect it to be readable for someone with no background in semantics. I probably would have considered something less verbose, but that might make it less accessible. Also, if that "less verbose thing" was not something standard like inference rules (or a specified subset of English), that would raise the question of "what is the semantics of *that* language?" and so on. Another interesting possibility would be to have two presentations: an English one and a more succinct one, both generated automatically from the same underlying thing.
David Young
CC BY-SA 4.0
2024-01-25T23:16:18.293Z
@DavidYoung: Indeed, when we were designing the type inference algorithms for C# 3 we asked Andrew Kennedy -- who designed and implemented a lot of the generics in .NET -- for an opinion on an early draft. He sent back a solid page of Hoare logic and said yep, looks good to me. I couldn't easily read Hoare logic at the time and we certainly were not going to put the burden of learning how on the spec readers, but it was very concise and had standardized semantics.
Eric Lippert
<h1>Executable specifications</h1>
<p>Essentially an independent executable test suite for the language written in the language itself that exercises every part of it, showcases every feature and checks that language semantics are implemented correctly by running the code and testing the results. Not <em>exactly</em> formal but certainly &quot;more formal&quot; than just publishing a reference implementation.</p>
<p><a href="https://github.com/ruby/spec" rel="nofollow noreferrer">The Ruby Spec</a> is a concrete example of such a thing. It is written in Ruby itself and executes test cases that check whether the Ruby implementation contains the specified features and that they behave according to Ruby semantics. For example, Ruby arrays are specified <a href="https://github.com/ruby/spec/blob/master/language/array_spec.rb" rel="nofollow noreferrer">like this</a>:</p>
<pre class="lang-ruby prettyprint-override"><code>describe &quot;Array literals&quot; do

  it &quot;[] should return a new array populated with the given elements&quot; do
    array = [1, 'a', nil]
    array.should be_kind_of(Array)
    array[0].should == 1
    array[1].should == 'a'
    array[2].should == nil
  end

  # ...

  it &quot;[] treats splatted nil as no element&quot; do
    [*nil].should == []
    [1, *nil].should == [1]
    [1, 2, *nil].should == [1, 2]
    [1, *nil, 3].should == [1, 3]
    [*nil, *nil, *nil].should == []
  end

  # ...

end
</code></pre>
<p>They fulfill the criteria you listed:</p>
<blockquote>
<p>I don't want to require people to read the interpreter code to learn my language's semantics.</p>
</blockquote>
<p>With an executable specification, people can read <em>and run</em> code written in your high level language instead.</p>
<blockquote>
<p>I want a single definitive resource for the semantics of my language.</p>
</blockquote>
<p>The executable specification provides a single source of truth, in executable format.</p>
<blockquote>
<p>Maybe other people want to make an interpreter. It would be better to have a definitive document than require them to test the behaviour of their interpreter against mine.</p>
</blockquote>
<p>The executable specification is independent of your reference implementation. People can run it on <em>their</em> interpreters too. If it runs and passes all tests, they can confidently say they created an implementation of your language.</p>
<blockquote>
<p>I want to write in a way that is widely understood.</p>
</blockquote>
<p>Code is widely understood by programmers. It's also understood by computers.</p>
<blockquote>
<p>I want to prove properties about my language.</p>
</blockquote>
<p>Successfully running the executable specification proves that it behaves as specified. Probably not as rigorous as formal proofs in the mathematical sense but still extremely useful.</p>
<blockquote>
<p>I'm looking for something that, at a high-level, specifies the step-by-step execution of my language in a similar way to how an interpreter would be written.</p>
</blockquote>
<p>That &quot;something&quot; reminds me of &quot;code&quot;, which is what executable specifications are made out of. Code specifies at a high level the instructions that must be executed to carry out the program, and all interpreters I know are implemented using code.</p>

CC BY-SA 4.0
2023-12-14T05:35:48.187Z
2023-12-14T05:35:48.187Z
Matheus Moreira
<p>In many cases, specifying a language by specifying all of the ways an implementation would be allowed to process the constructs therein may be more useful and precise than trying to formalize rules about program constructs themselves.  An objection some people may have to the approach described in David Young's answer is that it doesn't accommodate optimizations, but that doesn't mean that it couldn't be tweaked to do so.</p>
<p>For example, a specification for how a language is processed may specify that operations may be performed in a sequence which differs from specified in the absence of certain constructs where execution is deemed to be important; programmers would not be required to avoid all possible situations where processing things out of sequence might be observable, but would be required to accommodate the variations in sequence that might occur.</p>
<p>If in the absence of optimization, division by zero would have behavior defined as trapping, an &quot;optimization-friendly&quot; dialect might specify that such traps are not considered a &quot;sequenced side effect&quot;.  That would not imply a requirement that divisions by zero be prevented at all costs, even in response to invalid input, but rather that a program that might attempt a division by zero prepared for the possibility that the attempted division might have been performed out of sequence, and this may result in an arbitrary subset of the operations between the previous and succeeding &quot;causality barrier&quot; directives being executed before the trap fired.  While that may leave parts of a program's state inconsistent with anything that could have resulted from sequential program execution, recognizing such a state as a natural consequence of an allowable reordering of operations would avoid the need to characterize it as &quot;anything can happen&quot; UB.</p>

CC BY-SA 4.0
2023-12-11T20:57:59.217Z
2023-12-11T20:57:59.217Z
supercat
CC BY-SA 4.0
2023-12-12T07:40:22.963Z
Hmm, I'm not sure I fully understand what you're suggesting. You can represent nondeterminism in an operational semantics. In fact, it is often slightly easier to do this than to make things deterministic, because you remove requirements. if you take my rule [E-Add-2] and remove the requirement that $n$ be a value, then we have made the evaluation order of $\verb|add|$ undefined. The semantics would allow for both left-to-right and right-to-left evaluation of the arguments of $\verb|add|$.
David Young
CC BY-SA 4.0
2023-12-12T15:49:51.743Z
@DavidYoung: Consider the cited example of divide-by-zero behavior.  Specifying that an implementation may reorder a division operation ahead of across other operations upon which its operands do not depend, or defer it across other operations that do not depend upon its result, and that if the division were to trap, any sequence of observable operations that could result from that would be a legitimate way for the implementation to behave, would seem cleaner and simpler than trying to specify what "conforming" programs are allowed to do.
supercat
CC BY-SA 4.0
2023-12-12T15:57:32.427Z
@DavidYoung: While a choice of which operand to "+" is evaluate first may be a simple "Unspecified" choice, I don't see any way of saying that e.g. `do { extern1++; x = y/z; ... } while(whatever);` might be processed in a way that could trap without incrementing `extern1`, that would be easier than saying that an implementation may reorder the division ahead of preceding actions upon which its operands have no dependencies, in a manner *agnostic* to whether the division might trap.
supercat
CC BY-SA 4.0
2023-12-12T16:10:44.753Z
@DavidYoung: With regard to "real" non-determinism, "benign" race-condition behaviors could be described using a non-deterministic model that would allow for e.g. `uint16_t x = *p; int y = x - (x >> 15);` to be processed in a manner that could yield 65535 if `*p` changes from 65535 to 0 or vice versa during its execution, but provide programmers with a way of writing the expression so as to guarantee that `*p` is read *at most* once (without making it `volatile` and forcing it to be read *exactly* once), but it may be easier to reason about by specifying when compilers may "invent" reads.
supercat
<p>A popular way to do this is to give an <em>operational semantics</em> for your language. What is an operational semantics? Very roughly speaking, it is like a high-level outline for an interpreter. It is written in the same general <a href="https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation">notation that formal typing rules are written in</a>.</p>
<p>In this answer, I will cover what's known as a <em>small-step</em> operational semantics. This fits your requirement that it describes the individual steps that an interpreter takes. There are other forms of operational semantics as well, such as big-step and reduction semantics (aka contextual semantics).</p>
<p>If you've ever written an interpreter, then you <em>already understand</em> most of the fundamentals behind operational semantics! I'm going to describe a convenient &quot;shorthand&quot; to describe interpreters. This shorthand gives us a nice way to talk about the semantics of a programming language.</p>
<h1>A small language</h1>
<p>Lets consider a very small calculator language which allows us to write simple arithmetic expressions like <code>add(1, add(2, 3))</code>, <code>equal(5, sub(7, 10))</code> and <code>if(equal(1, 2), 3, 7)</code>. More specifically, we will have these features:</p>
<ul>
<li>integers literals</li>
<li>addition</li>
<li>subtraction</li>
<li>comparison for equality</li>
<li><code>if</code> expressions (these are sort of like C's ternary operator, but without using a special syntax).</li>
</ul>
<h1>An interpreter step</h1>
<p>Think about how our interpreter will work, step-by-step. Consider the expression <code>add(add(1, 2), 10)</code>. Our interpreter will initially evaluate the first argument of <code>add</code>, giving us <code>add(3, 10)</code>. Then, we will evaluate <code>add(3, 10)</code> to get <code>13</code>.</p>
<p>Notice how each step conceptually involves an expression getting turned into some other expression. We can express this fact as a <em>relation</em>: Each step <em>relates</em> an expression to the expression it reduces to in one step. This is the small-step reduction relation for our language. The symbol used for this is usually <span class="math-container">$\longrightarrow$</span>.</p>
<p><strong>A crucial point</strong>: When we write <span class="math-container">$e \longrightarrow e'$</span> this is <em>exactly the same</em> as saying &quot;<span class="math-container">$e$</span> reduces to <span class="math-container">$e'$</span> in one evaluation step&quot;. It is just much less cumbersome to write it using the arrow.</p>
<p>We will define our semantics by giving an exact definition for the relation <span class="math-container">$\longrightarrow$</span>.</p>
<h1>A refresher</h1>
<p>We will give a specific definition of <span class="math-container">$\longrightarrow$</span> using <em>inference rules</em>, <a href="https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation">in the same way that type systems are defined</a>.</p>
<p>An inference rule has two parts:</p>
<ul>
<li>A list of <em>premises</em></li>
<li>A <em>conclusion</em></li>
</ul>
<p>The rule tells us that whenever we can show that all of the premises hold, then the conclusion also holds.</p>
<p>It is written like this, where <span class="math-container">$J_1, \cdots, J_n$</span> are our premises and <span class="math-container">$J$</span> is our conclusion:</p>
<p><span class="math-container">$$
\cfrac{J_1 ~~~ J_2 ~~~ \cdots ~~~ J_n}
{J}~[\text{Rule-Name}]
$$</span></p>
<p>&quot;[Rule-Name]&quot; is an optional name for the inference rule. It is usually written in small capital letters, though I can't do that here. The <span class="math-container">$J$</span>'s are <em>judgments</em>. In our case, a judgment has the form <span class="math-container">$\cdots \longrightarrow \cdots$</span>. There can be other judgments as well.</p>
<p>When we list out a collection of inference rules, it is common to put the &quot;syntax&quot; of the judgment forms involved at the top of the page inside of a box like this:</p>
<p><span class="math-container">$$
\fbox{$e \longrightarrow e$}
$$</span></p>
<p>We have a binary relation called &quot;<span class="math-container">$\longrightarrow$</span>&quot; that takes an expression on the left-hand side and an expression on the right-hand side.</p>
<h1>Our semantics</h1>
<p>Here we define three inference rules for <span class="math-container">$\verb|add|$</span>: One to reduce the left argument, one to reduce the right argument and finally one rule for when both arguments are already values (they have been fully reduced).</p>
<p>I'll use the notation <span class="math-container">$\underline{n}$</span> to indicate that <span class="math-container">$n$</span> is a value (that is, a number rather than a compound expression). There are other ways to do this as well. For instance, you can introduce a unary judgment <span class="math-container">$\text{val}$</span> where <span class="math-container">$v~ \text{val}$</span> means &quot;<span class="math-container">$v$</span> is a value.&quot;</p>
<p>The first rule can be written like this:</p>
<p><span class="math-container">$$
\cfrac{e_1 \longrightarrow e_1'}
{\verb|add|(e_1, e_2) \longrightarrow \verb|add|(e_1', e_2)}[\text{E-Add-1}]
$$</span></p>
<p>This says: Whenever expression <span class="math-container">$e_1$</span> steps to <span class="math-container">$e_1'$</span>, then we know <span class="math-container">$\verb|add|(e_1, e_2)$</span> steps to <span class="math-container">$\verb|add|(e_1', e_2)$</span>. This is what are interpreter used in the first step of our example.</p>
<p>We have a very similar rule for the right argument. There is, however an important difference from the last case. Can you spot it?</p>
<p><span class="math-container">$$
\cfrac{e_2 \longrightarrow e_2'}
{\verb|add|(\underline{n}, e_2) \longrightarrow \verb|add|(\underline{n}, e_2')}~[\text{E-Add-2}]
$$</span></p>
<p>The difference is that we require the first argument to be a value. Why might we do this?</p>
<p>By inserting this requirement, we ensure that the arguments must be evaluated left-to-right. If we did not have a requirement like this anywhere, we might have an undefined evaluation order. We could still work with a semantics like this, but it might be less desirable. Something to consider: Is it ever <em>desirable</em> to have an undefined (or <em>less</em> defined) evaluation order? Why or why not?</p>
<p>Now we have our final case:</p>
<p><span class="math-container">$$
\cfrac{\underline{n} = \underline{n_1} + \underline{n_2}}
{\verb|add|(\underline{n_1}, \underline{n_2}) \longrightarrow \underline{n}}
~[\text{E-Add}]
$$</span></p>
<p>If both of our arguments are values, then we can just replace the <span class="math-container">$\verb|add|$</span> with the actual sum of the two values. We would use this rule, for example, when we have the expression <span class="math-container">$\verb|add|(1,2)$</span>.</p>
<p>We can define how the relation works in a similar way for <span class="math-container">$\verb|sub|$</span>. (<em>Exercise</em>: Define the relation for <span class="math-container">$\verb|equal|$</span> and for <span class="math-container">$\verb|if|$</span>. Use <span class="math-container">$\verb|true|$</span> and <span class="math-container">$\verb|false|$</span> as the Boolean values.)</p>
<p>By reasoning about our <span class="math-container">$\longrightarrow$</span> relation, we are able to formally talk about <em>properties</em> of our semantics:</p>
<ul>
<li>Does evaluation ever get &quot;stuck&quot; (if so, this could correspond to something like a runtime type error, where execution must stop)? This is discussed in more detail in <a href="https://langdev.stackexchange.com/a/3377/172">this answer about type soundness</a>.</li>
<li>Does evaluation always terminate (meaning, among other things, that our language is not Turing complete)?</li>
<li>Is our evaluation order always exactly defined? Is there any nondeterminism or undefined behavior?</li>
</ul>
<p>Using the relation, we can mathematically prove what the answers are for each of those questions!</p>
<h1>Applying the relation to our example</h1>
<p>Let's take our <span class="math-container">$\verb|add|(\verb|add|(1, 2), 10)$</span> example and use our inference rules. For the first step, we can't use [E-Add-2] or [E-Add] (<em>exercise</em>: why?). But we can use [E-Add-1]!</p>
<p><span class="math-container">$$
\cfrac{\verb|add|(1, 2) \longrightarrow \cdots}
{\verb|add|(\verb|add|(1, 2), 10) \longrightarrow \verb|add|(\cdots, 10)}~[\text{E-Add-1}]
$$</span></p>
<p>How do we figure out what to put in the places where I've written &quot;<span class="math-container">$\cdots$</span>&quot;? We need to use [E-Add] since we are applying <span class="math-container">$\verb|add|$</span> to two values in the expression <span class="math-container">$\verb|add|(1, 2)$</span>.</p>
<p>I'll start by &quot;stacking&quot; the two rules. Then, I will fill in the &quot;<span class="math-container">$\cdots$</span>&quot;.</p>
<p><span class="math-container">$$
\cfrac{
\cfrac{\cdots ~=~ 1 + 2}
{\verb|add|(1, 2) ~\longrightarrow~ \cdots}~[\text{E-Add}]}
{\verb|add|(\verb|add|(1, 2), 10) \longrightarrow \verb|add|(\cdots, 10)}~[\text{E-Add-1}]
$$</span></p>
<p>This is called a &quot;derivation.&quot; We often read derivations from the bottom up: we want to find the result of stepping <span class="math-container">$\verb|add|(\verb|add|(1, 2), 10)$</span>. In order to do this, we need to step <span class="math-container">$\verb|add|(1, 2)$</span>. And in order to do <em>that</em>, we need to compute <span class="math-container">$1 + 2$</span>.</p>
<p>Note how closely this mimics the way that an interpreter works!</p>
<p>If I fill in <span class="math-container">$3$</span> for the &quot;<span class="math-container">$\cdots$</span>&quot;, we finally end up with:</p>
<p><span class="math-container">$$
\cfrac{
\cfrac{3 ~=~ 1 + 2}
{\verb|add|(1, 2) ~\longrightarrow~ 3}~[\text{E-Add}]}
{\verb|add|(\verb|add|(1, 2), 10) \longrightarrow \verb|add|(3, 10)}~[\text{E-Add-1}]
$$</span></p>
<p>This is the complete derivation that shows how <span class="math-container">$\verb|add|(\verb|add|(1, 2), 10)$</span> steps to <span class="math-container">$\verb|add|(3, 10)$</span>.</p>
<h1>Multi-step relation</h1>
<p>We have discussed a relation that represents one evaluation step. How about a relation that represents zero or more evaluation steps? This is often written <span class="math-container">$\longrightarrow^{*}$</span>. Whenever we have defined a single-step relation, we can always define a multi-step relation.</p>
<p>More formally, we have the following two rules which define <span class="math-container">$\longrightarrow^{*}$</span> in terms of <span class="math-container">$\longrightarrow$</span>:</p>
<p><span class="math-container">$$
\cfrac{}
{e \longrightarrow^{*} e}~[\text{E-Done}]
$$</span></p>
<p>and</p>
<p><span class="math-container">$$
\cfrac{e \longrightarrow e' ~~~ e' \longrightarrow^{*} e''}
{e \longrightarrow^{*} e''}~[\text{E-Step}]
$$</span></p>
<p>Note that [E-Step] has <em>two</em> premises. We can use the <span class="math-container">$\longrightarrow^{*}$</span> relation to talk about <em>fully</em> reducing expressions, among other things. This can be used to answer questions like: &quot;Do all terminating expressions reduce to <em>unique</em> values?&quot; This is usually a desirable property of an operational semantics.</p>
<p><em>Exercise</em>: Write a derivation for <span class="math-container">$\verb|add|(\verb|add|(1, 2), 10) \longrightarrow^{*} 13$</span>.</p>
<p><em>Exercise</em>: Implement an interpreter for this language. Pay special attention to the relationship between the operational semantics and the implementation.</p>
<p><em>Exercise</em>: Using the <span class="math-container">$\longrightarrow^{*}$</span> relation for our language, <em>state</em> the property &quot;every expression terminates.&quot; <em>Hint</em>: recall the <span class="math-container">$\underline{n}$</span> notation for values.</p>
<p><em>Exercise</em>: Using the <span class="math-container">$\longrightarrow^{*}$</span> relation for our language, <em>state</em> the property &quot;every terminating expression reduces to a <em>unique</em> value.&quot;</p>
<p><em>Exercise</em>: For our language here, prove the property &quot;every expression terminates.&quot;</p>
<h1>Bonus: Extending our language with <code>print</code></h1>
<p>If we extend our language with a <code>print</code> command, how can we extend our semantics to model the output behavior? Lets say this allows us to do things like <code>print(add(2, 2))</code>. We'll also allow <code>print</code> to be used inside expressions like <code>add(print(1), 3)</code>. In these cases, <code>print</code> will just return its argument after it prints to the screen. Further, we will include a &quot;sequencing operator&quot; called <code>;</code>. For example, <code>print(1) ; print(3)</code> will print both <code>1</code> and <code>3</code> and it will evaluate to <code>3</code>.</p>
<p>So, now we can have programs like this</p>
<pre><code>print(sub(add(2, 4), 1);
print(7);
10
</code></pre>
<p>Also, we can have <code>print</code>s embedded in expressions like this:</p>
<pre><code>add(print(3), 5)
</code></pre>
<p>We will also say that the semicolon operator will evaluate both sides and just return the second. So, <code>print(3); print(7)</code> will print <code>3</code> and <code>7</code> and it will evaluate to <code>7</code>.</p>
<p>We will say that a <code>print</code> like this will print to the screen when it gets evaluated and it will return the its argument. So this will print <code>3</code> to the screen and the whole expression will evaluate to <code>8</code>.</p>
<p>Our original small-step relation relates two expressions. But this can't really tell us anything about <em>effects</em> like output. What we really need to do is relate two <em>pairs</em>, where the first item is an expression and the second item is a list of numbers. The list of numbers will represent our output.</p>
<p>First, we need to briefly establish a notation for lists of numbers. We will use <span class="math-container">$[]$</span> for the empty list. <span class="math-container">$[1,2,3]$</span> will be a list of the numbers <span class="math-container">$1$</span>, <span class="math-container">$2$</span> and <span class="math-container">$3$</span>. To prepend a single element to the head of the list, we will use <span class="math-container">$::$</span>. So, <span class="math-container">$10 :: [1,2,3]$</span> is the same as the list <span class="math-container">$[10,1,2,3]$</span>.</p>
<p>I will use the (meta-)variable <span class="math-container">$\omega$</span> to represent the list of output: <strong>o</strong>mega for &quot;<strong>o</strong>utput&quot;.</p>
<p>Our small-step evaluation judgment will now have this form:</p>
<p><span class="math-container">$$
\fbox{$\langle e, \omega \rangle \longrightarrow \langle e, \omega \rangle$}
$$</span></p>
<p>That is, on both sides it takes a pair consisting of an expression and a list of numbers.</p>
<p><strong>A crucial point</strong>: Whenever we see <span class="math-container">$\langle e, \omega \rangle \longrightarrow \langle e', \omega' \rangle$</span>, this means &quot;given that we have the output <span class="math-container">$\omega$</span> so far, expression <span class="math-container">$e$</span> evaluates to <span class="math-container">$e'$</span> in one-step and changes the output to <span class="math-container">$\omega'$</span>.</p>
<p>Let's first look at a couple of specific examples.</p>
<ul>
<li><p><span class="math-container">$\verb|add|(2, \verb|add|(4,4))$</span> should not do anything to the output, so if we are evaluating that expression when we've already printed <span class="math-container">$20$</span> to the screen we have <span class="math-container">$\langle \verb|add|(2, \verb|add|(4,4)), [20] \rangle \longrightarrow \langle \verb|add|(2, 8), [20] \rangle$</span>. We left the output unchanged, since the evaluation step did not print anything.</p>
</li>
<li><p>If, instead, we look at evaluating <span class="math-container">$\verb|add|(5, \verb|print|(7))$</span> and we have already printed <span class="math-container">$10$</span>, then we have <span class="math-container">$\langle \verb|add|(5, \verb|print|(7)), [10] \rangle \longrightarrow \langle \verb|add|(5, 7), [7, 10] \rangle$</span>. Note that we extended our output list, since we printed something to the screen.</p>
</li>
</ul>
<p>Now, let's generalize this. Here is what [E-Add-1] becomes with this new <span class="math-container">$\longrightarrow$</span> relation:</p>
<p><span class="math-container">$$
\cfrac{\langle e_1, \omega \rangle \longrightarrow \langle e_1', \omega' \rangle}
  {\langle \verb|add|(e_1, e_2), \omega \rangle \longrightarrow \langle \verb|add|(e_1', e_2), \omega' \rangle}~[\text{E-Add-1}]
$$</span></p>
<p>This is very similar to our original rule. In fact, if you cover up the <span class="math-container">$\omega$</span>s and the pair brackets, it is identical to our original rule! In our new rule, we just pass the output from evaluating our left argument. This makes sense because <span class="math-container">$\verb|add|$</span> does not, by itself, do anything to change the output.</p>
<p>Now it's pretty critical to figure out how to evaluate print itself! For this, we will have two rules. One to evaluate its argument (much like how <span class="math-container">$\verb|add|$</span> works) and one to actually perform the printing.</p>
<p><span class="math-container">$$
\cfrac{\langle e, \omega \rangle \longrightarrow \langle e', \omega' \rangle}
  {\langle \verb|print|(e), \omega \rangle \longrightarrow \langle \verb|print|(e'), \omega' \rangle}~[\text{E-Print-1}]
$$</span></p>
<p>Note we do not actually do anything here, other than evaluate the argument and pass the resulting output (if any) through.</p>
<p>The rule for actually printing:</p>
<p><span class="math-container">$$
\cfrac{}
  {\langle \verb|print|(\underline{n}), \omega \rangle \longrightarrow \langle \underline{n}, \underline{n} :: \omega \rangle}~[\text{E-Print}]
$$</span></p>
<p>If our argument is a value <span class="math-container">$\underline{n}$</span>, we can print <span class="math-container">$n$</span> to the screen (which we represent by extending the list <span class="math-container">$\omega$</span> to be <span class="math-container">$\underline{n} :: \omega$</span>) and we evaluate to <span class="math-container">$\underline{n}$</span>.</p>
<p>Another important piece is the semicolon operator (sequencing operator). We have three rules for this:</p>
<p><span class="math-container">$$
\cfrac{\langle e_1, \omega \rangle \longrightarrow \langle e_1', \omega' \rangle}
  {\langle (e_1 ; e_2), \omega \rangle \longrightarrow \langle (e_1' ; e_2), \omega' \rangle }~[\text{E-Seq-1}]
$$</span></p>
<p><span class="math-container">$$
\cfrac{\langle e_2, \omega \rangle \longrightarrow \langle e_2', \omega' \rangle}
  {\langle (\underline{n} ; e_2), \omega \rangle \longrightarrow \langle (\underline{n} ; e_2'), \omega' \rangle}~[\text{E-Seq-2}]
$$</span></p>
<p><span class="math-container">$$
\cfrac{}
  {\langle (\underline{n_1} ; \underline{n_2}), \omega \rangle \longrightarrow \langle \underline{n_2}, \omega \rangle }~[\text{E-Seq}]
$$</span></p>
<p>Lets try this out by making a derivation for <span class="math-container">$\verb|add|(\verb|print|(5), \verb|print|(10))$</span> using our small-step relation. Remember, this will be one evaluation step. We will say we haven't printed anything so far at the start of evaluation. I will incrementally write the derivation out step-by-step and use <span class="math-container">$e$</span> and <span class="math-container">$\omega$</span> as placeholders for what we haven't figured out yet (the things we need to figure out by continuing to write the derivation.</p>
<p>First, we evaluate the left argument of <span class="math-container">$\verb|add|$</span>.</p>
<p><span class="math-container">$$
\cfrac{\langle \verb|print|(5), [] \rangle \longrightarrow \langle e, \omega \rangle }
  {\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(e, \verb|print|(10)), \omega \rangle }~[\text{E-Add-1}]
$$</span></p>
<p>Now we need to figure out how to evaluate <span class="math-container">$\verb|print|(5)$</span> where we have no output so far:</p>
<p><span class="math-container">$$
\cfrac{
   \cfrac
 {}
 {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
  {\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
$$</span></p>
<p>Remember, <span class="math-container">$5 :: []$</span> is the same as <span class="math-container">$[5]$</span>.</p>
<p>Thanks to @theonlygusti for the comment about this.</p>
<p><em>Exercise</em>: What do we get when we fully reduce <span class="math-container">$\verb|print|(\verb|add|(\verb|print|(5), \verb|print|(10)))$</span>?</p>
<h2>A multi-step derivation example with <code>print</code></h2>
<p>Let's take another look at our example <span class="math-container">$\verb|add|(\verb|print|(5), \verb|print|(10))$</span>. We will use the multi-step relation <span class="math-container">$\longrightarrow^{*}$</span> to <em>fully</em> reduce it this time. We'll also see why we need an output state on both sides of the arrow.</p>
<p>First, we need to update our multi-step relation rules to use output.</p>
<p><span class="math-container">$$
\cfrac{}
{\langle e, \omega \rangle \longrightarrow^{*} \langle e, \omega \rangle}~[\text{E-Done}]
$$</span></p>
<p><span class="math-container">$$
\cfrac{\langle e, \omega \rangle \longrightarrow \langle e', \omega' \rangle ~~~ \langle e', \omega' \rangle \longrightarrow^{*} \langle e'', \omega'' \rangle}
{\langle e, \omega \rangle \longrightarrow^{*} \langle e'', \omega'' \rangle}~[\text{E-Step}]
$$</span></p>
<p>Note how the state is fed through the two premises of [E-Step].</p>
<p>Now, to the example. We will start with the single step derivation we had before:</p>
<p><span class="math-container">$$
\cfrac{
   \cfrac
 {}
 {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
  {\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
$$</span></p>
<p>This will be one of the premises of the multi-step derivation:</p>
<p><span class="math-container">$$
\cfrac{
  \begin{array}{c c}
  \cfrac{
 \cfrac
   {}
   {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
%
&amp;\cfrac{\cdots}{\langle \verb|add|(5, \verb|print|(10)), [5] \rangle \longrightarrow^{*} \langle e, \omega \rangle} \end{array}}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow^{*} \langle e, \omega \rangle}~[\text{E-Step}]
$$</span></p>
<p>I have filled in the one step which we already computed before. This is used as the first premise for the multi-step inference rule [E-Step]. Now, we need to do the rest by figuring out the second premise. Then, we will be able to update the conclusion by replacing <span class="math-container">$e$</span> with the evaluation result and <span class="math-container">$\omega$</span> with the final output.</p>
<p>So, doing steps until we reach a value we get this somewhat complicated looking derivation:</p>
<p><span class="math-container">$$
\cfrac{
  \begin{array}{c c}
  \cfrac{
 \cfrac
   {}
   {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
%
&amp;\cfrac{
 \begin{array}{c c}
   \cfrac{
   \cfrac{}
     {\langle \verb|print|(10), [5] \rangle \longrightarrow \langle 10, [10, 5] \rangle}~[\text{E-Print}]
   }
 {\langle \verb|add|(5, \verb|print|(10)), [5] \rangle \longrightarrow \langle \verb|add|(5, 10), [10,5] \rangle}~[\text{E-Add-2}]&amp;
   \cfrac{
   \begin{array}{c c}
     \cfrac{15 = 5 + 10}
       {\langle \verb|add|(5, 10), [10,5] \rangle \longrightarrow \langle 15, [10,5] \rangle}~[\text{E-Add}]&amp;
     \cfrac{}
       {\langle 15, [10,5] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Done}]
   \end{array}
  }
{\langle \verb|add|(5, 10), [10,5] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Step}]
 \end{array}
}
  {\langle \verb|add|(5, \verb|print|(10)), [5] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Step}]
%
\end{array}}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Step}]
$$</span></p>
<p>Now, this is difficult to read. It spells out all of the dependencies, but this verbosity is what makes it challenging.</p>
<p>But note how the output state gets threaded through the steps. If the step that executed <span class="math-container">$\verb|print|(10)$</span> did not know that we already printed a <span class="math-container">$5$</span>, then it could not know how to give the correct new output of <span class="math-container">$[10,5]$</span> (I have the lists going &quot;backwards&quot; from how the actual output would work, but this is not necessary).</p>
<p>You might wonder if we can leave out the outputs on the left-hand side of the single-step relation and then combine the right-hand outputs together in the multi-step relation. But remember that we are looking at the very special case of printing to a screen. In this case, we can concatenate outputs. But, in general, effects don't necessarily work this way.</p>
<h1>Comparison to reference interpreters</h1>
<p>@JerryCoffin brings up a very good point in the comments: Why not use a &quot;reference interpreter?&quot; How does this approach compare? A reference interpreter is where you define a semantics by giving an actual interpreter written in an existing language like Haskell.</p>
<p>A very big difference is the complexity. Any programming language that can be used to practically write an interpreter is going to be far, <em>far</em> more complex than the &quot;language&quot; of inference rules!</p>
<p>For example, Haskell has nontermination, exceptions, a specific evaluation order, etc. It has things like higher-order functions and a standard library. Other languages might have classes and objects. Inference rules have none of those things. Inference rules don't even have functions! The <em>only</em> thing an inference rule can do is say &quot;if you know these things, then you can derive this thing&quot;. That is the only &quot;abstraction&quot; given to you by the language of inference rules. Note how I had to specifically spell out the evaluation order for <span class="math-container">$\verb|add|$</span>. But we can use this framework to specify languages.</p>
<p>There are only two things in the &quot;language of inference rules&quot;: judgments (like <span class="math-container">$\longrightarrow$</span>) and inference rules. We can also make use of basic mathematical constructs like our use of <span class="math-container">$=$</span> and <span class="math-container">$+$</span> in the rule [E-Add]. But note that even this is used very rarely!</p>
<p>One advantage of this simplicity is that it makes it much easier to write proofs, compared to using a reference interpreter. If we tried to write a proof about evaluation of our language and we used a reference interpreter written in Haskell, we would need some kind of semantics for Haskell in addition to a semantics for our language (at least informally). Here, we don't need that.</p>
<p>Additionally, it inherently provides a way visualize how a result is computed in the form of derivations. All of the dependencies the evaluation of subexpressions are shown in these derivations.</p>
<p>Reference interpreters have their place, but the approach outlined here also has advantages. The approach here is very frequently used in academic settings over many decades. Most programming language papers that give an &quot;execution&quot; semantics will give it in this style.</p>
<h1>Further topics</h1>
<ul>
<li><p>Another very important topic is the way that an operational semantics relates to a type system. It is often desirable to prove that the language has a property called &quot;syntactic type soundness.&quot; This is outside the scope of this answer.</p>
</li>
<li><p>When we give a <em>denotational</em> semantics for a language, we usually want the two semantics to be very closely linked with each other. The basic theorem linking them that you always want to hold is called &quot;adequacy.&quot; There is also a stronger theorem that holds for some semantics called &quot;full abstraction.&quot; There is some more detail at the end of <a href="https://langdev.stackexchange.com/questions/2015/how-can-we-compare-expressive-power-between-two-turing-complete-languages/2016#2016">this answer</a>. Another answer should cover this in more detail. There is also background on denotational semantics more generally <a href="https://langdev.stackexchange.com/questions/2019/what-are-denotational-semantics-and-what-are-they-useful-for/">here</a> and <a href="https://langdev.stackexchange.com/questions/1953/how-can-we-define-a-denotational-semantics-for-recursive-functions/">here</a>.</p>
</li>
</ul>
<h1>References</h1>
<h2>Talks</h2>
<ul>
<li><a href="https://www.youtube.com/watch?v=exhwykjH_z4" rel="noreferrer">Basic Mechanics of Operational Semantics</a> by David Van Horn</li>
</ul>
<h2>Books</h2>
<ul>
<li><em>Types and Programming Languages</em> by Benjamin Pierce</li>
<li><em>Practical Foundations for Programming Languages</em> by Robert Harper</li>
<li><em>Formal Semantics of Programming Languages</em> by Glynn Winksel</li>
</ul>
<h2>Papers</h2>
<ul>
<li><a href="https://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf" rel="noreferrer"><em>A Structural Approach to Operational
Semantics</em></a> by Gordon Plotkin (Plotkin is the origin of this kind of operational semantics)</li>
</ul>

CC BY-SA 4.0
2023-12-11T04:29:24.293Z
2023-12-16T21:28:33.170Z
2023-12-16T21:28:33.170Z
David Young
CC BY-SA 4.0
2023-12-11T16:37:49.893Z
@theonlygusti That's a good question! For `print`, you would typically do that like this: Instead of relating two expressions, we have $\longrightarrow$ relate two pairs. The pairs consist of an expression and a list of the outputs. If we extend our language with `print`, everything except `print` will ignore the "output" part of the pairs. `print` will extend the list. I'll add a section to my answer about this.
David Young
CC BY-SA 4.0
2023-12-11T18:59:43.347Z
@JerryCoffin It has been extremely widely used in academic contexts for the last 40+ years. If you look at almost any paper describing "execution" semantics of a PL written in that time, it will be written in this style. You cannot describe an "execution trace" as easily (or as visually) if you only have it written in Haskell. And as much as I love Haskell, it is also far more complicated. If you want to prove something about a Haskell program, then you need to worry about the evaluation order of Haskell, etc (basically, you will *also* need some kind of semantics of Haskell).
David Young
CC BY-SA 4.0
2023-12-11T19:01:47.583Z
Compared to the semantics of Haskell, there is actually very little involved in this representation! There are just inference rules, which say "if you know these things, then you are allowed to derive this thing." In this language of inference rules, there are no "exceptions," no specific evaluation order, no "nontermination", etc. Not even any functions! It is more fundamental and "simple" than that (not to say that it is necessarily, at first, easy to learn).
David Young
CC BY-SA 4.0
2023-12-11T19:03:00.760Z
What you're describing is a *reference interpreter*. That has its place too, but what I'm describing here also has a place. Also, your comment is not too negative at all! I appreciate the feedback!
David Young
CC BY-SA 4.0
2023-12-11T19:32:32.823Z
@JerryCoffin I added a section addressing your comment, since I think this is a very useful topic to discuss. I hope that helps. Also somewhat relatedly, at some point, I might work on a web-based thing that will take code written in a small language and interactively show you how derivations for the multi-step evaluation relation are constructed. This will show the relationship between an interpreter and an operational semantics.
David Young
CC BY-SA 4.0
2023-12-12T00:20:52.690Z
"*the same general notation that formal typing rules are written in*" - aka [The most popular programming language in computer science](https://www.youtube.com/watch?v=dCuZkaaou0Q)
Bergi
CC BY-SA 4.0
2023-12-12T16:01:59.073Z
@theonlygusti Remember that the $\longrightarrow$ is a *single* step. We need to perform several single steps to fully reduce something, in general. In order to know what to produce as output, we need to know what we've outputted so far. You might wonder now why not just concatenate the single-step outputs in our multi-step relation? Well, remember that we are looking at the very special case of printing something. Other effects might not be things you can just concatenate. I added a subsection to my answer addressing this in more detail.
David Young
CC BY-SA 4.0
2023-12-12T20:09:22.993Z
Wouldn't a simpler way of defining sequencing be (e1,w) -> (e1',w') => ((e1;e2),w) -> (e2,w')?
Moonchild
CC BY-SA 4.0
2023-12-13T12:58:58.513Z
OP wrote: *"I want to write in a way that is widely understood."* Unfortunately, I don't think the shown inference rule notation is widely understood by the general population of programmers.
G. Sliepen
CC BY-SA 4.0
2023-12-14T15:31:37.490Z
@G.Sliepen: It is, however, widely understood by computer scientists, and while programmers _may not_ at first understand it, it is simple enough that they should be able to in relatively short order.
Matthieu M.
CC BY-SA 4.0
2023-12-15T18:19:50.633Z
@Moonchild That does not quite work. Remember that $\longrightarrow$ does exactly one step. So, the premise of your rule would evaluate the first expression exactly one step and then throw away the rest. I have written up a counterexample in Agda [here](https://github.com/roboguy13/agda-stuff/blob/5aec8c753959f54d79c73a5e051db4b42e420143/calc/CalcSmallStep.agda#L255-L273), showing that the two semantics are different. It shows that $\verb|add|(\verb|print|(1), \verb|print|(2)) ; \verb|print|(3)$ cannot produce the same output in the new semantics as the old semantics.
David Young
CC BY-SA 4.0
2023-12-15T18:21:23.017Z
@Moonchild What you're describing is much closer to how a big-step semantics would work. [Here](https://github.com/roboguy13/agda-stuff/blob/5aec8c753959f54d79c73a5e051db4b42e420143/calc/CalcBigStep.agda#L32-L36) is the relevant rule of a big-step semantics for the language. Also, I've shown in that file that the big-step semantics I give there is equivalent to the small-step semantics I've shown earlier.
David Young
CC BY-SA 4.0
2023-12-16T19:39:30.960Z
Small-step semantics is typically about making it easy to prove theorems. Since OP is trying to convey understanding, a big step, natural deduction semantics might be a better choice.
Norman Ramsey
CC BY-SA 4.0
2023-12-16T20:02:43.760Z
@NormanRamsey While I do agree with that, the OP was intending to set this up to specifically ask for small-step semantics. The reason for using the phrase "step-by-step" is to be more suggestive of small-step semantics. As you point out, while big-step definitely has its own advantages, small-step can be very useful for proving things and so it conveys another sort of understanding of a language. I am certain that this is the intention since I am the OP =) I wanted to collect some fundamental theory concepts into some Q&A's here, to stimulate discussion a bit (and because it's useful & fun).
David Young
CC BY-SA 4.0
2023-12-16T20:02:46.227Z
I wanted to talk about small-step here in particular because I wanted to talk about type soundness later (which I recently wrote an answer about). Also along the lines of your comment: A contextual/reduction semantics would often be better in this situation than a traditional small-step semantics. However, you must understand how a typical small-step semantics works before you can learn about contextual semantics. If I can find a good way to frame the question, I might write one about this at some point.
David Young
# How can I specify a programming language step-by-step more formally than by providing a reference interpreter?
Posted by: username_0 on 2023-12-11
I want to give an *exact* specification of the meaning of my programming language. I know how to write an interpreter for it, but:

* I don't want to require people to read the interpreter code to learn my language's semantics.
* I want a single definitive resource for the semantics of my language. Maybe other people want to make an interpreter. It would be better to have a definitive document than require them to test the behaviour of their interpreter against mine.
* The specification could be written in a natural language like English, but natural languages are imprecise. And if we *can* make English precise enough, it usually becomes very hard to read.
* I want to write in a way that is widely understood.
* I want to prove properties about my language.

I'm looking for something that, at a high-level, specifies the step-by-step execution of my language in a similar way to how an interpreter would be written. How do I do this?
**Tags:** language-design semantics
> **Comments:**
> **username_1**: *"And if we can make English precise enough, it usually becomes very hard to read."* - that's probably true also of programming languages. The more general a language becomes in the concepts it is capable of expressing, and the more precisely the language expresses them, then the harder to read it becomes. Because natural language is expected to be fully general (that is, capable of accomodating anything at all we want to talk about), and because it cannot be unusable, then a certain amount of its precision is encoded in the context of use and in the cultural common sense of the reader. (1/2)  
> **username_1**: The implication of this is that a working natural language does not just consist of expressed words and grammatical structures - rather, it consists also of an ecosystem of people who have a reproducible knowledge of what the expressed part of the language means, whose knowledge of what the language means is reproduced separately from any single reading (i.e. there are no self-contained texts which fully describe their own meaning), and who make sense of what they read by combining what they read with what they already know. (2/2)  
> **username_2**: IIRC, "denotational semantics" was created to serve this purpose.  
> **username_0**: @Barmar Since I am asking about the behavior of an interpreter, this is more a question about *operational* semantics. A denotational semantics often abstracts over those details (which is certainly good in some cases, but not what I'm looking for here). There are some forms of denotational semantics which *do* capture this level of operational detail (for instance game semantics), but an operational semantics fundamentally *must* capture these details while a denotational semantics might not (and often does not).  
> **username_0**: I don't think I can easily ask people this, unfortunately, but: Why the close votes? I would like to improve my question if possible!  
> **username_3**: The question is now on SE's "hot networks questions" (HNQ) list... You may want to clarify what is "meaning of a language"  (I have no idea what it means... good thing I'm not into computer languages) before a lot of people get confused. Also "widely known" compared to answer is not really as "widely" as you may imply... consider picking better conditions there too while [edit].  
> **username_0**: @AlexeiLevenkov Hmm, interesting. My intention with "meaning of a language" is to make it more friendly than "semantics of a language." You should take the phrase pretty literally: for each language feature, what does that feature mean in the sense "what is it intended to cause the computer to do?" The only words I can think of so far are "meaning" or "semantics". Can you think of any other possibilities?  
> **username_3**: @DavidYoung I think "this is more a question about operational semantics" in one of your comments is far more useful for title and unlikely to be misunderstood compared to "meaning" (which for me is more suitable for philosophical discussion similar to "meaning of life").  
> **username_0**: @AlexeiLevenkov I partially agree. On the other hand, I was hoping to bring in people who might not typically click on a question about "whatever operational semantics is"... After all, I think these are the main people that wouldn't already know about it! I thought the word "formally" helped, somewhat. I'm hoping to popularize these ideas among people outside academia. They're extremely well known in the academic study of programming languages (which is really what I mean when I say "widely known"), but not so much outside that. It's an extremely flexible way to organize certain kinds of info  
> **username_3**: "I'm hoping to popularize these ideas among people outside academia." - have you seen your answer :) ? (I hope someone is able to read past first heading... unlike me)  
> **username_0**: @AlexeiLevenkov Aw, that's exactly what I was hoping to avoid! The actual concept itself is far, *far* simpler than actually writing code! Someday, I'm going to put some videos together where I actually show how this relates to a real interpreter. As pragmatic as possible. Probably with some live-coding. And maybe I'll also make a web-based, interactive thing that will let you step through a program to show you how these derivations are made and how the rules work. Hmm  
> **username_4**: https://webassembly.github.io/spec/core/ is the specification of WASM in the style proposed here and could serve as a more complex example.  
> **username_5**: I've made an edit which I think makes some of the phrasing clearer; feel free to revert it, or any parts of it, if you think there is no improvement. To be honest I think this question could only be asked like this by someone who already knows what operational semantics are, but the Q&A is probably useful for people who wouldn't have put the question exactly this way themselves.  
> **username_6**: I don't think this should be closed. This is a good question with a useful answer.  
> **username_7**: I greatly appreciate this question & answer. The close votes were a shame.  
> **username_0**: @AlexeiLevenkov I have replaced the first code block with a short English description including examples. The intention of that part is to explain the syntax of a very small calculator-like language that does arithmetic. Hopefully this is better communicated now! I think the original description was the only thing that I did not really explain in the answer. So, the answer should now be entirely self-contained.  
> **username_4**: I mention WASM above. This IFCP keynote talks about the difficulty and process to define a language formally and how to increase trust in that formalization.  https://youtu.be/Lb45xIcqGjg?si=Br60_2LRraef1TaM  
> **username_8**: Have you read the ECMAScript specification, and if yes, what's your opinion on that style? We tried to get a balance between readability and precision. There was an attempt to write the whole spec in an executable metalanguage but that didn't really catch on.  
> **username_0**: @EricLippert Skimming through it, it looks good to me! I expect it to be readable for someone with no background in semantics. I probably would have considered something less verbose, but that might make it less accessible. Also, if that "less verbose thing" was not something standard like inference rules (or a specified subset of English), that would raise the question of "what is the semantics of *that* language?" and so on. Another interesting possibility would be to have two presentations: an English one and a more succinct one, both generated automatically from the same underlying thing.  
> **username_8**: @DavidYoung: Indeed, when we were designing the type inference algorithms for C# 3 we asked Andrew Kennedy -- who designed and implemented a lot of the generics in .NET -- for an opinion on an early draft. He sent back a solid page of Hoare logic and said yep, looks good to me. I couldn't easily read Hoare logic at the time and we certainly were not going to put the burden of learning how on the spec readers, but it was very concise and had standardized semantics.  
---
## 3 answers
### Answer by username_0 on 2023-12-11. Score: 25 | Accepted answer
A popular way to do this is to give an operational semantics for your language. What is an operational semantics? Very roughly speaking, it is like a high-level outline for an interpreter. It is written in the same general notation that formal typing rules are written in.
In this answer, I will cover what's known as a small-step operational semantics. This fits your requirement that it describes the individual steps that an interpreter takes. There are other forms of operational semantics as well, such as big-step and reduction semantics (aka contextual semantics).
If you've ever written an interpreter, then you already understand most of the fundamentals behind operational semantics! I'm going to describe a convenient "shorthand" to describe interpreters. This shorthand gives us a nice way to talk about the semantics of a programming language.
A small language
Lets consider a very small calculator language which allows us to write simple arithmetic expressions like add(1, add(2, 3)), equal(5, sub(7, 10)) and if(equal(1, 2), 3, 7). More specifically, we will have these features:

integers literals
addition
subtraction
comparison for equality
if expressions (these are sort of like C's ternary operator, but without using a special syntax).

An interpreter step
Think about how our interpreter will work, step-by-step. Consider the expression add(add(1, 2), 10). Our interpreter will initially evaluate the first argument of add, giving us add(3, 10). Then, we will evaluate add(3, 10) to get 13.
Notice how each step conceptually involves an expression getting turned into some other expression. We can express this fact as a relation: Each step relates an expression to the expression it reduces to in one step. This is the small-step reduction relation for our language. The symbol used for this is usually $\longrightarrow$.
A crucial point: When we write $e \longrightarrow e'$ this is exactly the same as saying "$e$ reduces to $e'$ in one evaluation step". It is just much less cumbersome to write it using the arrow.
We will define our semantics by giving an exact definition for the relation $\longrightarrow$.
A refresher
We will give a specific definition of $\longrightarrow$ using inference rules, in the same way that type systems are defined.
An inference rule has two parts:

A list of premises
A conclusion

The rule tells us that whenever we can show that all of the premises hold, then the conclusion also holds.
It is written like this, where $J_1, \cdots, J_n$ are our premises and $J$ is our conclusion:
$$
\cfrac{J_1 ~~~ J_2 ~~~ \cdots ~~~ J_n}
{J}~[\text{Rule-Name}]
$$
"[Rule-Name]" is an optional name for the inference rule. It is usually written in small capital letters, though I can't do that here. The $J$'s are judgments. In our case, a judgment has the form $\cdots \longrightarrow \cdots$. There can be other judgments as well.
When we list out a collection of inference rules, it is common to put the "syntax" of the judgment forms involved at the top of the page inside of a box like this:
$$
\fbox{$e \longrightarrow e$}
$$
We have a binary relation called "$\longrightarrow$" that takes an expression on the left-hand side and an expression on the right-hand side.
Our semantics
Here we define three inference rules for $\verb|add|$: One to reduce the left argument, one to reduce the right argument and finally one rule for when both arguments are already values (they have been fully reduced).
I'll use the notation $\underline{n}$ to indicate that $n$ is a value (that is, a number rather than a compound expression). There are other ways to do this as well. For instance, you can introduce a unary judgment $\text{val}$ where $v~ \text{val}$ means "$v$ is a value."
The first rule can be written like this:
$$
\cfrac{e_1 \longrightarrow e_1'}
{\verb|add|(e_1, e_2) \longrightarrow \verb|add|(e_1', e_2)}[\text{E-Add-1}]
$$
This says: Whenever expression $e_1$ steps to $e_1'$, then we know $\verb|add|(e_1, e_2)$ steps to $\verb|add|(e_1', e_2)$. This is what are interpreter used in the first step of our example.
We have a very similar rule for the right argument. There is, however an important difference from the last case. Can you spot it?
$$
\cfrac{e_2 \longrightarrow e_2'}
{\verb|add|(\underline{n}, e_2) \longrightarrow \verb|add|(\underline{n}, e_2')}~[\text{E-Add-2}]
$$
The difference is that we require the first argument to be a value. Why might we do this?
By inserting this requirement, we ensure that the arguments must be evaluated left-to-right. If we did not have a requirement like this anywhere, we might have an undefined evaluation order. We could still work with a semantics like this, but it might be less desirable. Something to consider: Is it ever desirable to have an undefined (or less defined) evaluation order? Why or why not?
Now we have our final case:
$$
\cfrac{\underline{n} = \underline{n_1} + \underline{n_2}}
{\verb|add|(\underline{n_1}, \underline{n_2}) \longrightarrow \underline{n}}
~[\text{E-Add}]
$$
If both of our arguments are values, then we can just replace the $\verb|add|$ with the actual sum of the two values. We would use this rule, for example, when we have the expression $\verb|add|(1,2)$.
We can define how the relation works in a similar way for $\verb|sub|$. (Exercise: Define the relation for $\verb|equal|$ and for $\verb|if|$. Use $\verb|true|$ and $\verb|false|$ as the Boolean values.)
By reasoning about our $\longrightarrow$ relation, we are able to formally talk about properties of our semantics:

Does evaluation ever get "stuck" (if so, this could correspond to something like a runtime type error, where execution must stop)? This is discussed in more detail in this answer about type soundness.
Does evaluation always terminate (meaning, among other things, that our language is not Turing complete)?
Is our evaluation order always exactly defined? Is there any nondeterminism or undefined behavior?

Using the relation, we can mathematically prove what the answers are for each of those questions!
Applying the relation to our example
Let's take our $\verb|add|(\verb|add|(1, 2), 10)$ example and use our inference rules. For the first step, we can't use [E-Add-2] or [E-Add] (exercise: why?). But we can use [E-Add-1]!
$$
\cfrac{\verb|add|(1, 2) \longrightarrow \cdots}
{\verb|add|(\verb|add|(1, 2), 10) \longrightarrow \verb|add|(\cdots, 10)}~[\text{E-Add-1}]
$$
How do we figure out what to put in the places where I've written "$\cdots$"? We need to use [E-Add] since we are applying $\verb|add|$ to two values in the expression $\verb|add|(1, 2)$.
I'll start by "stacking" the two rules. Then, I will fill in the "$\cdots$".
$$
\cfrac{
\cfrac{\cdots ~=~ 1 + 2}
{\verb|add|(1, 2) ~\longrightarrow~ \cdots}~[\text{E-Add}]}
{\verb|add|(\verb|add|(1, 2), 10) \longrightarrow \verb|add|(\cdots, 10)}~[\text{E-Add-1}]
$$
This is called a "derivation." We often read derivations from the bottom up: we want to find the result of stepping $\verb|add|(\verb|add|(1, 2), 10)$. In order to do this, we need to step $\verb|add|(1, 2)$. And in order to do that, we need to compute $1 + 2$.
Note how closely this mimics the way that an interpreter works!
If I fill in $3$ for the "$\cdots$", we finally end up with:
$$
\cfrac{
\cfrac{3 ~=~ 1 + 2}
{\verb|add|(1, 2) ~\longrightarrow~ 3}~[\text{E-Add}]}
{\verb|add|(\verb|add|(1, 2), 10) \longrightarrow \verb|add|(3, 10)}~[\text{E-Add-1}]
$$
This is the complete derivation that shows how $\verb|add|(\verb|add|(1, 2), 10)$ steps to $\verb|add|(3, 10)$.
Multi-step relation
We have discussed a relation that represents one evaluation step. How about a relation that represents zero or more evaluation steps? This is often written $\longrightarrow^{*}$. Whenever we have defined a single-step relation, we can always define a multi-step relation.
More formally, we have the following two rules which define $\longrightarrow^{*}$ in terms of $\longrightarrow$:
$$
\cfrac{}
{e \longrightarrow^{*} e}~[\text{E-Done}]
$$
and
$$
\cfrac{e \longrightarrow e' ~~~ e' \longrightarrow^{*} e''}
{e \longrightarrow^{*} e''}~[\text{E-Step}]
$$
Note that [E-Step] has two premises. We can use the $\longrightarrow^{*}$ relation to talk about fully reducing expressions, among other things. This can be used to answer questions like: "Do all terminating expressions reduce to unique values?" This is usually a desirable property of an operational semantics.
Exercise: Write a derivation for $\verb|add|(\verb|add|(1, 2), 10) \longrightarrow^{*} 13$.
Exercise: Implement an interpreter for this language. Pay special attention to the relationship between the operational semantics and the implementation.
Exercise: Using the $\longrightarrow^{*}$ relation for our language, state the property "every expression terminates." Hint: recall the $\underline{n}$ notation for values.
Exercise: Using the $\longrightarrow^{*}$ relation for our language, state the property "every terminating expression reduces to a unique value."
Exercise: For our language here, prove the property "every expression terminates."
Bonus: Extending our language with print
If we extend our language with a print command, how can we extend our semantics to model the output behavior? Lets say this allows us to do things like print(add(2, 2)). We'll also allow print to be used inside expressions like add(print(1), 3). In these cases, print will just return its argument after it prints to the screen. Further, we will include a "sequencing operator" called ;. For example, print(1) ; print(3) will print both 1 and 3 and it will evaluate to 3.
So, now we can have programs like this
print(sub(add(2, 4), 1);
print(7);
10

Also, we can have prints embedded in expressions like this:
add(print(3), 5)

We will also say that the semicolon operator will evaluate both sides and just return the second. So, print(3); print(7) will print 3 and 7 and it will evaluate to 7.
We will say that a print like this will print to the screen when it gets evaluated and it will return the its argument. So this will print 3 to the screen and the whole expression will evaluate to 8.
Our original small-step relation relates two expressions. But this can't really tell us anything about effects like output. What we really need to do is relate two pairs, where the first item is an expression and the second item is a list of numbers. The list of numbers will represent our output.
First, we need to briefly establish a notation for lists of numbers. We will use $[]$ for the empty list. $[1,2,3]$ will be a list of the numbers $1$, $2$ and $3$. To prepend a single element to the head of the list, we will use $::$. So, $10 :: [1,2,3]$ is the same as the list $[10,1,2,3]$.
I will use the (meta-)variable $\omega$ to represent the list of output: omega for "output".
Our small-step evaluation judgment will now have this form:
$$
\fbox{$\langle e, \omega \rangle \longrightarrow \langle e, \omega \rangle$}
$$
That is, on both sides it takes a pair consisting of an expression and a list of numbers.
A crucial point: Whenever we see $\langle e, \omega \rangle \longrightarrow \langle e', \omega' \rangle$, this means "given that we have the output $\omega$ so far, expression $e$ evaluates to $e'$ in one-step and changes the output to $\omega'$.
Let's first look at a couple of specific examples.

$\verb|add|(2, \verb|add|(4,4))$ should not do anything to the output, so if we are evaluating that expression when we've already printed $20$ to the screen we have $\langle \verb|add|(2, \verb|add|(4,4)), [20] \rangle \longrightarrow \langle \verb|add|(2, 8), [20] \rangle$. We left the output unchanged, since the evaluation step did not print anything.

If, instead, we look at evaluating $\verb|add|(5, \verb|print|(7))$ and we have already printed $10$, then we have $\langle \verb|add|(5, \verb|print|(7)), [10] \rangle \longrightarrow \langle \verb|add|(5, 7), [7, 10] \rangle$. Note that we extended our output list, since we printed something to the screen.


Now, let's generalize this. Here is what [E-Add-1] becomes with this new $\longrightarrow$ relation:
$$
\cfrac{\langle e_1, \omega \rangle \longrightarrow \langle e_1', \omega' \rangle}
  {\langle \verb|add|(e_1, e_2), \omega \rangle \longrightarrow \langle \verb|add|(e_1', e_2), \omega' \rangle}~[\text{E-Add-1}]
$$
This is very similar to our original rule. In fact, if you cover up the $\omega$s and the pair brackets, it is identical to our original rule! In our new rule, we just pass the output from evaluating our left argument. This makes sense because $\verb|add|$ does not, by itself, do anything to change the output.
Now it's pretty critical to figure out how to evaluate print itself! For this, we will have two rules. One to evaluate its argument (much like how $\verb|add|$ works) and one to actually perform the printing.
$$
\cfrac{\langle e, \omega \rangle \longrightarrow \langle e', \omega' \rangle}
  {\langle \verb|print|(e), \omega \rangle \longrightarrow \langle \verb|print|(e'), \omega' \rangle}~[\text{E-Print-1}]
$$
Note we do not actually do anything here, other than evaluate the argument and pass the resulting output (if any) through.
The rule for actually printing:
$$
\cfrac{}
  {\langle \verb|print|(\underline{n}), \omega \rangle \longrightarrow \langle \underline{n}, \underline{n} :: \omega \rangle}~[\text{E-Print}]
$$
If our argument is a value $\underline{n}$, we can print $n$ to the screen (which we represent by extending the list $\omega$ to be $\underline{n} :: \omega$) and we evaluate to $\underline{n}$.
Another important piece is the semicolon operator (sequencing operator). We have three rules for this:
$$
\cfrac{\langle e_1, \omega \rangle \longrightarrow \langle e_1', \omega' \rangle}
  {\langle (e_1 ; e_2), \omega \rangle \longrightarrow \langle (e_1' ; e_2), \omega' \rangle }~[\text{E-Seq-1}]
$$
$$
\cfrac{\langle e_2, \omega \rangle \longrightarrow \langle e_2', \omega' \rangle}
  {\langle (\underline{n} ; e_2), \omega \rangle \longrightarrow \langle (\underline{n} ; e_2'), \omega' \rangle}~[\text{E-Seq-2}]
$$
$$
\cfrac{}
  {\langle (\underline{n_1} ; \underline{n_2}), \omega \rangle \longrightarrow \langle \underline{n_2}, \omega \rangle }~[\text{E-Seq}]
$$
Lets try this out by making a derivation for $\verb|add|(\verb|print|(5), \verb|print|(10))$ using our small-step relation. Remember, this will be one evaluation step. We will say we haven't printed anything so far at the start of evaluation. I will incrementally write the derivation out step-by-step and use $e$ and $\omega$ as placeholders for what we haven't figured out yet (the things we need to figure out by continuing to write the derivation.
First, we evaluate the left argument of $\verb|add|$.
$$
\cfrac{\langle \verb|print|(5), [] \rangle \longrightarrow \langle e, \omega \rangle }
  {\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(e, \verb|print|(10)), \omega \rangle }~[\text{E-Add-1}]
$$
Now we need to figure out how to evaluate $\verb|print|(5)$ where we have no output so far:
$$
\cfrac{
   \cfrac
 {}
 {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
  {\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
$$
Remember, $5 :: []$ is the same as $[5]$.
Thanks to @theonlygusti for the comment about this.
Exercise: What do we get when we fully reduce $\verb|print|(\verb|add|(\verb|print|(5), \verb|print|(10)))$?
A multi-step derivation example with print
Let's take another look at our example $\verb|add|(\verb|print|(5), \verb|print|(10))$. We will use the multi-step relation $\longrightarrow^{*}$ to fully reduce it this time. We'll also see why we need an output state on both sides of the arrow.
First, we need to update our multi-step relation rules to use output.
$$
\cfrac{}
{\langle e, \omega \rangle \longrightarrow^{*} \langle e, \omega \rangle}~[\text{E-Done}]
$$
$$
\cfrac{\langle e, \omega \rangle \longrightarrow \langle e', \omega' \rangle ~~~ \langle e', \omega' \rangle \longrightarrow^{*} \langle e'', \omega'' \rangle}
{\langle e, \omega \rangle \longrightarrow^{*} \langle e'', \omega'' \rangle}~[\text{E-Step}]
$$
Note how the state is fed through the two premises of [E-Step].
Now, to the example. We will start with the single step derivation we had before:
$$
\cfrac{
   \cfrac
 {}
 {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
  {\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
$$
This will be one of the premises of the multi-step derivation:
$$
\cfrac{
  \begin{array}{c c}
  \cfrac{
 \cfrac
   {}
   {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
%
&\cfrac{\cdots}{\langle \verb|add|(5, \verb|print|(10)), [5] \rangle \longrightarrow^{*} \langle e, \omega \rangle} \end{array}}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow^{*} \langle e, \omega \rangle}~[\text{E-Step}]
$$
I have filled in the one step which we already computed before. This is used as the first premise for the multi-step inference rule [E-Step]. Now, we need to do the rest by figuring out the second premise. Then, we will be able to update the conclusion by replacing $e$ with the evaluation result and $\omega$ with the final output.
So, doing steps until we reach a value we get this somewhat complicated looking derivation:
$$
\cfrac{
  \begin{array}{c c}
  \cfrac{
 \cfrac
   {}
   {\langle \verb|print|(5), [] \rangle \longrightarrow \langle 5, [5] \rangle}~[\text{E-Print}]}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow \langle \verb|add|(5, \verb|print|(10)), [5] \rangle }~[\text{E-Add-1}]
%
&\cfrac{
 \begin{array}{c c}
   \cfrac{
   \cfrac{}
     {\langle \verb|print|(10), [5] \rangle \longrightarrow \langle 10, [10, 5] \rangle}~[\text{E-Print}]
   }
 {\langle \verb|add|(5, \verb|print|(10)), [5] \rangle \longrightarrow \langle \verb|add|(5, 10), [10,5] \rangle}~[\text{E-Add-2}]&
   \cfrac{
   \begin{array}{c c}
     \cfrac{15 = 5 + 10}
       {\langle \verb|add|(5, 10), [10,5] \rangle \longrightarrow \langle 15, [10,5] \rangle}~[\text{E-Add}]&
     \cfrac{}
       {\langle 15, [10,5] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Done}]
   \end{array}
  }
{\langle \verb|add|(5, 10), [10,5] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Step}]
 \end{array}
}
  {\langle \verb|add|(5, \verb|print|(10)), [5] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Step}]
%
\end{array}}
{\langle \verb|add|(\verb|print|(5), \verb|print|(10)), [] \rangle \longrightarrow^{*} \langle 15, [10,5] \rangle}~[\text{E-Step}]
$$
Now, this is difficult to read. It spells out all of the dependencies, but this verbosity is what makes it challenging.
But note how the output state gets threaded through the steps. If the step that executed $\verb|print|(10)$ did not know that we already printed a $5$, then it could not know how to give the correct new output of $[10,5]$ (I have the lists going "backwards" from how the actual output would work, but this is not necessary).
You might wonder if we can leave out the outputs on the left-hand side of the single-step relation and then combine the right-hand outputs together in the multi-step relation. But remember that we are looking at the very special case of printing to a screen. In this case, we can concatenate outputs. But, in general, effects don't necessarily work this way.
Comparison to reference interpreters
@JerryCoffin brings up a very good point in the comments: Why not use a "reference interpreter?" How does this approach compare? A reference interpreter is where you define a semantics by giving an actual interpreter written in an existing language like Haskell.
A very big difference is the complexity. Any programming language that can be used to practically write an interpreter is going to be far, far more complex than the "language" of inference rules!
For example, Haskell has nontermination, exceptions, a specific evaluation order, etc. It has things like higher-order functions and a standard library. Other languages might have classes and objects. Inference rules have none of those things. Inference rules don't even have functions! The only thing an inference rule can do is say "if you know these things, then you can derive this thing". That is the only "abstraction" given to you by the language of inference rules. Note how I had to specifically spell out the evaluation order for $\verb|add|$. But we can use this framework to specify languages.
There are only two things in the "language of inference rules": judgments (like $\longrightarrow$) and inference rules. We can also make use of basic mathematical constructs like our use of $=$ and $+$ in the rule [E-Add]. But note that even this is used very rarely!
One advantage of this simplicity is that it makes it much easier to write proofs, compared to using a reference interpreter. If we tried to write a proof about evaluation of our language and we used a reference interpreter written in Haskell, we would need some kind of semantics for Haskell in addition to a semantics for our language (at least informally). Here, we don't need that.
Additionally, it inherently provides a way visualize how a result is computed in the form of derivations. All of the dependencies the evaluation of subexpressions are shown in these derivations.
Reference interpreters have their place, but the approach outlined here also has advantages. The approach here is very frequently used in academic settings over many decades. Most programming language papers that give an "execution" semantics will give it in this style.
Further topics

Another very important topic is the way that an operational semantics relates to a type system. It is often desirable to prove that the language has a property called "syntactic type soundness." This is outside the scope of this answer.

When we give a denotational semantics for a language, we usually want the two semantics to be very closely linked with each other. The basic theorem linking them that you always want to hold is called "adequacy." There is also a stronger theorem that holds for some semantics called "full abstraction." There is some more detail at the end of this answer. Another answer should cover this in more detail. There is also background on denotational semantics more generally here and here.


References
Talks

Basic Mechanics of Operational Semantics by David Van Horn

Books

Types and Programming Languages by Benjamin Pierce
Practical Foundations for Programming Languages by Robert Harper
Formal Semantics of Programming Languages by Glynn Winksel

Papers

A Structural Approach to Operational
Semantics by Gordon Plotkin (Plotkin is the origin of this kind of operational semantics)
> **Comments:**
> **username_0** (2023-12-11): @theonlygusti That's a good question! For `print`, you would typically do that like this: Instead of relating two expressions, we have $\longrightarrow$ relate two pairs. The pairs consist of an expression and a list of the outputs. If we extend our language with `print`, everything except `print` will ignore the "output" part of the pairs. `print` will extend the list. I'll add a section to my answer about this.  
> **username_0** (2023-12-11): @JerryCoffin It has been extremely widely used in academic contexts for the last 40+ years. If you look at almost any paper describing "execution" semantics of a PL written in that time, it will be written in this style. You cannot describe an "execution trace" as easily (or as visually) if you only have it written in Haskell. And as much as I love Haskell, it is also far more complicated. If you want to prove something about a Haskell program, then you need to worry about the evaluation order of Haskell, etc (basically, you will *also* need some kind of semantics of Haskell).  
> **username_0** (2023-12-11): Compared to the semantics of Haskell, there is actually very little involved in this representation! There are just inference rules, which say "if you know these things, then you are allowed to derive this thing." In this language of inference rules, there are no "exceptions," no specific evaluation order, no "nontermination", etc. Not even any functions! It is more fundamental and "simple" than that (not to say that it is necessarily, at first, easy to learn).  
> **username_0** (2023-12-11): What you're describing is a *reference interpreter*. That has its place too, but what I'm describing here also has a place. Also, your comment is not too negative at all! I appreciate the feedback!  
> **username_0** (2023-12-11): @JerryCoffin I added a section addressing your comment, since I think this is a very useful topic to discuss. I hope that helps. Also somewhat relatedly, at some point, I might work on a web-based thing that will take code written in a small language and interactively show you how derivations for the multi-step evaluation relation are constructed. This will show the relationship between an interpreter and an operational semantics.  
> **username_11** (2023-12-12): "*the same general notation that formal typing rules are written in*" - aka [The most popular programming language in computer science](https://www.youtube.com/watch?v=dCuZkaaou0Q)  
> **username_0** (2023-12-12): @theonlygusti Remember that the $\longrightarrow$ is a *single* step. We need to perform several single steps to fully reduce something, in general. In order to know what to produce as output, we need to know what we've outputted so far. You might wonder now why not just concatenate the single-step outputs in our multi-step relation? Well, remember that we are looking at the very special case of printing something. Other effects might not be things you can just concatenate. I added a subsection to my answer addressing this in more detail.  
> **username_12** (2023-12-12): Wouldn't a simpler way of defining sequencing be (e1,w) -> (e1',w') => ((e1;e2),w) -> (e2,w')?  
> **username_13** (2023-12-13): OP wrote: *"I want to write in a way that is widely understood."* Unfortunately, I don't think the shown inference rule notation is widely understood by the general population of programmers.  
> **username_14** (2023-12-14): @G.Sliepen: It is, however, widely understood by computer scientists, and while programmers _may not_ at first understand it, it is simple enough that they should be able to in relatively short order.  
> **username_0** (2023-12-15): @Moonchild That does not quite work. Remember that $\longrightarrow$ does exactly one step. So, the premise of your rule would evaluate the first expression exactly one step and then throw away the rest. I have written up a counterexample in Agda [here](https://github.com/roboguy13/agda-stuff/blob/5aec8c753959f54d79c73a5e051db4b42e420143/calc/CalcSmallStep.agda#L255-L273), showing that the two semantics are different. It shows that $\verb|add|(\verb|print|(1), \verb|print|(2)) ; \verb|print|(3)$ cannot produce the same output in the new semantics as the old semantics.  
> **username_0** (2023-12-15): @Moonchild What you're describing is much closer to how a big-step semantics would work. [Here](https://github.com/roboguy13/agda-stuff/blob/5aec8c753959f54d79c73a5e051db4b42e420143/calc/CalcBigStep.agda#L32-L36) is the relevant rule of a big-step semantics for the language. Also, I've shown in that file that the big-step semantics I give there is equivalent to the small-step semantics I've shown earlier.  
> **username_15** (2023-12-16): Small-step semantics is typically about making it easy to prove theorems. Since OP is trying to convey understanding, a big step, natural deduction semantics might be a better choice.  
> **username_0** (2023-12-16): @NormanRamsey While I do agree with that, the OP was intending to set this up to specifically ask for small-step semantics. The reason for using the phrase "step-by-step" is to be more suggestive of small-step semantics. As you point out, while big-step definitely has its own advantages, small-step can be very useful for proving things and so it conveys another sort of understanding of a language. I am certain that this is the intention since I am the OP =) I wanted to collect some fundamental theory concepts into some Q&A's here, to stimulate discussion a bit (and because it's useful & fun).  
> **username_0** (2023-12-16): I wanted to talk about small-step here in particular because I wanted to talk about type soundness later (which I recently wrote an answer about). Also along the lines of your comment: A contextual/reduction semantics would often be better in this situation than a traditional small-step semantics. However, you must understand how a typical small-step semantics works before you can learn about contextual semantics. If I can find a good way to frame the question, I might write one about this at some point.  
---
### Answer by username_9 on 2023-12-14. Score: 0
Executable specifications
Essentially an independent executable test suite for the language written in the language itself that exercises every part of it, showcases every feature and checks that language semantics are implemented correctly by running the code and testing the results. Not exactly formal but certainly "more formal" than just publishing a reference implementation.
The Ruby Spec is a concrete example of such a thing. It is written in Ruby itself and executes test cases that check whether the Ruby implementation contains the specified features and that they behave according to Ruby semantics. For example, Ruby arrays are specified like this:
describe "Array literals" do

  it "[] should return a new array populated with the given elements" do
    array = [1, 'a', nil]
    array.should be_kind_of(Array)
    array[0].should == 1
    array[1].should == 'a'
    array[2].should == nil
  end

  # ...

  it "[] treats splatted nil as no element" do
    [*nil].should == []
    [1, *nil].should == [1]
    [1, 2, *nil].should == [1, 2]
    [1, *nil, 3].should == [1, 3]
    [*nil, *nil, *nil].should == []
  end

  # ...

end

They fulfill the criteria you listed:

I don't want to require people to read the interpreter code to learn my language's semantics.

With an executable specification, people can read and run code written in your high level language instead.

I want a single definitive resource for the semantics of my language.

The executable specification provides a single source of truth, in executable format.

Maybe other people want to make an interpreter. It would be better to have a definitive document than require them to test the behaviour of their interpreter against mine.

The executable specification is independent of your reference implementation. People can run it on their interpreters too. If it runs and passes all tests, they can confidently say they created an implementation of your language.

I want to write in a way that is widely understood.

Code is widely understood by programmers. It's also understood by computers.

I want to prove properties about my language.

Successfully running the executable specification proves that it behaves as specified. Probably not as rigorous as formal proofs in the mathematical sense but still extremely useful.

I'm looking for something that, at a high-level, specifies the step-by-step execution of my language in a similar way to how an interpreter would be written.

That "something" reminds me of "code", which is what executable specifications are made out of. Code specifies at a high level the instructions that must be executed to carry out the program, and all interpreters I know are implemented using code.
---
### Answer by username_10 on 2023-12-11. Score: -2
In many cases, specifying a language by specifying all of the ways an implementation would be allowed to process the constructs therein may be more useful and precise than trying to formalize rules about program constructs themselves. An objection some people may have to the approach described in David Young's answer is that it doesn't accommodate optimizations, but that doesn't mean that it couldn't be tweaked to do so.

For example, a specification for how a language is processed may specify that operations may be performed in a sequence which differs from specified in the absence of certain constructs where execution is deemed to be important; programmers would not be required to avoid all possible situations where processing things out of sequence might be observable, but would be required to accommodate the variations in sequence that might occur.

If in the absence of optimization, division by zero would have behavior defined as trapping, an "optimization-friendly" dialect might specify that such traps are not considered a "sequenced side effect". That would not imply a requirement that divisions by zero be prevented at all costs, even in response to invalid input, but rather that a program that might attempt a division by zero prepared for the possibility that the attempted division might have been performed out of sequence, and this may result in an arbitrary subset of the operations between the previous and succeeding "causality barrier" directives being executed before the trap fired. While that may leave parts of a program's state inconsistent with anything that could have resulted from sequential program execution, recognizing such a state as a natural consequence of an allowable reordering of operations would avoid the need to characterize it as "anything can happen" UB.
> **Comments:**
> **username_0** (2023-12-12): Hmm, I'm not sure I fully understand what you're suggesting. You can represent nondeterminism in an operational semantics. In fact, it is often slightly easier to do this than to make things deterministic, because you remove requirements. if you take my rule [E-Add-2] and remove the requirement that $n$ be a value, then we have made the evaluation order of $\verb|add|$ undefined. The semantics would allow for both left-to-right and right-to-left evaluation of the arguments of $\verb|add|$.  
> **username_10** (2023-12-12): @DavidYoung: Consider the cited example of divide-by-zero behavior.  Specifying that an implementation may reorder a division operation ahead of across other operations upon which its operands do not depend, or defer it across other operations that do not depend upon its result, and that if the division were to trap, any sequence of observable operations that could result from that would be a legitimate way for the implementation to behave, would seem cleaner and simpler than trying to specify what "conforming" programs are allowed to do.  
> **username_10** (2023-12-12): @DavidYoung: While a choice of which operand to "+" is evaluate first may be a simple "Unspecified" choice, I don't see any way of saying that e.g. `do { extern1++; x = y/z; ... } while(whatever);` might be processed in a way that could trap without incrementing `extern1`, that would be easier than saying that an implementation may reorder the division ahead of preceding actions upon which its operands have no dependencies, in a manner *agnostic* to whether the division might trap.  
> **username_10** (2023-12-12): @DavidYoung: With regard to "real" non-determinism, "benign" race-condition behaviors could be described using a non-deterministic model that would allow for e.g. `uint16_t x = *p; int y = x - (x >> 15);` to be processed in a manner that could yield 65535 if `*p` changes from 65535 to 0 or vice versa during its execution, but provide programmers with a way of writing the expression so as to guarantee that `*p` is read *at most* once (without making it `volatile` and forcing it to be read *exactly* once), but it may be easier to reason about by specifying when compilers may "invent" reads.  
---
