38

Small-step semantics defines a method to evaluate expressions one computation step at a time. Formally speaking, a small-step semantics for an expression language $E$ is a relation $\rightarrow : E \times E$ called the reduction relation. Small-step semantics describes what happens to an expression in detail. It's able to give a precise account of even non-...


25

This is a standard notation for an inference rule. The premises are put above a horizontal line, and the conclusion is put below the line. Thus, it ends up looking like a "fraction", but with one or more logical propositions above the line and a single proposition below the line. If you see a label (e.g., "LET" or "VAR" in your example) next to it, that's ...


15

This is something that I think is not explicitly pointed out or not pointed out with enough emphasis in many, even introductory, CS/type theory/logic texts. $\vdash$ doesn't mean anything. Instead, in this example, the three place relation $- \vdash - \Rightarrow -$ is what has meaning. Except that was a lie. It doesn't a priori have meaning either. That ...


11

There is no real agreement what characterises denotational semantics (see also this article), except that it must be compositional. That means that if $\newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack} \SEMB{\cdot}$ is the semantic function, mapping programs to their meaning, something like the following must be the case for all $n$-ary program ...


10

The meaning of the words is not fixed, but I can give you my interpretation. A calculus is something that we calculate with in the sense of juggling equations (think manipulation of Taylor series or computation of integrals in analysis). A calculus tells us what the rules of manipulation are, but not which ones we should used in a given situation. A ...


10

The state can change in subsequent reduction steps because on the right hand side of $$ \langle while\ B\ do\ S, \sigma \rangle \quad\rightarrow\quad \langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle $$ the $while$-loop is guarded (preceeded) by $S$. The computation of $S$ may change the state so that the ...


10

In programming language semantics, the notion of program state is not a vague philosophical notion, but a very precise mathematical one. A state $s$ in this small-step operational semantics is a partial function $$ s : \mathbf{Var} \hookrightarrow \mathbb{Z} $$ that records the values of the variables. So if $s\, x = v$, then variable $x$ has value $v$. ...


9

The state $\sigma$ does not change when we consider $B$ to decide whether to perform one iteration of the loop, but it can change later when we run the body $S$. And so, the next time we consider $B$, there can be a change of $\sigma$.


9

There are many compilers, which compile widely different kinds of languages which serve widely different purposes. For example, a database language will have very different optimizations than an array-based language like APL. Compilers themselves use several intermediate languages, from the input language, to a de-sugared version of the input language, all ...


8

There is an (operational) semantics for Java 1.4 formulated in the $\mathbb{K}$ framework. Associated to this framework is a proof system called Matching Logic. While that page describes a prototype implementation, it seems that the functionality is being incorporated into the $\mathbb{K}$ framework tools themselves as kprover. Unfortunately, it seems the ...


8

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


7

Here is a very informal explanation that might help people unfamiliar with formal notations to get a foot in the door. It does not replace a formal definition! The Ap is the state of your system or your running program. "State" can mean a lot of things but in this case it seems to include a list of all defined local variables and their values. Why is Ap a ...


7

Featherweight Java is quite highly regarded in the PL community. But if that doesn't suit your needs, here's a general approach to modelling: Formalize your language's AST into expressions and statements Write a semantics for expressions and statements. Your semantics will need: an evaluation relation, relating expression-state pairs $(e,\sigma)$ to an ...


6

I think your examples show you do somehow understand the basic points of the several styles of semantics. Still, note that the whole point of having a semantics of a programming language is to have a formal, mathematically rigorous description of the program behavior. That inherently involves math and several formulae -- one can't really do without math. ...


5

I'll write $O(p,\sigma)$ for the only $\sigma'$ so that $\langle p, \sigma \rangle \to \sigma'$ (and $\bot$ if it doesn't exist) and $D(p)$ for the denotational semantics of $p$. Note that if you define both semantics properly, you'll most likely have $O(p,\sigma)=D(p)(\sigma)$. I'll write $S(p)$ to mean either $\sigma\mapsto O(p,\sigma)$ or $D(p)$. Now ...


5

Your attempt does not work. Note that $s_1$ is never executed. (And if you prepend the right-hand side with "$s_1;$", it will be executed multiple times.) What you can do is to translate the for loop into an equivalent while loop: $$\sigma,\text{for } s_1, e_1, e_2, s_2 \text{ endfor} \to \sigma, s_1; \text{while } e_1 \text{ do } s_2; e_2 \text{ endwhile}....


