Module 11: Small-step reduction
This module is due at 1:15pm on Tuesday, October 18.
Write your team names here:
Pick an initial driver and write their name here:
Begin by pasting in your most recent implementation of the Arith language.
I promise that after fall break we will be done with Arith. ;-)
Bound variables
Consider the expression let x = e1 in e2
. We say that this expression binds the variable x
, that is, it introduces a local definition for x
. We say that x
is bound in e2
, that is, any occurrences of x
in e2
refer to the x
defined by the let
. (However, x
is not bound in e1
—we will think more about this later.)
For example, in
let x = 2+3 in x + if x < 10 then 3 else 7
both occurrences of x
after the in
refer to the x
defined by the let
, so this expression evaluates to 8.
Actually, it is not quite true that any occurrence of x
in e2
refers to the x
defined by the let
. We have to take shadowing into account. For example, consider this expression:
let x = 5 in let x = 6 in x + x
What does this evaluate to, 10 or 12?
Why?
What does this expression evaluate to (be sure to guess before trying it)?
let x = 2+3 in let x = 2*x in 4+x
(Hint: remember that in
let x = e1 in e2
,x
is bound ine2
but not ine1
.)What would it mean if
let x = e1 in e2
boundx
in bothe1
ande2
?Do you think this could be a useful feature for the Arith language?
Try evaluating
let x = 2+3 in let x = 2*x in 4+x
as a Haskell expression (that is, just type it at a GHCi prompt). What do you think this means aboutlet
in Haskell?
![](../images/stop.gif)
Free variables and substitution
- ROTATE ROLES and write the name of the new driver here:
A variable is free if it is not bound. For example, in the expression
let x = 2 in x + y
The x
is bound, but y
is free.
Write a function
fv :: Arith -> S.Set String
which computes the set of free variables of anArith
expression. You should addimport qualified Data.Set as S
at the top of the module; see the documentation for
Data.Set
here.We won’t actually need the
fv
function, but it is a good warm-up exercise for thinking about bound and free variables.Now write a substitution function,
subst :: String -> Arith -> Arith -> Arith
subst x e1 e2
should result ine2
, but with every free occurrence ofx
replaced bye1
. For example,subst x 3 "x + let x = x+1 in x*6" = "3 + let x = 3+1 in x*6"
In the above example every free occurrence of
x
is replaced by3
, but the bound occurrences ofx
are left alone. (The above is not actually valid syntax; I am using strings as a shorthand for their parsedArith
equivalents. To help testsubst
and other functions later, it may be helpful to write a functionp :: String -> Arith
which tries to parse the givenString
and simply crashes witherror
if it does not. Then you can actually write things likesubst "x" (p "3") (p "x + let x ...")
.)
![](../images/green.png)
Small-step reduction
- ROTATE ROLES and write the name of the new driver here:
When we have written interpreters before, they have used what is called a big-step semantics: for example, they take an Arith
and simply reduce it to a value in one “big step”. There is no way to extract any sort of intermediate expressions or states from the interpreter: running the interpreter is an all-or-nothing sort of operation.
We will now consider an alternative model, where we define what it means for an expression to take a (small) reduction step, resulting in another expression. A reduction step changes as little as possible while still making nontrivial progress. We can then write an interpreter by repeatedly applying reduction steps until the expression cannot take any more steps. For example, consider the expression if 3 + 5 < 7 then 2*5 else (let x = 3 in x+x)
. The interpArith
function would simply take this expression and return 6
(by making recursive calls to interpArith
to evaluate the subexpressions, and so on). On the other hand, if we evaluate the expression by repeatedly applying small reduction steps, it would reduce as follows:
if 3 + 5 < 7 then 2*5 else (let x = 3 in x+x)
if 8 < 7 then 2*5 else (let x = 3 in x+x)
if False then 2*5 else (let x = 3 in x+x)
let x = 3 in x+x
3+3
6
Writing an interpreter in this style is usually inefficient compared to a direct (big-step) implementation, but it can be a very useful way to think and reason about the semantics of a language. It is often useful to define both small-step and big-step semantics for a language, along with a formal proof that the two give equivalent results.
![](../images/stop.gif)
Write a function
step :: Arith -> Maybe Arith
which implements one step of reduction. If the inputArith
cannot take a step (either because of an error, or because there is no more reduction left to do),step
returnsNothing
. Some notes to help you in your implementation are below, with keywords highlighted. Start writing your implementation and consult the list of notes as you go.Of course, literals cannot take a step.
Variables cannot take a step either. Note we are not going to pass along an environment mapping variables to values, as we did with
interpArith
. A variable by itself simply cannot take a step. You will see how to deal with variables when you get tolet
.- To step an application of a binary operator, \(e_1 \mathbin{op} e_2\):
First see if the left-hand argument \(e_1\) can take a step (by calling
step
recursively). If \(e_1 \longrightarrow e_1'\) (that is, \(e_1\) can successfully take a step, resulting in \(e_1'\)), then the result of stepping \(e_1 \mathbin{op} e_2\) is \(e_1' \mathbin{op} e_2\).For example,
"(3+2) * (2*3)"
steps to"5 * (2*3)"
. (Again, these strings are really just standing in for appropriate parsedArith
values.)Otherwise, if the left-hand argument cannot take a step, see if the right-hand argument can take a step. For example,
"5 * (2*3)"
steps to"5 * 6"
.If neither argument can take a step, then see if they are both literals appropriate to the operator. If so, do the operation. For example, given
"5 * 6"
, neither side can take a step (since they are already literals), so the whole expression steps to"30"
.Remember to check for division by zero. Instead of generating an error, however, an expression like
"5 / 0"
simply cannot take a step; it is “stuck”.Otherwise (e.g. if you have something like
"5 + True"
), the operator cannot take a step.
I will let you think about if and let on your own. A few hints:
Use the example reduction from above (of
if 3 + 5 < 7 then 2*5 else (let x = 3 in x+x)
) to help guide you.Remember the
subst
function!
Once you get to the point where you are annoyed by pattern-matching on Maybe, consider these questions:
What is the type of
Bin op <$> step e1 <*> Just e2
? What does it evaluate to?What is the type of
(Bin op <$> step e1 <*> Just e2) <|> (Bin op <$> Just e1 <*> step e2)
? What does it evaluate to?
Can you use these tools to write
step
without ever explicitly writing acase
on the results of recursive calls tostep
?
Now write a function
reduce :: Arith -> Arith
which simply iteratesstep
until the expression cannot take another step, and returns the final, un-steppable expression.Finally, write a function
eval2 :: String -> IO ()
which works similarly toeval
but usesreduce
instead ofinterpArith
. You can use this to test your implementation ofstep
, to make sure that stepwise reduction yields the same results asinterpArith
.
Feedback
How long would you estimate that you spent working on this module?
Were any parts particularly confusing or difficult?
Were any parts particularly fun or interesting?
Record here any other questions, comments, or suggestions for improvement.