Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [operational-semantics]

The tag has no usage guidance.

-1
votes
0answers
16 views

Operator Precedence Parsing

In operator precedence parsing we have the rule that no production is allowed to have two adjacent non-terminals or an epsilon production. Hence, the production $S \to ab$ is allowed but not $S \to AB$...
0
votes
0answers
12 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
40 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 ...
4
votes
1answer
260 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 ...
2
votes
1answer
74 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 \...
0
votes
1answer
18 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 ...
1
vote
1answer
53 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 ...
7
votes
2answers
148 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 ...
3
votes
0answers
419 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 ...
4
votes
1answer
94 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 ...
11
votes
3answers
327 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 ...
4
votes
0answers
271 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 ...
1
vote
1answer
168 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
0answers
57 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 ...
9
votes
3answers
885 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 \> ...
3
votes
0answers
45 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, ...
0
votes
0answers
78 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$...
6
votes
1answer
46 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
142 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. ...
14
votes
2answers
336 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 ...
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 ...
1
vote
0answers
120 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 ...
2
votes
1answer
69 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 ...
3
votes
1answer
61 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 ...
2
votes
1answer
78 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 ...
5
votes
1answer
714 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 ...
25
votes
1answer
6k 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.
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: ...
2
votes
1answer
189 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\; ...
1
vote
1answer
73 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
0
votes
0answers
142 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 ...
2
votes
1answer
684 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 ...
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 ...
1
vote
2answers
309 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 ...
2
votes
1answer
96 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 ...
4
votes
2answers
944 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
216 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
2answers
280 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) ...
5
votes
1answer
211 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 ...
7
votes
1answer
263 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) ...