Cheap and Secure Web Hosting Provider : See Now

[Solved]: How does one deduce small step operational semantics?

, , No Comments
Problem Detail: 

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) in Figure 3-2 on page 41, there is the rule

$pred\;(succ\;nv_1)\rightarrow\;nv_1$

My understanding is that it is to keep out invalid input like

$pred\;(false)$

but how did he come to that exact syntax for the rule? Is there some algorithm that is used to massage the rules into the necessary form? Is there some book or paper that explains how to formulate rules for small step operational semantics?

Note: I am aware that there is a forum dedicated to questions for the book here.

Asked By : Guy Coder

Answered By : Andrej Bauer

Devising an operational semantics of a programming language requires ingenuity, just like engineering a new car does. Nevertheless, there are some principle and correctness criteria by which we can judge whether a given semantics is "good".

For example, a good operational semantics should make sure that "valid programs do not do bad things". In practice this translates to "if a program succesfully compiled it is not going to dump core when we run it". Some languages are unsafe in this respect (C/C++), some are designed with safety in mind (Java, Python), and some are proved to be safe (Standard ML).

One way of translating "valid programs do not do bad things" is to interpret "valid program" as "well typed program" and "bad thing" as "getting stuck during evalution, even though we have not reached a final value". For this to make sense you have to define what "well typed" and "value" means. The central theorem then is

Safety: If a program $p$ has type $\tau$ then its evaluation diverges or terminates in a value of type $\tau$.

The theorem is typically proved by combining two lemmas:

Type preservation: If $p$ has type $\tau$ and $p \mapsto p'$ then $p'$ has type $\tau$. Remember this as "types do not change during evaluation".

Progress: If $p$ has type $\tau$ then it is either a value or there is a program $p'$ such that $p \mapsto p'$.

On the other hand, it does not matter what the operational semantics does with senseless programs, such as $\mathtt{pred}(\mathtt{false})$ because those do not have a type. It is the combination of typing and operational semantics that ensures safety. You cannot ensure safety just with the operational semantics, unless you are willing to make bizarre evaluation rules that will make your language awfully hard to debug.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/10347

3.2K people like this

 Download Related Notes/Documents

0 comments:

Post a Comment

Let us know your responses and feedback