25 votes
Accepted

What is this fraction-like "discrete mathematics"–style notation used for formal rules?

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 ...
D.W.'s user avatar
  • 158k
15 votes

What does ⊢ mean in operational semantics?

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, ...
Derek Elkins left SE's user avatar
13 votes
Accepted

What questions can denotational semantics answer that operational semantics can't?

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 \...
Martin Berger's user avatar
10 votes

Why does the state remain unchanged in the small-step operational semantics of a while loop?

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}};\ ...
Martin Berger's user avatar
10 votes
Accepted

Why does the state remain unchanged in the small-step operational semantics of a while loop?

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 ...
Hans Hüttel's user avatar
  • 2,486
10 votes
Accepted

What's the difference between a calculus and a programming language?

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 ...
Andrej Bauer's user avatar
  • 30.3k
9 votes
Accepted

What formal representation is commonly used to describe compiler optimizations?

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-...
cody's user avatar
  • 8,154
9 votes

Why does the state remain unchanged in the small-step operational semantics of a while loop?

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$, ...
Andrej Bauer's user avatar
  • 30.3k
8 votes

Formal model of execution for Java (or general imperative language)

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 ...
Derek Elkins left SE's user avatar
8 votes

When would one use equational dynamics?

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 ...
Andrej Bauer's user avatar
  • 30.3k
7 votes

What is this fraction-like "discrete mathematics"–style notation used for formal rules?

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 ...
trunklop's user avatar
  • 171
7 votes
Accepted

Formal model of execution for Java (or general imperative language)

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 ...
Joey Eremondi's user avatar
6 votes
Accepted

What's the difference between: operational, denotational and axiomatic semantics?

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 ...
chi's user avatar
  • 14.5k
6 votes

What questions can denotational semantics answer that operational semantics can't?

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 ...
xavierm02's user avatar
  • 1,245
4 votes

What makes an operational semantics good?

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 ...
cody's user avatar
  • 8,154
3 votes
Accepted

Mitchell FPL 3.6.2 (Show that equation does not hold in initial algebra)

If all you need to show is that union a b = union b a is not provable, where a and b are ...
Andrej Bauer's user avatar
  • 30.3k
3 votes

How does one prove that Big Step semantics and Small Step semantics are equivalent for IMP?

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 ...
chi's user avatar
  • 14.5k
3 votes
Accepted

How is a Transition System in Operational Semantics defined?

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 ...
gardenhead's user avatar
  • 2,230
3 votes

How to write operational semantics rule for havoc x?

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 ...
cody's user avatar
  • 8,154
3 votes
Accepted

defining the operational semantics of a concurrent language

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 ...
Gergely's user avatar
  • 379
2 votes

What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics?

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 \!\, \...
Anton Trunov's user avatar
  • 3,469
2 votes

Software code generation from the (operational) semantics - reference request for automatic programming

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 ...
Lance's user avatar
  • 2,193
2 votes

What is the semantics of a Turing machine?

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 ...
Andrej Bauer's user avatar
  • 30.3k
2 votes

What are the benefits of languages that are not Turing complete?

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 ...
Joey Eremondi's user avatar
2 votes
Accepted

Show that if <S1;S2,s> => * s', it is not necessarily the case that <S1,s> =>* s'

The proof you give is a counterexample of the reciprocal. That is, you're giving an example where $\langle S_1, s\rangle \Rightarrow^* s'$ but not $\langle S_1; S_2, s\rangle \Rightarrow^* s'$. To ...
Carlos Miguel Soto's user avatar
2 votes

What is the definition of a redex and what are they for in programming languages literature?

A redex is an expressions on which we can perform a computation step, such as: fst (a, b) is a redex, it computes to a ...
Andrej Bauer's user avatar
  • 30.3k
1 vote
Accepted

From big-step to small-step semantics

Here are a couple articles on the matter. From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation and Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step ...
dader's user avatar
  • 214
1 vote
Accepted

Examples of interesting semantics to study during a small project for a graduate Semantics course

You could add more flow control to IMP, like (simple) exceptions, or break to exit early from a while loop. You could some ...
chi's user avatar
  • 14.5k
1 vote

What's the difference between a calculus and a programming language?

"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 ...
André Souza Lemos's user avatar
1 vote

What's the difference between a calculus and a programming language?

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 ...
xavierm02's user avatar
  • 1,245

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