# Assignment 6 (week 7)

## Evaluation order in Combinatory Logic

1. Give a term that the lazy evaluators (either [[the Haskell
evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
normal form, i.e., that contains a redex somewhere inside of it after
it has been reduced.

<!-- reduce3 (FA (K, FA (I, I))) -->

2. One of the [[criteria we established for classifying reduction
strategies|topics/week3_evaluation_order]] strategies is whether they
reduce subexpressions hidden under lambdas.  That is, for a term like
`(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
we reduce further to `\y.z`?  Explain what the corresponding question
would be for CL. Using either the OCaml CL evaluator or the Haskell
evaluator developed in the wiki notes, prove that the evaluator does
reduce expressions inside of at least some "functional" CL
expressions.  Then provide a modified evaluator that does not perform
reductions in those positions. (Just give the modified version of your
recursive reduction function.)

<!-- just add early no-op cases for Ka and Sab -->

## Evaluation in the untyped lambda calculus: substitution

Once you grok reduction and evaluation order in Combinatory Logic,
we're going to begin to construct an evaluator for a simple language
that includes lambda abstraction.  We're going to work through the
issues twice: once with a function that does substitution in the
obvious way.  You'll see it's somewhat complicated.  The complications
come from the need to worry about variable capture.  (Seeing these
complications should give you an inkling of why we presented the
evaluation order discussion using Combinatory Logic, since we don't
need to worry about variables in CL.)  

We're not going to ask you to write the entire program yourself.
Instead, we're going to give you [[the complete program, minus a few
little bits of glue|code/reduction.ml]].  What you need to do is
understand how it all fits together.  When you do, you'll understand
how to add the last little bits to make functioning program.  Here's a
first target for when you get it working:

    # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
    - : lambdaTerm = Constant (Num 3)

1. In the previous homework, you built a function that took an
identifier and a lambda term and returned a boolean representing
whether that identifier occured free inside of the term.  Your first
task is to adapt your previous solution as necessary to work with the
code base.  Once you have your function working, you should be able to
run queries such as this: