Questions tagged [operational-semantics]
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms.
44
questions
30
votes
1answer
9k views
Difference Between Small and Big-step Operational Semantics
What's the fundamental difference(s) between small and big-step operational semantics?
I'm having a hard time grasping what it is and the motivation for having the two.
18
votes
2answers
3k views
What is this fraction-like “discrete mathematics”–style notation used for formal rules?
In the paper "A Conflict-Free Replicated JSON Datatype", I encountered this notation for formally defining "rules":
What is this notation called? How do I read it?
For example:
the ...
14
votes
2answers
460 views
What questions can denotational semantics answer that operational semantics can't?
I am familiar with operational semantics (both small-step and big-step) for defining programming languages. I'm interested in learning denotational semantics as well, but I'm not sure if it will be ...
13
votes
3answers
426 views
What's the difference between a calculus and a programming language?
I think I'm pretty confused about what's called a calculus and what's called a programming language.
I tend to think, and might have been told, that a calculus is a formal system for reasoning about ...
9
votes
3answers
927 views
Why does the state remain unchanged in the small-step operational semantics of a while loop?
Usually I see that in the structural operational semantics representation for the while loop, the program state don't change:
$(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> ...
7
votes
2answers
173 views
Formal model of execution for Java (or general imperative language)
I'm trying to prove some statements about execution in Java programs under some heavy restrictions (basically I have a conjecture that if two methods satisfy a set of constraints for a given input ...
7
votes
1answer
271 views
Reduction rule for IF?
I'm working through Simon Peyton Jones' "The Implementation of Functional Programming Languages" and on page 20 I see:
IF TRUE ((λp.p) 3) ↔ IF TRUE 3 (per β red) (1)
...
6
votes
1answer
48 views
When would one use equational dynamics?
I'm trying to sort out in my mind the different ways of assigning semantics to a programming language. There are two main methodologies: operational semantics and denotational semantics (I asked a ...
6
votes
1answer
2k views
What's the difference between: operational, denotational and axiomatic semantics?
Recap of the terms from the dictionary:
semantics: the study of meaning in a language (words, phrases, etc) and of language constructs in programming languages (basically any syntactically valid part ...
6
votes
0answers
156 views
Is there relation between K-Framework and structural operational semantics?
K-framework strives to give one (instead of two - operational and denotational) semantics for industrial programming languages. The same unification is done by structural operational semantic as well. ...
5
votes
1answer
803 views
What does ⊢ mean in operational semantics?
I have been reading a couple of texts on operational semantics.
In [1], the evaluation of expressions is done as in this rule:
$\frac{<e_1,s>\;\Rightarrow \;n_1\;\;\;<e_2,s>\;\Rightarrow ...
5
votes
1answer
224 views
Notation for operational semantics that can be used in code comments
I'm defining an intermediate language for a multi-backend code generator that I'm writing. I want to document the operational semantics for this intermediate language in a way that is readable both ...
4
votes
1answer
105 views
What formal representation is commonly used to describe compiler optimizations?
I have devised a compiler optimization that works on any structured language that has arrays assignments array[index] = value and counted loops ...
4
votes
2answers
1k views
Double, down facing arrow in operational semantics
What is the meaning of the double, down facing arrow $\Downarrow$ in the context of operational semantics? Here's the example formula that uses it:
$$\frac{s_0 \vdash M_1 \Downarrow P_1, s_1 \; ... \;...
4
votes
2answers
322 views
How does one deduce small step operational semantics?
This question arises from my reading of "Types and Programming Languages" (WoldCat) by Benjamin C. Pierce.
For the small step operational semantic evaluation rules for the arithmetic expressions (NB) ...
4
votes
2answers
260 views
TAPL: Explanation and example(s) for satisfied
This question arises from my reading of "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce.
On page 36 is the definition for satisfied
A rule is satisfied by a relation if, for ...
4
votes
0answers
365 views
How are observational equivalence, contextual equivalence, and extensional equality related?
First, some context: I'm reading this blog post by Andrej Bauer.
So, I stumbled in these terms: "observational equivalence" and "contextual equivalence".
I know almost nothing about operational ...
3
votes
1answer
70 views
What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics?
Revising for an exam and I'm trying to get to grips with operational semantics. Here's the exam question that prompted me posting this:
Exam Question:
We add to the language $\mathsf{SIMP}$ two new ...
3
votes
0answers
489 views
How to decide between operational, denotational, and axiomatic semantics?
Context
I'm designing a language which implements lambda calculus and (first-order) predicate calculus, where lambdas behave as the abstraction encapsulating logic, compositionally forming a ...
3
votes
0answers
49 views
Termination of deterministic term rewriting
Consider a simple language:
$$t ::= plus ~ t ~ t ~ | ~ gen ~ t ~ | ~ except ~ N ~ t ~ | ~ N$$
with N constructors plus, gen and except, N being the natural numbers, and $G = \{t_n\}$ a finite, ...
2
votes
1answer
75 views
What makes an operational semantics good?
Some papers define an operational semantics of a programming language. That is nice, but what makes such a semantics fit for the purpose?
An idea is to have a progress theorem, i.e. well-formed ...
2
votes
1answer
222 views
Proof via induction for small-step semantics
I'm doing a course in Computer Programming Languages and I'm trying to prove the following (roughly following Pierce's Types and Programming Languages book):
if $t \rightarrow^* t'$ then $if\; t\; ...
2
votes
1answer
862 views
Small-step semantics: for-loops
I'm trying to construct the small-step semantic rules involving the for-loops, but I can't find anything about it in the literature (only about while-loops).
I was wondering if anyone could help me ...
2
votes
1answer
207 views
How does one prove that Big Step semantics and Small Step semantics are equivalent for IMP?
I know there is this paper but I wanted to do a special case proof for just IMP for fun. So the theorem is:
$$ \langle P , \sigma \rangle \to_{Big} \langle \{ \} , \sigma' \rangle \iff \exists N \...
2
votes
1answer
97 views
How to write operational semantics rule for havoc x?
If I want to extend a new language by adding a new command havoc x, which
updates the variable x with a non-deterministic value, how to write operational semantics rule for havoc x?
I'm confused about ...
2
votes
1answer
108 views
defining the operational semantics of a concurrent language
As big-step operational semantics is about evaluating an expression to a final value, can we state that for defining a concurrent language one needs small-step semantics, as concurrent programs need ...
1
vote
2answers
342 views
Rule induction principles in Harper's PFPL
I have a few small questions about section 2.4 ("Rule induction") in Practical Foundations for Programming Languages (p. 19).
(1) In the rule induction principles for ...
1
vote
1answer
60 views
Software code generation from the (operational) semantics - reference request for automatic programming
Are there research trends that try to research code generation directly from the (operational or some other kind of) semantics? One can imagine cognitive architecture that discovers and reasons about ...
1
vote
1answer
300 views
How is a Transition System in Operational Semantics defined?
I'm describing the semantics of a new optimization for Java using Operational Semantics but I'm not sure how to define the transition system.
I found this link :http://www.irisa.fr/celtique/teaching/...
1
vote
1answer
77 views
Substitution-based Operational Semantics of algebraic datatypes
Assume, I want to define the operational semantics for some subset of ML.
...
1
vote
0answers
23 views
structural operational semantic equivalence
We add the following derivation rule to the structural operational semantic:
< repeat S until b, s >$\Rightarrow$ < S; if b then skip else (repeat S until b) >
Prove that "repeat S until b" is ...
1
vote
0answers
96 views
Small step vs big step semantics for static analysis?
To be an honest question poster I do not yet fully grasp the difference between small step and big step semantics. There was a good discussion here
My question is if I were to do static analysis on ...
1
vote
0answers
61 views
Operational Semantics - Include SKIP, SEQUENCE and IF?
I'm writing a paper for a programming languages workshop in which I have to describe the semantics of a new optimization for Java using Operational Semantics, small step style.
I have never used ...
1
vote
0answers
128 views
Program equivalence with Structural induction
I recently attended my first lecture on structural induction and the professor stated that structural induction can be used to to prove that two programming languages are equivalent.
I am new to ...
0
votes
1answer
77 views
What are the benefits of languages that are not Turing complete?
Unfortunately I did a degree in CS without much theoretical computer science. One thing I used to hear is that sub languages, or languages which are not Turing complete, allow for better optimization?
...
0
votes
1answer
27 views
Examples of interesting semantics to study during a small project for a graduate Semantics course
I have been following the course Concrete Semantics with Isabelle/HOL. At some point we are given the task to verify a program/extend some semantic construction/prove some mathematical fact. I ...
0
votes
0answers
36 views
What is the semantics of a Turing machine?
Can we formalize the operational/denotational semantics of a Turing Machine? Is there any formalization in literature?
0
votes
0answers
21 views
Proof of Small-Step Semantics property
I'm trying to solve the exercise 2.20 from the book "Semantics with Applications" by Nielson & Nielson. The request is the following:
Exercise 2.20 Suppose that (S1;S2,s) =>* (S2,s'). Show that ...
0
votes
0answers
28 views
What is the difference between programming and planning? Is programming the special case of planning?
Computer programming is laying out the predefined operations (actions) in compositional/recursive/recurrent manner to go from one defined state (e.g. assignment of variables) to the other defined ...
0
votes
0answers
61 views
Why algebraic semantics of programming languages have died out and have not used today?
Algebraic semantics is one type of semantics that uses algebraic expressions for connecting the formal descriptions of initial and final states of some operation of some operation that is defined in ...
0
votes
0answers
97 views
Reasonable definition of beta-equivalence in big-step semantics
Assume, an extension of the lambda calculus with terms $t$ and values $v$ is defined in big-step operational semantics with evaluation relation $t \Downarrow v$.
It is intuitive to assume that $\beta$...
0
votes
0answers
41 views
How to check if two program are simulated or bisimulated?
Suppose I have programs A and B defined in this way:
...
0
votes
0answers
166 views
Proving the small-step semantics of factorial program
I am given the following command $C$:
$y:=1;$
while $\neg (x=1)$ do
$y:= y*x;$
$x:= x - 1$.
I have to show that $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto s(x)!\}$ if $s(x) \geq 1$ and undefined ...
0
votes
1answer
54 views
How to prove the following properties of Small-step semantics?
I have to prove the following 2 properties of the Small-step semantics of the WHILE programming language:
If $\langle C_1; C_2, s\rangle \rightarrow^k s'$ then there is a
state $s''$ and natural ...