4

The induction should be on the derivation of $t \to^* t'$: If $t \to t'$ in one step, then we get the desired result by the E-IF rule. Suppose $t \to^* t'$ because $t \to t'' \to^* t'$. By the E-IF rule we have $$(\mathtt{if}\;t\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to (\mathtt{if}\;t''\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3)$$ and by the ...


4

I think you have it a bit backwards: proving type preservation is a good property of the type system with respect to the operational semantics, rather than the opposite. Alternately: the whole point of a programing language is the ability to use it to perform some computational task. Because of this, the operational semantics is one of the requirements of ...


3

Don't proceed by induction on $P$, i.e. by structural induction on the syntax of programs. This is because structural induction is quite weak, and is likely to fail on while loops. Look at the inference rules for the big step semantics for while, in particular at the while-true rule which handles the case where the guard is true. In such case, you'll see ...


3

Coinductive Big-Step Semantics for Concurrency by Tarmo Uustalu writes: Second, contrary to what is so often stated, concurrency is not inherently small-step, or at least not more inherently than any kind of effect produced incrementally during a program’s run (e.g., interactive output). Big-step semantics for concurrency can be built by ...


3

I'm going to assume that all the allowed values for $x$ are (unbounded) integers. In that case your proposal somewhat makes sense, insomuch as $e$ is some arbitrary well-formed expression (which evaluates to some value in the context $\sigma$). But it's just as easy to write this $$\frac{n\in\mathbb{Z}}{(\mathrm{havoc}\ x,\sigma)\rightarrow (x:=n,\sigma)} $...


2

Operational semantics utilizes the tools of logic, so as a prerequisite we must understand judgements and inference rules. A judgement is like a proposition, but more general. It asserts a relation between two entities of our language. For example, in programming, we often employ the judgement $e: \tau$, asserting that expression $e$ has type $\tau$. ...


2

It seems you have some doubts about the first added evaluation rule $$ \frac {\langle B, s \rangle \to \!\, \langle B', s' \rangle} {\langle \mathsf{assert}\ B\ \mathsf{before}\ C, s \rangle \to \!\, \langle \mathsf{assert}\ B'\ \mathsf{before}\ C, s' \rangle} $$ It might be redundant, but I ought to point out it's one rule: the top part is called a premise ...


2

I found the solution to my answer: ADTs can be represented by a combination of sum-types and tuples enter link description here. In that representation, every construction takes exactly one argument (possibly the unit value). Two special tagging forms, inl and inr for "inject left" and "inject right" are introduced. These forms allow the encoding of ...


2

At the beginning of Section 2.4 the book explains that $\mathcal{P}(J)$ stands for a property of a judgment $J$. That is, the $\mathcal{P}$ in $\mathcal{P}(a\ \mathtt{nat})$ does not stand for a property of numbers, but a property of the judgment $a\ \mathtt{nat}$, which is the judgment that "$a$ is a number". It just so happens that the inference rules for ...


2

The main advantage of having a Programming Language that is not Turing Complete is that your language can be strongly normalizing, that is, you can ensure that all terms halt with a unique, well formed value. I've come across non-Turing complete languages primarily with proof assistants. When you're using programs to prove theorems, you need to make sure ...


2

I haven't seen anything on this but the closest I could find is Evolving Algebras: Evolving Algebras: An Attempt to Discover Semantics Evolving Algebras: Mini-Course Communicating Evolving Algebras In that mini course there are several papers outlining different aspects and applications of the Evolving Algebra. From one of them: In 1988 Yuri Gurevich ...


2

The usual definitions of Turing machines are given in terms of formal semantics. For instance, the Wikipedia definition describes Turing machines in precise mathematical formalism. If you are looking for something even more formal, have a look at this Coq formalization of Turing machines.


1

You could add more flow control to IMP, like (simple) exceptions, or break to exit early from a while loop. You could some partial operators (division, square root) requiring you to handle runtime errors. You could add more complex data types, like pairs. Make it so that e.g. projecting a value out of a non-pair value causes a runtime error. Craft a (first-...


1

"Programming language" and "calculus" are polysemic terms, that is, they mean different things depending on the context. In some contexts, programming languages and calculi have converged to refer to the same concept, that of a rewriting system based on a set of formal rules that can be "mechanically" applied. The reason why this convergence is ...


Only top voted, non community-wiki answers of a minimum length are eligible