Understanding Computation (7 page)

Writing the correct reduction rules for a «
while
»
statement is slightly tricky. We could try treating it like an «
if
» statement: reduce the condition if possible; otherwise, reduce to either
the body or «
do-nothing
», depending on whether the
condition is «
true
» or «
false
», respectively. But once the abstract machine has completely reduced
the body, what next? The condition has been reduced to a value and thrown away, and the
body has been reduced to «
do-nothing
», so how do we
perform another iteration of the loop? Each reduction step can only communicate with
future steps by producing a new statement and environment, and this approach doesn’t give
us anywhere to “remember” the original condition and body for use on the next
iteration.

The small-step solution
^[
11
]
is to use the sequence statement to
unroll
one level of the «
while
», reducing it to an «
if
» that performs a single iteration of the
loop and then repeats the original «
while
». This means we only need one
reduction rule:

And this rule is easy to implement in Ruby:

class
While
<
Struct
.
new
(
:condition
,
:body
)
def
to_s
"while (
#{
condition
}
) {
#{
body
}
}"
end
def
inspect
"«
#{
self
}
»"
end
def
reducible?
true
end
def
reduce
(
environment
)
[
If
.
new
(
condition
,
Sequence
.
new
(
body
,
self
),
DoNothing
.
new
),
environment
]
end
end

This gives the virtual machine the opportunity to evaluate the
condition and body as many times as necessary:

>>
Machine
.
new
(
While
.
new
(
LessThan
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
5
)),
Assign
.
new
(
:x
,
Multiply
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
3
)))
),
{
x
:
Number
.
new
(
1
)
}
)
.
run
while (x < 5) { x = x * 3 }, {:x=>«1»}
if (x < 5) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«1»}
if (1 < 5) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«1»}
if (true) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«1»}
x = x * 3; while (x < 5) { x = x * 3 }, {:x=>«1»}
x = 1 * 3; while (x < 5) { x = x * 3 }, {:x=>«1»}
x = 3; while (x < 5) { x = x * 3 }, {:x=>«1»}
do-nothing; while (x < 5) { x = x * 3 }, {:x=>«3»}
while (x < 5) { x = x * 3 }, {:x=>«3»}
if (x < 5) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«3»}
if (3 < 5) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«3»}
if (true) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«3»}
x = x * 3; while (x < 5) { x = x * 3 }, {:x=>«3»}
x = 3 * 3; while (x < 5) { x = x * 3 }, {:x=>«3»}
x = 9; while (x < 5) { x = x * 3 }, {:x=>«3»}
do-nothing; while (x < 5) { x = x * 3 }, {:x=>«9»}
while (x < 5) { x = x * 3 }, {:x=>«9»}
if (x < 5) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«9»}
if (9 < 5) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«9»}
if (false) { x = x * 3; while (x < 5) { x = x * 3 } } else { do-nothing }, {:x=>«9»}
do-nothing, {:x=>«9»}
=> nil

Perhaps this reduction rule seems like a bit of a dodge—it’s almost as though we’re
perpetually postponing reduction of the «
while
» until
later, without ever actually getting there—but on the other hand, it does a good job of
explaining what we really mean by a «
while
» statement:
check the condition, evaluate the body, then start again. It’s curious that reducing
«
while
» turns it into a syntactically larger program
involving conditional and sequence statements instead of directly reducing its condition
or body, and one reason why it’s useful to have a technical framework for specifying the
formal semantics of a language is to help us see how different parts of the language
relate to each other like this.

We’ve completely
ignored what will happen when a syntactically valid but
otherwise incorrect program is executed according to the semantics
we’ve given. The statement «
x = true; x = x +
1
» is a valid piece of
Simple
syntax—we can certainly construct an
abstract syntax tree to represent it—but it’ll blow up when we try to
repeatedly reduce it, because the abstract machine will end up trying
to add «
1
» to «
true
»:

