# Reasoning about evaluation order in Combinatory Logic
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
+We've discussed [[evaluation order|topics/week3_evaluation_order]]
+before, primarily in connection with the untyped lambda calculus.
+Whenever a term contains more than one redex, we have to choose which
+one to reduce, and this choice can make a difference. For instance,
+recall that
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
+ Ω == ωω == (\x.xx)(\x.xx), so
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI
- -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
-
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
-
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
+ ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
+ * *
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
+There are two redexes in this term; we've marked the operative lambdas
+with a star. If we reduce the leftmost redex first, the term reduces
+to the normal form `I` in one step. But if we reduce the rightmost
+redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
+danger of entering an infinite loop.
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
+Thanks to the introduction of sum types (disjoint union) in the last lecture, we
+are now in a position to gain a deeper understanding of evaluation
+order by writing a program that allows us to reasoning explicitly about evaluation.
One thing we'll see is that it is all too easy for the evaluation
order properties of an evaluator to depend on the evaluation order
properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
+written. We would like to write an evaluator in which the order of
evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
+find an order-insensitive way to reason about evaluation order. We
+will not fully succeed in this first attempt, but we will make good
+progress.
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
+The first evaluator we will develop will evaluate terms in Combinatory
+Logic. This significantly simplifies the discussion, since we won't
need to worry about variables or substitution. As we develop and
extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
+now, working with the simplicity of Combinatory Logic will make it
+easier to highlight evaluation order issues.
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
+A brief review of Combinatory Logic: a term in CL is the combination
+of three basic expressions, `S`, `K`, and `I`, governed by the
+following reduction rules:
Ia ~~> a
- Kab ~~> b
+ Kab ~~> a
Sabc ~~> ac(bc)
where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
+how to embed the untyped lambda calculus in CL, so it's no surprise
+that evaluation order issues arise in CL. To illustrate, we'll use
+the following definition:
- skomega = SII(SII)
+ skomega = SII
+ Skomega = skomega skomega == SII(SII)
~~> I(SII)(I(SII))
~~> SII(SII)
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
+We'll use the same symbol, `Ω`, for Omega and Skomega: in a lambda
+term, `Ω` refers to Omega, but in a CL term, `Ω` refers to Skomega as
+defined here.
+
+Just as in the corresponding term in the lambda calculus, CL terms can
+contain more than one redex:
KIΩ == KI(SII(SII))
+ * *
-we can choose to reduce the leftmost redex by firing the reduction
+we can choose to reduce the leftmost redex by applying the reduction
rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
+one step; or we can choose to reduce the Skomega part, by applying the
+reduction rule `S`, in which case we do not get a normal form, and
we're headed towards an infinite loop.
-With sum types, we can define terms in CL in OCaml as follows:
+With sum types, we can define CL terms in OCaml as follows:
- type term = I | S | K | FA of (term * term)
+ type term = I | K | S | App of (term * term)
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
+ let skomega = App (App (App (S, I), I), App (App (S, I), I))
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
+This type definition says that a term in CL is either one of the three
+simple expressions (`I`, `K`, or `S`), or else a pair of CL
+expressions. `App` stands for Functional Application. With this type
+definition, we can encode skomega, as well as other terms whose
+reduction behavior we want to try to control.
Using pattern matching, it is easy to code the one-step reduction
rules for CL:
let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
+ App(I,a) -> a
+ | App(App(K,a),b) -> a
+ | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
| _ -> t
- # reduce_one_step (FA(FA(K,S),I));;
+ # reduce_one_step (App(App(K,S),I));;
- : term = S
# reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
+ - : term = App (App (I, App (App (S, I), I)), App (I, App (App (S, I), I)))
+
+The definition of `reduce_one_step` explicitly says that it expects
+its input argument `t` to have type `term`, and the second `:term`
+says that the type of the output it delivers as a result will be of
+type `term`.
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
+The type constructor `App` obscures things a bit, but it's still
+possible to see how the one-step reduction function is just the
+reduction rules for CL. The OCaml interpreter shows us that the
+function faithfully recognizes that `KSI ~~> S`, and `skomega ~~>
+I(SII)(I(SII))`.
We can now say precisely what it means to be a redex in CL.
# is_redex K;;
- : bool = false
- # is_redex (FA(K,I));;
+ # is_redex (App(K,I));;
- : bool = false
- # is_redex (FA(FA(K,I),S));;
+ # is_redex (App(App(K,I),S));;
- : bool = true
# is_redex skomega;;
- : book = true
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
+Warning: this definition relies on the accidental fact that the
+one-step reduction of a CL term is never identical to the original
+term. This would not work for the untyped lambda calculus, since
+`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.
+
+Note that in order to decide whether two terms are equal, OCaml has to
+recursively compare the elements of complex CL terms. It is able to
+figure out how to do this because we provided an explicit definition
+of the datatype `term`.
As you would expect, a term in CL is in normal form when it contains
-no redexes.
+no redexes (analogously for head normal form, weak head normal form, etc.)
In order to fully reduce a term, we need to be able to reduce redexes
that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
Because we need to process subparts, and because the result after
processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
+structure of our evaluation function has to be somewhat subtle. To
+truly understand, you will need to do some sophisticated thinking
+about how recursion works.
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
+We'll develop our full reduction function in two stages. Once we have
+it working, we'll then consider a variant.
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
+ let rec reduce_stage1 (t:term):term =
+ if (is_redex t) then reduce_stage1 (reduce_one_step t)
else t
If the input is a redex, we ship it off to `reduce_one_step` for
processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
-
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
-
-But this function doesn't do enough reduction.
+itself a redex, we recursively call `reduce_stage1`. The recursion
+will continue until the result is no longer a redex. We're aiming at
+allowing the evaluator to recognize that
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
+ I (I K) ~~> I K ~~> K
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
-
- let rec reduce2 (t:term):term = match t with
- I -> I
- | K -> K
- | S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
- else t'
-
-Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
-carefully:
-
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
-
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
-
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
-
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
- - : term = K
-
-Ok, there's a lot going on here. Since the input is complex, the
-first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
-
-In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
-
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
-reduction work to be done (there isn't), and that's our final result.
-
-You can see in more detail what is going on by tracing both reduce2
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
-
- # reduce2 (FA(FA(K,I),skomega));;
- C-c C-cInterrupted.
-
-instead of performing the leftmost reduction first, and recognizing
-that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell. We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml Haskell
-========================================================== =========================================================
-
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell). But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term has more than one redex,
-we have to choose which one to reduce, and this choice can make a
-difference. For instance, in the term `((\x.I)(ωω)`, if we reduce the
-leftmost redex first, the term reduces to the normal form `I` in one
-step. But if we reduce the left most redex instead (namely, `(ωω)`),
-we do not arrive at a normal form, and are in danger of entering an
-infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-One thing we'll see is that it is all too easy for the evaluation
-order properties of an evaluator to depend on the evaluation order
-properties of the programming language in which the evaluator is
-written. We will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language. The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic. That will significantly simplify the program, since we won't
-need to worry about variables or substitution. As we develop and
-extend our evaluator in future weeks, we'll switch to lambdas, but for
-now, working with the elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
- Ia ~~> a
- Kab ~~> b
- Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
- skomega = SII(SII)
- ~~> I(SII)(I(SII))
- ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`. If we consider the term
-
- KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing the reduction
-rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
- type term = I | S | K | FA of (term * term)
-
- let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
- let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-Using pattern matching, it is easy to code the one-step reduction
-rules for CL:
-
- let reduce_one_step (t:term):term = match t with
- FA(I,a) -> a
- | FA(FA(K,a),b) -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
- | _ -> t
-
- # reduce_one_step (FA(FA(K,S),I));;
- - : term = S
- # reduce_one_step skomega;;
- - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` obscures
-things a bit, but it's still possible to see how the one-step
-reduction function is just the reduction rules for CL. The
-OCaml interpreter shows us that the function faithfully recognizes
-that `KSI ~~> S`, and `skomega ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
- let is_redex (t:term):bool = not (t = reduce_one_step t)
-
- # is_redex K;;
- - : bool = false
- # is_redex (FA(K,I));;
- - : bool = false
- # is_redex (FA(FA(K,I),S));;
- - : bool = true
- # is_redex skomega;;
- - : book = true
-
-Warning: this definition relies on the fact that the one-step
-reduction of a CL term is never identical to the original term. This
-would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Note that in
-order to decide whether two terms are equal, OCaml has to recursively
-compare the elements of complex CL terms. It is able to figure out
-how to do this because we provided an explicit definition of the
-datatype Term.
-
-As you would expect, a term in CL is in normal form when it contains
-no redexes.
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-
- (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
-structure of our evaluation function has to be quite subtle. To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works. We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
+When trying to understand how recursive functions work, it can be
+extremely helpful to examining an execution trace of inputs and
outputs.
-We'll develop our full reduction function in stages. Once we have it
-working, we'll then consider some variants. Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
+ # #trace reduce_stage1;;
+ reduce_stage1 is now traced.
+ # reduce_stage1 (App (I, App (I, K)));;
+ reduce_stage1 <-- App (I, App (I, K))
+ reduce_stage1 <-- App (I, K)
+ reduce_stage1 <-- K
+ reduce_stage1 --> K
+ reduce_stage1 --> K
+ reduce_stage1 --> K
+ - : term = K
- let rec reduce1 (t:term):term =
- if (is_redex t) then reduce1 (reduce_one_step t)
- else t
+In the trace, "`<--`" shows the input argument to a call to
+`reduce_stage1`, and "`-->`" shows the output result.
-If the input is a redex, we ship it off to `reduce_one_step` for
-processing. But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce1`. The recursion will
-continue until the result is no longer a redex.
+Since the initial input (`I(IK)`) is a redex, the result after the
+one-step reduction is `IK`. We recursively call `reduce_stage1` on
+this input. Since `IK` is itself a redex, the result after one-step
+reduction is `K`. We recursively call `reduce_stage1` on this input. Since
+`K` is not a redex, the recursion bottoms out, and we return the
+result.
- #trace reduce1;;
- reduce1 is now traced.
- # reduce1 (FA (I, FA (I, K)));;
- reduce1 <-- FA (I, FA (I, K))
- reduce1 <-- FA (I, K)
- reduce1 <-- K
- reduce1 --> K
- reduce1 --> K
- reduce1 --> K
- - : term = K
+But this function doesn't do enough reduction. We want to recognize
+the following reduction path:
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`. We recursively call `reduce1` on this
-input. Since `IK` is itself a redex, the result after one-step
-reduction is `K`. We recursively call `reduce1` on this input. Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.
+ I I K ~~> I K ~~> K
-But this function doesn't do enough reduction.
+But the reduction function as written above does not deliver this result:
- # reduce1 (FA (FA (I, I), K));;
- - : term = FA (FA (I, I), K)
+ # reduce_stage1 (App (App (I, I), K));;
+ - : term = App (App (I, I), K)
-Because the top-level term is not a redex, `reduce1` returns it
-without any evaluation. What we want is to evaluate the subparts of a
-complex term.
+Because the top-level term is not a redex to start with,
+`reduce_stage1` returns it without any evaluation. What we want is to
+evaluate the subparts of a complex term. We'll do this by evaluating
+the subparts of the top-level expression.
- let rec reduce2 (t:term):term = match t with
+ let rec reduce (t:term):term = match t with
I -> I
| K -> K
| S -> S
- | FA (a, b) ->
- let t' = FA (reduce2 a, reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t')
+ | App (a, b) ->
+ let t' = App (reduce a, reduce b) in
+ if (is_redex t') then reduce 2 (reduce_one_step t')
else t'
Since we need access to the subterms, we do pattern matching on the
-input term. If the input is simple, we return it. If the input is
-complex, we first process the subexpressions, and only then see if we
-have a redex. To understand how this works, follow the trace
+input. If the input is simple (the first three `match` cases), we
+return it without further processing. But if the input is complex, we
+first process the subexpressions, and only then see if we have a redex
+at the top level. To understand how this works, follow the trace
carefully:
- # reduce2 (FA(FA(I,I),K));;
- reduce2 <-- FA (FA (I, I), K)
+ # reduce (App(App(I,I),K));;
+ reduce <-- App (App (I, I), K)
- reduce2 <-- K ; first main recursive call
- reduce2 --> K
+ reduce <-- K ; first main recursive call
+ reduce --> K
- reduce2 <-- FA (I, I) ; second main recursive call
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
- reduce2 --> I
- reduce2 <-- I
+ reduce <-- App (I, I) ; second main recursive call
+ reduce <-- I
+ reduce --> I
+ reduce <-- I
+ reduce --> I
+ reduce <-- I
+ reduce --> I
+ reduce --> I
- reduce2 --> I ; third main recursive call
- reduce2 --> I
-
- reduce2 <-- K ; fourth
- reduce2 --> K
- reduce2 --> K
+ reduce <-- K ; third
+ reduce --> K
+ reduce --> K
- : term = K
Ok, there's a lot going on here. Since the input is complex, the
first thing the function does is construct `t'`. In order to do this,
-it must reduce the two main subexpressions, `II` and `K`. But we see
-from the trace that it begins with the right-hand expression, `K`. We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control. (We'll get it back later, don't worry.)
+it must reduce the two main subexpressions, `II` and `K`.
+
+There are three recursive calls to the `reduce` function, each of
+which gets triggered during the processing of this example. They have
+been marked in the trace.
+
+The don't quite go in the order in which they appear in the code,
+however! We see from the trace that it begins with the right-hand
+expression, `K`. We didn't explicitly tell it to begin with the
+right-hand subexpression, so control over evaluation order is starting
+to spin out of our control. (We'll get it back later, don't worry.)
In any case, in the second main recursive call, we evaluate `II`. The
-result is `I`. The third main recursive call tests whether this
-result needs any further processing; it doesn't.
+result is `I`.
-At this point, we have constructed `t' == FA(I,K)`. Since that's a
+At this point, we have constructed `t' == App(I,K)`. Since that's a
redex, we ship it off to reduce_one_step, getting the term `K` as a
-result. The fourth recursive call checks that there is no more
+result. The third recursive call checks that there is no more
reduction work to be done (there isn't), and that's our final result.
-You can see in more detail what is going on by tracing both reduce2
+You can see in more detail what is going on by tracing both reduce
and reduce_one_step, but that makes for some long traces.
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
+So we've solved our first problem: reduce recognizes that `IIK ~~>
K`, as desired.
-Because the OCaml interpreter evaluates the rightmost expression
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not. And sure
-enough,
+Because the OCaml interpreter evaluates each subexpression in the
+course of building `t'`, however, it will always evaluate the right
+hand subexpression, whether it needs to or not. And sure enough,
- # reduce2 (FA(FA(K,I),skomega));;
+ # reduce (App(App(K,I),skomega));;
C-c C-cInterrupted.
-instead of performing the leftmost reduction first, and recognizing
+Running the evaluator with this input leads to an infinite loop, and
+the only way to get out is to kill the interpreter with control-c.
+
+Instead of performing the leftmost reduction first, and recognizing
that this term reduces to the normal form `I`, we get lost endlessly
trying to reduce skomega.
+## Laziness is hard to overcome
+
To emphasize that our evaluation order here is at the mercy of the
evaluation order of OCaml, here is the exact same program translated
into Haskell. We'll put them side by side to emphasize the exact parallel.
OCaml Haskell
========================================================== =========================================================
-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
+type term = I | S | K | App of (term * term) data Term = I | S | K | App Term Term deriving (Eq, Show)
+
+let skomega = App (App (App (S,I), I), App (App (S,I), I)) skomega = (App (App (App S I) I) (App (App S I) I))
+
+ reduce_one_step :: Term -> Term
+let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
+ App(I,a) -> a App I a -> a
+ | App(App(K,a),b) -> a App (App K a) b -> a
+ | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) App (App (App S a) b) c -> App (App a c) (App b c)
+ | _ -> t _ -> t
+
+ is_redex :: Term -> Bool
+let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
+
+ reduce :: Term -> Term
+let rec reduce (t:term):term = match t with reduce t = case t of
+ I -> I I -> I
+ | K -> K K -> K
+ | S -> S S -> S
+ | App (a, b) -> App a b ->
+ let t' = App (reduce a, reduce b) in let t' = App (reduce a) (reduce b) in
+ if (is_redex t') then reduce (reduce_one_step t') if (is_redex t') then reduce (reduce_one_step t')
+ else t' else t'
</pre>
-There are some differences in the way types are specified, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
+There are some differences in the way types are made explicit, and in
+the way terms are specified (`App(a,b)` for Ocaml versus `App a b` for
Haskell). But the two programs are essentially identical.
-Yet the Haskell program finds the normal form for KIΩ.
+Yet the Haskell program finds the normal form for `KIΩ`:
- *Main> reduce2 (FA (FA K I) skomega)
+ *Main> reduce (App (App K I) skomega)
I
Woa! First of all, this is wierd. Haskell's evaluation strategy is
called "lazy". Apparently, Haskell is so lazy that even after we've
-asked it to construct t' by evaluating `reduce2 a` and `reduce2 b`, it
-doesn't bother computing `reduce2 b`. Instead, it waits to see if we
+asked it to construct t' by evaluating `reduce a` and `reduce b`, it
+doesn't bother computing `reduce b`. Instead, it waits to see if we
ever really need to use the result.
-So despite intuitions, the program as written does NOT determine
-evaluation order behavior. At this stage, we have defined an
-evaluation order that still depends on the evaluation order of the
-underlying interpreter.
+So the program as written does NOT fully determine evaluation order
+behavior. At this stage, we have defined an evaluation order that
+still depends on the evaluation order of the underlying interpreter.
-There are two questions we could ask: Can we adjust the OCaml
-evaluator to exhibit lazy behavior? and Can we adjust the Haskell
-evaluator to exhibit eager behavior? The answer to the first question
-is easy and interesting, and we'll give it right away. The answer to
-the second question is also interesting, but not easy. There are
-various tricks available in Haskell we could use (such as the `seq`
+There are two questions we could ask:
+
+* Can we adjust the OCaml evaluator to exhibit lazy behavior?
+
+* Can we adjust the Haskell evaluator to exhibit eager behavior?
+
+The answer to the first question is easy and interesting, and we'll
+give it right away. The answer to the second question is also
+interesting, but not easy. There are various tricks available in
+Haskell we could use (such as the `seq` operator, or the `deepseq`
operator), but a fully general, satisifying resolution will have to
-wait until we have Continuation Passing Transforms.
+wait until we have Continuation Passing Style transforms.
The answer to the first question (Can we adjust the OCaml evaluator to
exhibit lazy behavior?) is quite simple:
<pre>
-let rec reduce3 (t:term):term = match t with
+let rec reduce_lazy (t:term):term = match t with
I -> I
| K -> K
| S -> S
- | FA (a, b) ->
- let t' = FA (reduce3 a, b) in
- if (is_redex t') then reduce3 (reduce_one_step t')
+ | App (a, b) ->
+ let t' = App (reduce_lazy a, b) in
+ if (is_redex t') then reduce_lazy (reduce_one_step t')
else t'
</pre>
-There is only one small difference: instead of setting `t'` to
-`FA (reduce a, reduce b)`, we have `FA (reduce a, b)`. That is, we
-don't evaluate the right-hand subexpression at all. Ever! The only
-way to get evaluated is to somehow get into functor position.
+There is only one small difference: instead of setting `t'` to `App
+(reduce a, reduce b)`, we omit one of the recursive calls, and have
+`App (reduce a, b)`. That is, we don't evaluate the right-hand
+subexpression at all. Ever! The only way to get evaluated is to
+somehow get into functor position.
- # reduce3 (FA(FA(K,I),skomega));;
+ # reduce3 (App(App(K,I),skomega));;
- : term = I
# reduce3 skomega;;
C-c C-cInterrupted.
The evaluator now has no trouble finding the normal form for `KIΩ`,
but evaluating skomega still gives an infinite loop.
-As a final note, we can clarify the larger question at the heart of
+We can now clarify the larger question at the heart of
this discussion:
*How can we can we specify the evaluation order of a computational
system in a way that is completely insensitive to the evaluation order
of the specification language?*
+
+As a final note, we should mention that the evaluators given here are
+absurdly inefficient computationally. Some computer scientists have
+trouble even looking at code this inefficient, but the emphasis here
+is on getting the concepts across as simply as possible.