Understanding Computation by Tom Stuart Page A

our small-step semantics is
     explicit about the order in which operations are supposed to happen, because at every point,
     it identifies what the next step of reduction should be, but big-step semantics is often
     written in a looser style that just says which subcomputations to perform without
     necessarily specifying what order to perform them in. [ 14 ] Small-step semantics also gives us an easy way to observe the intermediate
     stages of a computation, whereas big-step semantics just returns a result and doesn’t
     produce any direct evidence of how it was computed.
    To understand this trade-off, let’s revisit some common language constructs and see how
     to implement their big-step semantics in Ruby. Our small-step semantics required a
Machine
class to keep track of state and perform repeated
     reductions, but we won’t need that here; big-step rules describe how to compute the result
     of an entire program by walking over its abstract syntax tree in a single attempt, so
     there’s no state or repetition to deal with. We’ll just define an
#evaluate
method on our expression and statement classes and call it
     directly.
    Expressions
    With small-stepsemantics we had to distinguish reducible expressions
     like «
1 + 2
» from irreducible
     expressions like «
3
» so that the
     reduction rules could tell when a subexpression was ready to be used
     as part of some larger computation, but in big-step semantics every
     expression can be evaluated. The only distinction, if we wanted to
     make one, is that some expressions immediately evaluate to themselves,
     while others perform some computation and evaluate to a different
     expression.
    The goal of big-step semantics is to model the same runtime behavior as the small-step
     semantics, which means we expect the big-step rules for each kind of program construct to
     agree with what repeated application of the small-step rules would eventually produce.
     (This is exactly the sort of thing that can be formally proved when an operational
     semantics is written mathematically.) The small-step rules for values like
Number
and
Boolean
say that
     we can’t reduce them at all, so their big-step rules are very simple: values immediately
     evaluate to themselves.
class
Number
def
evaluate
(
environment
)
self
end
end
class
Boolean
def
evaluate
(
environment
)
self
end
end
    Variable
expressions are
     unique in that their small-step semantics allow them to be reduced
     exactly once before they turn into a value, so their big-step rule is
     the same as their small-step one: look up the variable name in the
     environment and return its value.
class
Variable
def
evaluate
(
environment
)
environment
[
name
]
end
end
    The binary expressions
Add
,
Multiply
, and
LessThan
are slightly more interesting,
     requiring recursive evaluation of their left and right subexpressions
     before combining both values with the appropriate Ruby
     operator:
class
Add
def
evaluate
(
environment
)
Number
.
new
(
left
.
evaluate
(
environment
)
.
value
+
right
.
evaluate
(
environment
)
.
value
)
end
end
class
Multiply
def
evaluate
(
environment
)
Number
.
new
(
left
.
evaluate
(
environment
)
.
value
*
right
.
evaluate
(
environment
)
.
value
)
end
end
class
LessThan
def
evaluate
(
environment
)
Boolean
.
new
(
left
.
evaluate
(
environment
)
.
value
<
right
.
evaluate
(
environment
)
.
value
)
end
end
    To check that these big-step expression semantics are correct,
     here they are in action on the Rubyconsole:
>>
Number
.
new
(
23
)
.
evaluate
({})
=> «23»
>>
Variable
.
new
(
:x
)
.
evaluate
({
x
:
Number
.
new
(
23
)
})
=> «23»
>>
LessThan
.
new
(
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
2
)),
Variable
.
new
(
:y
)
)
.
evaluate
({
x
:
Number
.
new
(
2
),
y
:
Number
.
new
(
5
)
})
=> «true»
    Statements
    This style ofsemantics shines when we come to specify the behavior of
     statements. Expressions reduce to other expressions under small-step
     semantics, but statements reduce to