>>
Machine
.
new
(
Sequence
.
new
(
Assign
.
new
(
:x
,
Boolean
.
new
(
true
)),
Assign
.
new
(
:x
,
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
1
)))
),
{}
)
.
run
x = true; x = x + 1, {}
do-nothing; x = x + 1, {:x=>«true»}
x = x + 1, {:x=>«true»}
x = true + 1, {:x=>«true»}
NoMethodError: undefined method `+' for true:TrueClass

One way to handle this is to be more restrictive about when expressions can be
reduced, which introduces the possibility that evaluation will get
stuck
rather than always trying to reduce to a value (and
potentially blowing up in the process). We could have implemented
Add#reducible?
to only return
true
when
both arguments to «
+
» are either reducible or an
instance of
Number
, in which case the expression
«
true + 1
» would get stuck and never turn into a
value.

Ultimately, we need a more powerful tool than syntax, something that can “see the
future” and prevent us from trying to execute any program that has the potential to blow
up or get stuck. This chapter is
about
dynamic semantics
—what a program does when it’s
executed—but that’s not the only kind of meaning that a program can have; in
Chapter 9
, we’ll investigate
static semantics
to see how we can decide whether a syntactically
valid program has a useful meaning according to the language’s dynamic semantics.

The programming
language
we’ve specified is very basic, but in writing down all the reduction rules,
we’ve still had to make some design decisions and express them unambiguously. For example,
unlike Ruby,
Simple
is a language that makes a
distinction between expressions, which return a value, and statements, which don’t; like
Ruby,
Simple
evaluates expressions in a left-to-right
order; and like Ruby,
Simple
’s environments associate
variables only with fully reduced
values, not with larger expressions that still have some unfinished
computation to perform.
^[
12
]
We could change any of these decisions by giving a different small-step
semantics which would describe a new language with the same syntax but different runtime
behavior. If we added more elaborate features to the language—data structures, procedure
calls, exceptions, an object system—we’d need to make many more design decisions and
express them unambiguously in the semantic definition.

The detailed, execution-oriented style of small-step semantics lends itself well to
the task of unambiguously specifying real-world programming languages. For example, the
latest R6RS standard for the
Scheme programming language uses
small-step semantics
to describe its execution, and provides a
reference implementation of those semantics
written
in
PLT Redex
, “a
domain-specific language designed for specifying and debugging operational semantics.” The
OCaml programming language, which
is built as a series of layers on top of a simpler language called Core ML,
also has a
small-step semantic definition
of the base language’s runtime behavior.

See
Semantics
for another example of using
small-step operational semantics to specify the meaning of expressions in an even simpler
programming language called the lambda
calculus.

With small-step
semantics 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 Ruby
console:

>>
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»

This style of
semantics shines when we come to specify the behavior of
statements. Expressions reduce to other expressions under small-step
semantics, but statements reduce to «
do-nothing
» and leave a modified environment
behind. We can think of big-step statement evaluation as a process
that always turns a statement and an initial environment into a final
environment, avoiding the small-step complication of also having to
deal with the intermediate statement generated by
#reduce
. Big-step evaluation of an
assignment statement, for example, should fully evaluate its
expression and return an updated environment containing the resulting
value:

class
Assign
def
evaluate
(
environment
)
environment
.
merge
({
name
=>
expression
.
evaluate
(
environment
)
})
end
end

Similarly,
DoNothing#evaluate
will clearly return the unmodified environment, and
If#evaluate
has a pretty straightforward job
on its hands: evaluate the condition, then return the environment that
results from evaluating either the consequence or the
alternative.

class
DoNothing
def
evaluate
(
environment
)
environment
end
end
class
If
def
evaluate
(
environment
)
case
condition
.
evaluate
(
environment
)
when
Boolean
.
new
(
true
)
consequence
.
evaluate
(
environment
)
when
Boolean
.
new
(
false
)
alternative
.
evaluate
(
environment
)
end
end
end

The two interesting cases are
sequence statements and «
while
» loops. For
sequences, we just need to evaluate both statements, but the initial environment needs to
be “threaded through” these two evaluations, so that the result of evaluating the first
statement becomes the environment in which the second statement is evaluated. This can be
written in Ruby by using the first evaluation’s result as the argument to the
second:

class
Sequence
def
evaluate
(
environment
)
second
.
evaluate
(
first
.
evaluate
(
environment
))
end
end

This threading of the environment is vital to allow earlier
statements to prepare variables for later ones:

>>
statement
=
Sequence
.
new
(
Assign
.
new
(
:x
,
Add
.
new
(
Number
.
new
(
1
),
Number
.
new
(
1
))),
Assign
.
new
(
:y
,
Add
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
3
)))
)
=> «x = 1 + 1; y = x + 3»
>>
statement
.
evaluate
({})
=> {:x=>«2», :y=>«5»}

For «
while
» statements, we need to think through
the stages of completely evaluating a loop:

This is a recursive explanation of how a «
while
»
statement should behave. As with sequence statements, it’s important that the updated
environment generated by the loop body is used for the next iteration; otherwise, the
condition will never stop being «
true
», and the loop
will never get a chance to terminate.
^[
15
]

Once we know how big-step «
while
» semantics should behave, we can
implement
While#evaluate
:

class
While
def
evaluate
(
environment
)
case
condition
.
evaluate
(
environment
)
when
Boolean
.
new
(
true
)
evaluate
(
body
.
evaluate
(
environment
))
when
Boolean
.
new
(
false
)
environment
end
end
end

RubyVM
::
InstructionSequence
.
compile_option
=
{
tailcall_optimization
:
true
,
trace_instruction
:
false
}

To confirm that this works properly, we can try evaluating the
same «
while
» statement we used to
check the small-step semantics:

>>
statement
=
While
.
new
(
LessThan
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
5
)),
Assign
.
new
(
:x
,
Multiply
.
new
(
Variable
.
new
(
:x
),
Number
.
new
(
3
)))
)
=> «while (x < 5) { x = x * 3 }»
>>
statement
.
evaluate
({
x
:
Number
.
new
(
1
)
})
=> {:x=>«9»}

This is the same result that the small-step semantics gave, so
it looks like
While#evaluate
does
the right
thing.