Skip to main content

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.

Filter by
Sorted by
Tagged with
2 votes
1 answer
67 views

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

Mitchell specifies a set data type: ie, an algebraic specification for set. He then asks to prove that the equation union s s' = union s' s [s, s': set] does not hold in the initial algebra. He ...
emesupap's user avatar
  • 183
0 votes
0 answers
22 views

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

I am trying to solve this proof. In structural semantics I need to proof that: ...
Francisco Aguilera's user avatar
0 votes
1 answer
74 views

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

I am studying Structural Semantics for programming languages and I have come to this proof that I can not achieve. Whith these rules plus Splitting and No interference, I am trying to get a proof. I ...
Francisco Aguilera's user avatar
0 votes
0 answers
82 views

Semantics Equivalence of Structural Semantics of While Programming Language

I'm taking a course about the formality of programming languages and while reading Semantics with Applications: An Appetizer by H.R Nielson and F. Nielson I came across the following exercise: I'm ...
MiddleEasternPrince's user avatar
2 votes
1 answer
729 views

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

I saw the word "redex" in the context of proramming language theory/semantics in 2018 and now when I was reading a neurosymbolic research paper (machine learning with neural nets + symbolic ...
Charlie Parker's user avatar
2 votes
1 answer
122 views

From big-step to small-step semantics

Ciobaca: From Small-Step Semantics to Big-Step Semantics, Automatically describes how to go from small-step to big-step semantics. I need to do the other way around: from big-step to small-step. Is ...
Gergely's user avatar
  • 379
1 vote
0 answers
156 views

CEK machine vs SECD machine

What are the differences between the CEK machine and the modern variant of the SECD machine (which combines stack and dump) from the point of view of performance, memory efficiency, and other factors? ...
user76284's user avatar
  • 416
1 vote
0 answers
27 views

Why structural rules define the "smallest relation" satisfying the rules?

I'm following a university course based on these slides, and I have a question about structural operational semantics. As you can see at page 7 (4-th slide), a structural rule is interpreted logically ...
user402843's user avatar
0 votes
1 answer
348 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?
Linpeng Zhang's user avatar
0 votes
0 answers
139 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 ...
TomR's user avatar
  • 1,401
1 vote
1 answer
402 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? ...
Zeruno's user avatar
  • 111
1 vote
0 answers
45 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 ...
user's user avatar
  • 11
1 vote
0 answers
218 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 ...
John Smith's user avatar
10 votes
1 answer
9k 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 ...
George's user avatar
  • 203
2 votes
1 answer
868 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 \...
Charlie Parker's user avatar
0 votes
1 answer
55 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 ...
user1868607's user avatar
  • 2,194
1 vote
1 answer
84 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 ...
TomR's user avatar
  • 1,401
7 votes
2 answers
212 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 ...
Ben Kushigian's user avatar
3 votes
0 answers
752 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 ...
Phizo's user avatar
  • 51
4 votes
1 answer
130 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 ...
El Marce's user avatar
  • 333
14 votes
3 answers
599 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 ...
Guido's user avatar
  • 398
6 votes
0 answers
497 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 ...
Rafael Castro's user avatar
1 vote
1 answer
438 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/...
El Marce's user avatar
  • 333
1 vote
0 answers
86 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 ...
El Marce's user avatar
  • 333
9 votes
3 answers
1k 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 \> ...
El Marce's user avatar
  • 333
3 votes
0 answers
53 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, ...
choeger's user avatar
  • 610
0 votes
0 answers
127 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$...
choeger's user avatar
  • 610
6 votes
1 answer
65 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 ...
gardenhead's user avatar
  • 2,230
6 votes
0 answers
174 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. ...
TomR's user avatar
  • 1,401
17 votes
2 answers
708 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 ...
gardenhead's user avatar
  • 2,230
19 votes
2 answers
5k 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 ...
natevw's user avatar
  • 293
1 vote
0 answers
148 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 ...
anil keshav's user avatar
2 votes
1 answer
99 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 ...
Gergely's user avatar
  • 379
3 votes
1 answer
88 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 ...
notywq's user avatar
  • 31
2 votes
1 answer
273 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 ...
user2435797's user avatar
5 votes
1 answer
1k 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 ...
josh's user avatar
  • 341
42 votes
2 answers
14k 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.
Simon Morgan's user avatar
0 votes
0 answers
44 views

How to check if two program are simulated or bisimulated?

Suppose I have programs A and B defined in this way: ...
Oper's user avatar
  • 109
3 votes
1 answer
292 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\; ...
racketball's user avatar
1 vote
1 answer
108 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
choeger's user avatar
  • 610
0 votes
0 answers
239 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 ...
trojan's user avatar
  • 3
2 votes
1 answer
1k 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 ...
ABC's user avatar
  • 123
0 votes
1 answer
66 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 ...
trojan's user avatar
  • 3
2 votes
2 answers
445 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 ...
Fixnum's user avatar
  • 71
2 votes
1 answer
145 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 ...
Gergely's user avatar
  • 379
4 votes
2 answers
2k 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 \; ... \;...
wvxvw's user avatar
  • 1,388
7 votes
2 answers
432 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 ...
Guy Coder's user avatar
  • 5,121
4 votes
2 answers
472 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) ...
Guy Coder's user avatar
  • 5,121
5 votes
1 answer
246 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 ...
Mike Samuel's user avatar
  • 1,204
7 votes
1 answer
289 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) ...
galaxybeing's user avatar