World's most popular travel blog for travel bloggers.

# How is a Transition System in Operational Semantics defined?

, ,
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 :http://www.irisa.fr/celtique/teaching/PAS/opsem-2016.pdf where in slide 20 the transition system is defined but I don't get it.

###### Asked By : El Marce

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).