1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Please make your question self-contained. What exactly seems to be a problem? In current form the answer is simply doomed, it will either describe things that you understand and someones time will be wasted, or the part that is crucial to you will not get enough details and it will still be problematic. Have you tried different resources? $\endgroup$ – Evil Nov 13 '16 at 4:10
2
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.