-[[!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.
-
- # 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 specified, 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Ω.
-