Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.

Questions tagged [operational-semantics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
27
votes
1answer
7k 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
2k 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
375 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
355 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
896 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
154 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
265 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
0answers
153 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
746 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
216 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
98 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
292 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
1answer
745 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 ...
4
votes
2answers
231 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
309 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
67 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
443 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
47 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
70 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
203 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
742 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
118 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
90 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
102 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
324 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
56 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
244 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
76 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
1
vote
0answers
67 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
59 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
124 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
42 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
24 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
21 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
47 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
17 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 ...
0
votes
0answers
86 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
40 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
143 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
50 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 ...