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 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$. ...


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 ...


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 ...


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$.


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 ...


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 ...


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 ...


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 ...


6

The language of inference rules are much more general than what is usually given in Logic. Indeed you can look at systems with rules of the shape $$ \frac{\Theta_1\ldots \Theta_n}{\Theta}$$ Where the $\Theta_i, \Theta$ are some kind of statement and ask: what are all the possible $\Theta$ I can get by repeated application of these rules? In the above case,...


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

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

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 ...


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 ...


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 ...


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

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)} $...


3

There are two systems of operational semantics: small-step and big step. The symbol $\Downarrow$ is used in the latter to denote "this term evaluates to that final value". E.g., $t \Downarrow v$. There is a short discussion of the system in Pierce's Types and Programming Languages pages 42-43. The $\vdash$ is used to imply that if the types on the left hand ...


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 ...


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

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

"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 ...


2

The goal of calculi is not just to study program equivalences, it's to study programs. An example of fancy calculus is this where the strategy (call-by-value or call-by-name) is determined locally. It could be implemented someday in a programming language but it's first studied as a calculus. You also use calculi to study type systems (with some calculi such ...


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$. ...


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