has to come from a subsequent re-invocation of the function.
-Let's think about how we should detect that the term has been reduced as far as we can take it. In the substitute-and-repeat interpreter Chris demonstrated for combinatory logic, we had the `reduce_if_redex` function perform a single reduction *if it could*, and then it was up to the caller to compare the result to the original term to see whether any reduction took place. That worked for the example we had. But it has some disadvantages. One is that it's inefficient. Another is that it's sensitive to the idiosyncrasies of how your programming language handles equality comparisons on complex structures; and these details turn out to be very complex and vary from language to language (and even across different versions of different implementations of a single language). We'd be glad to discuss these subtleties offline, but if you're not prepared to master them, it would be smart to foster an ingrained hesitation to blindly applying a language's `=` operator to complex structures. (Some problem cases: large numbers, set structures, structures that contain functions.) A third difficulty is that it's sensitive to the particular combinators we took as basic. With `S` and `K` and `I`, it can never happen that a term has been reduced, but the output is identical to the input. That can happen in the lambda calculus, though (remember `ω ω`); and it can happen in combinatory logic if other terms are chosen as primitive (`W W1 W2` reduces to `W1 W2 W2`, so let them all just be plain `W`s).
+Let's think about how we should detect that the term has been reduced as far as we can take it. In the substitute-and-repeat interpreter Chris demonstrated for combinatory logic, we had the `reduce_if_redex` function perform a single reduction *if it could*, and then it was up to the caller to compare the result to the original term to see whether any reduction took place. That worked for the example we had. But it has some disadvantages. One is that it's inefficient. Another is that it's sensitive to the idiosyncrasies of how your programming language handles equality comparisons on complex structures; and these details turn out to be very complex and vary from language to language (and even across different versions of different implementations of a single language). We'd be glad to discuss these subtleties offline, but if you're not prepared to master them, it would be smart to foster an ingrained hesitation to blindly applying a language's `=` operator to complex structures. (Some problem cases: large numbers, set structures, structures that contain functions, cyclic structures.) A third difficulty is that it's sensitive to the particular combinators we took as basic. With `S` and `K` and `I`, it can never happen that a term has been reduced, but the output is identical to the input. That can happen in the lambda calculus, though (remember `ω ω`); and it can happen in combinatory logic if other terms are chosen as primitive (`W W1 W2` reduces to `W1 W2 W2`, so let them all just be plain `W`s).
So let's consider different strategies for how to detect that the term cannot be reduced any further. One possibility is to write a function that traverses the term ahead of time, and just reports whether it's already a result, without trying to perform any reductions itself. Another strategy is to "raise an exception" or error when we ask the `reduce_head_once` function to reduce an irreducible term; then we can use OCaml's error-handling facilities to "catch" the error at an earlier point in our code and we'll know then that we're finished. Pierce's code used a mix of these two strategies.
This makes sure to substitute the replacement for any free occurrences of `Var ident` in the original, renaming bound variables in the original as needed so that no terms free in the replacement become captured by binding `Lambda`s or `Let`s in the original. This function is tricky to write correctly; so we supplied it for you.
-However, one of the helper functions that *it* calls is `free_in (ident : identifier) (term : term) : bool`, and this was a function that you did [[write for an earlier homework|/exercises/assignment5/#occurs_free]]. Hence we asked you to adapt your implementation of that to the term datatype used in this interpreter. Here is a skeleton of this function:
+However, one of the helper functions that *it* calls is `free_in (ident : identifier) (term : term) : bool`, and this was a function that you did [[write for an earlier homework|/exercises/assignment5-6#occurs_free]]. Hence we asked you to adapt your implementation of that to the term datatype used in this interpreter. Here is a skeleton of this function:
let rec free_in (ident : identifier) (term : term) : bool =
match term with
Now `Closure`s are not a new kind of lambda _term_: the syntax for our language doesn't have any constituents that get parsed into `Closure`s. `Closure`s are only created _during the course of evaluating_ terms: specifically, when a variable gets bound to an abstract, which may itself contain variables that are locally free (not bound by the abstract itself). This is why we have separate datatypes for _terms_ and for the _results_ that terms can evaluate to. `Closure`s are results, but they aren't terms. `App`s are terms, but not results. Our boolean and number literals, as well as our primitive functions, constructors, and destructors, are both.
+In later weeks, we will see more examples of results that aren't terms, but can only be generated during the course of a computation. (I'm thinking of mutable reference cells. Arguably, partially applied constructors are yet another example, that we're already familiar with.)
+
Getting, reading, and compiling the source code
-----------------------------------------------
-You can download the source code for the intepreter [[here|/code/untyped_full-1.3.tgz]]. That link will always give you the latest version. We will update it as we find any issues. Let us know about any difficulties you experience.
+You can download the source code for the intepreter [[here|/code/untyped_full-1.7.tgz]]. That link will always give you the latest version. We will update it as we find any issues. Let us know about any difficulties you experience.
When you unpack the downloaded source code, you will get a folder with the following contents, sorted here by logical order rather than alphabetically.
ocamlc -o interp.exe lolevel.cmo types.cmo hilevel.cmo primitives.cmo \
engine.cmo parser.cmo lexer.cmo main.cmo
-If your computer doesn't ... TODO
-
OK, I built the interpeter. How can I use it?
---------------------------------------------
/* note that it's not f x (g y) (h z) */
"strings" /* you can input these and pass them around, but can't perform any operations on them */
-Predefined combinators include: `S`, `K` (same as `const`), `I` (same as `id`), `B` (same as `(o)`, occurring in prefix not infix position), `C` (same as `flip`), `T`, `V` (the Church pairing combinator), `W`, `M` (better known as `ω`), and `L`.
+Predefined combinators include: `S`, `K` (same as `const`), `I` (same as `id`), `B` (same as `(o)`, occurring in prefix not infix position), `C` (same as `flip`), `T` (same as `flip ($)`), `V` (the Church pairing combinator), `W`, `M` (better known as `ω`), and `L`.
The parser also accepts `letrec ... in ...` terms, but currently there is no implementation for how to reduce/interpret these (that's for a later assignment), so you'll just get an error.