Table of Contents for Programming Languages: a survey
The clearest intro i've seen: http://wingolog.org/archives/2014/05/18/effects-analysis-in-guile
(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
Links:
---
Unifying Theories of Programming (UTP) by Hoare and He. https://en.wikipedia.org/wiki/Unifying_Theories_of_Programming
---
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
Links: