From: Chris <chris.barker@nyu.edu>
Date: Sat, 14 Mar 2015 13:18:30 +0000 (-0400)
Subject: developing exx
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=8cd605a9141eba85196521657010fb7ae6f0ada1

developing exx
---

diff --git a/code/reduction.ml b/code/reduction.ml
index 3882c7fb..188a90b6 100644
--- a/code/reduction.ml
+++ b/code/reduction.ml
@@ -10,8 +10,8 @@ let rec free_in (ident:identifier) (term:lambdaTerm) : bool =
   match term with
     | Constant _ -> false
     | Var(var_ident) -> var_ident = ident
-    | Abstract(bound_ident, body) -> bound_ident <> ident && free_in ident body
-    | App(head, arg) -> free_in ident head || free_in ident arg
+(*    | Abstract(bound_ident, body) ->  COMPLETE THIS LINE *)
+(*    | App(head, arg) -> COMPLETE THIS LINE *)
     | IfThenElse(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no
     | Let(bound_ident, arg, body) -> free_in ident arg || (bound_ident <> ident && free_in ident body)
 
diff --git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn
index aabcbe07..f6a48030 100644
--- a/exercises/_assignment6.mdwn
+++ b/exercises/_assignment6.mdwn
@@ -24,5 +24,33 @@ recursive reduction function.)
 
 <!-- just add early no-op cases for Ka and Sab -->
 
-## Evaluation in the untyped lambda calculus
+## 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:
+