Table of Contents for Programming Languages: a survey

Chapter : Semantics



What else?

Effect analysis

The clearest intro i've seen:

Abstract interpretation

(If you are familiar with the mathematical idea of homomorphism, this is just an application of that)

If you are going to multiply two integers,

c = a * b

then you known that if sign(a) = +, sign(b) = +, then sign(c) = +, and similarly

sign(a) = + and sign(b) = - --> sign(c) = - sign(a) = - and sign(b) = + --> sign(c) = - sign(a) = - and sign(b) = - --> sign(c) = +

so, you could imagine an operator, call it multiply_sign in the domain {-,+} with this behavior. So you map the domain of integers to the domain of {-,+}, and map the multiplication operator * to multiply_sign. This allows you to know something about c without calculating it directly (in particular, if you know the sign of a and of b, you can know the sign of c).


Todo: big step, small step, etc Semantics of programming languages



Unifying Theories of Programming (UTP) by Hoare and He.


Operational semantics: Structural operational semantics: big step semantics vs. small step semantics

In small-step semantics, we write inference rules for individual reduction steps.

For example, if <e, state> denotes expression 'e' in context 'context', one rule might be (given in sequent notation):

   <e1, s> -> <e1', s>

<e1 + e2, s> -> <e1' + e2, s>

and another might be

   <e1, s> -> <e1', s>

<e2 + e1, s> -> <e2 + e1', s>

In big-step semantics, each 'big step' is just the result of combining many small-step transitions into one step.

For example, we might say:

   <e1, s> => <e1', s>   <e2, s> => <e2', s>

         <e1 + e2, s> => <e1' + e2', s>

where => denotes a 'big arrow' (usually denoted by a big downward-facing arrow) and "a => b" means "after applying one or more small-steps, a can be reduced to b, and cannot be further reduced" (todo: check: is that actually what it formally means?).

For terminating reduction chains, the big-step and small-step semantics of a language should agree (and people try to prove this, for specific semantics for specific languages).

"big-step semantics cannot talk directly about nontermination" If <e, s> does not terminate, then there is no <e2, s2> such that <e,s> => <e2, s2> [1]

" Comparison of big-step vs. small-step SOS

5.1 Small-step

5.2 Big-step