2011/03/28

Big-step semantics

Operational semantics

In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operatational semantics (or small-step semantics) formally describe how the individual steps of a computation take place in a computer-based system. By opposition natural semantics (or big-step semantics) describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.

The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps. These sequences then are the meaning of the program. In the context of functional programs, the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could be nondeterministic, and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.)

For the first time, the concept of operational semantics was used in defining the semantics of Algol 68. The following statement is a quote from the revised ALGOL 68 report:

The first use of the term "operational semantics" in its present meaning is attributed to Dana Scott (Plotkin04). What follows is a quote from Scott's seminal paper on formal semantics, in which he mentions the "operational" aspects of semantics.

Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of LISP by [John McCarthy. "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I". http://www-formal.stanford.edu/jmc/recursive.html. Retrieved 2006-10-13.]. Abstract machines in the tradition of the SECD machine are also closely related.

Approaches

Gordon Plotkin introduced the structural operational semantics, Gilles Kahn the natural semantics.

Structural operational semantics

Structural operational semantics (also called structured operational semantics or small-step semantics) was introduced by Gordon Plotkin in (Plotkin81) as a logical means to defining operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax oriented and inductive, view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) transition relation(s). SOS specifications take the form of a set of inference rules which define the valid transitions of a composite piece of syntax in terms of the transitions of its components.

For a simple example, we consider part of the semantics of a simple programming language; proper illustrations are given in Plotkin81 and Hennessy90, and other textbooks. Let C1,C2 range over programs of the language, and let s range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by E), values (V) and locations (L), then a memory update command would have semantics:

\frac{\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle\longrightarrow (s\uplus (L\mapsto V))}

Informally, the rule says that "if the expression E in state s reduces to value V, then the program L: = E will update the state s with the assignment L = V".

The semantics of sequencing can be given by the following three rules:

\frac{\langle C_1,s\rangle \longrightarrow s'} {\langle C_1;C_2 \,,s\rangle\longrightarrow \langle C_2, s'\rangle} \quad\quad \frac{\langle C_1,s\rangle \longrightarrow \langle C_1',s'\rangle} {\langle C_1;C_2 \,,s\rangle\longrightarrow \langle C_1';C_2\,, s'\rangle} \quad\quad \frac{} {\langle \mathbf{skip} ,s\rangle\longrightarrow s}

Informally, the first rule says that, if program C1 in state s finishes in state s', then the program C1;C2 in state s will reduce to the program C2 in state s'. (You can think of this as formalizing "You can run C1, and then run C2 using the resulting memory store.) The second rule says that if the program C1 in state s can reduce to the program C1' with state s', then the program C1;C2 in state s will reduce to the program C1';C2 in state s'. (You can think of this as formalizing the principle for an optimizing compiler: "You are allowed to transform C1 as if it were stand-alone, even if it is just the first part of a program.") The semantics is structural, because the meaning of the sequential program C1;C2, is defined by the meaning of C1 and the meaning of C2.

If we also have Boolean expressions over the state, ranged over by B, then we can define the semantics of the while command: \frac{\langle B,s\rangle \Rightarrow \mathbf{true}}{\langle\mathbf{while}\ B\ \mathbf{ do }\ C,s\rangle\longrightarrow \langle C;\mathbf{while}\ B\ \mathbf{do}\ C,s\rangle} \quad \frac{\langle B,s\rangle \Rightarrow \mathbf{false}}{\langle\mathbf{while}\ B\ \mathbf{ do }\ C,s\rangle\longrightarrow s}

Such a definition allows formal analysis of the behavior of programs, permitting the study of relations between programs. Important relations include simulation preorders and bisimulation. These are especially useful in the context of concurrency theory.

Thanks to its intuitive look and easy to follow structure, SOS has gained great popularity and has become a de facto standard in defining operational semantics. As a sign of success, the original report (so-called Aarhus report) on SOS (Plotkin81) has attracted more than 1000 citations according to the CiteSeer [1], making it one of the most cited technical reports in Computer Science.

Natural semantics

Natural semantics (or big-step semantics) ...

See also

References






Retrieved from : http://en.wikipedia.org/wiki/Operational_semantics#Natural_semantics
Posted by at

No comments:

Post a Comment

Subscribe to: Post Comments (Atom)