World's most popular travel blog for travel bloggers.

How is a Transition System in Operational Semantics defined?

, , No Comments
Problem Detail: 

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 : where in slide 20 the transition system is defined but I don't get it.

Asked By : El Marce
Answered By : gardenhead

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 between two entities of our language. For example, in programming, we often employ the judgement $e: \tau$, asserting that expression $e$ has type $\tau$.

Inference rules are used to define judgements. They have the general form

$$ \frac{J_1 \dots J_n}{J} $$

which reads: if we know judgements $J_1$ through $J_n$, we can infer judgement $J$. For example, we may have the following self-explanatory inference rule for the previously defined typing judgement:

$$ \frac{n: \text{int} \quad m: \text{int}}{n+m: \text{int}}. $$

A structural operational semantics is defined using a transition system between states. In a programing language, the states are all closed expression in the language, and the final states are values. Formally, we make use of two judgements:

  1. $e_1 \to e_2$, stating that expression $e_1$ transitions to state $e_2$ in one step
  2. $e \space \text{final}$, stating that expression $e$ is a final state of the system.

Here are some example inference rules in a language with arithmetic and function abstraction:

$$ \frac{}{n \text{ final}} $$ $$ \frac{}{n+0 \to n} $$ $$ \frac{n + m \to k}{s(n) + m \to s(k)} $$ $$ \frac{}{\lambda x. e \ \text{final}} $$ $$ \frac{(\lambda x. e_1)e_2}{[e_2/x]e_1} $$

Most languages do not have a formal definition, including Java (as far as I know). There are also other methods for defining the semantics of a language, but for describing an optimization, I believe structural dynamics is a wise choice, as it has a natural notion of time complexity (the number of transitions).

Best Answer from StackOverflow

Question Source :

3200 people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback