19
$\begingroup$

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?

$\endgroup$
20
  • 1
    $\begingroup$ @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). $\endgroup$ Dec 11, 2023 at 17:08
  • 1
    $\begingroup$ 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! $\endgroup$ Dec 11, 2023 at 18:28
  • 1
    $\begingroup$ 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. $\endgroup$ Dec 11, 2023 at 21:27
  • 1
    $\begingroup$ @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 $\endgroup$ Dec 11, 2023 at 21:59
  • 1
    $\begingroup$ "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) $\endgroup$ Dec 11, 2023 at 22:42

3 Answers 3

24
$\begingroup$

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

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

$\endgroup$
17
  • 3
    $\begingroup$ How do you describe something a bit more complicated and further removed from mathematics than pure functions, like how your language's print statement should work? $\endgroup$
    – minseong
    Dec 11, 2023 at 13:57
  • $\begingroup$ @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. $\endgroup$ Dec 11, 2023 at 16:37
  • $\begingroup$ @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). $\endgroup$ Dec 11, 2023 at 18:59
  • $\begingroup$ 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). $\endgroup$ Dec 11, 2023 at 19:01
  • 1
    $\begingroup$ "the same general notation that formal typing rules are written in" - aka The most popular programming language in computer science $\endgroup$
    – Bergi
    Dec 12, 2023 at 0:20
0
$\begingroup$

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.

$\endgroup$
-2
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ 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|$. $\endgroup$ Dec 12, 2023 at 7:40
  • $\begingroup$ @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. $\endgroup$
    – supercat
    Dec 12, 2023 at 15:49
  • $\begingroup$ @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. $\endgroup$
    – supercat
    Dec 12, 2023 at 15:57
  • $\begingroup$ @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. $\endgroup$
    – supercat
    Dec 12, 2023 at 16:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .