+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' ++ +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. + +

+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' ++ +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. + +

+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' ++ +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. + +

+let rec reduce3 (t:term):term = match t with + I -> I + | K -> K + | S -> S + | FA (a, b) -> + let t' = FA (reduce3 a, b) in + if (is_redex t') then reduce3 (reduce_one_step t') + else t' ++ +There is only one small difference: instead of setting `t'` to +`FA (reduce a, reduce b)`, we have `FA (reduce a, b)`. That is, we +don't evaluate the right-hand subexpression at all. Ever! The only +way to get evaluated is to somehow get into functor position. + + # reduce3 (FA(FA(K,I),skomega));; + - : term = I + # reduce3 skomega;; + C-c C-cInterrupted. + +The evaluator now has no trouble finding the normal form for `KIÎ©`, +but evaluating skomega still gives an infinite loop. + +As a final note, we can clarify the larger question at the heart of +this discussion: + +*How can we can we specify the evaluation order of a computational +system in a way that is completely insensitive to the evaluation order +of the specification language?* -- 2.11.0