developing exx

[lambda.git] / topics / _week7_eval_cl.mdwn

<!-- λ Λ ∀ ≡ α β ω Ω -->

[[!toc levels=2]]

# Reasoning about evaluation order in Combinatory Logic

We've discussed [[evaluation order|topics/week3_evaluation_order]]
before, primarily in connection with the untyped lambda calculus.
Whenever a term contains more than one redex, we have to choose which
one to reduce, and this choice can make a difference.  For instance,
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 recent introduction of sum types (disjoint union), we are now
in a position to gain a deeper understanding of evaluation order by
writing a program that experiments 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.  We
will not fully succeed in this first attempt, but we will make good
progress. 

The first evaluator we will develop will evaluate terms in Combinatory
Logic.  This significantly simplifies the discussion, since we won't need
to worry about variables or substitution.  As we develop and extend
our evaluator in future weeks, we'll switch to lambdas, but for now,
working with the 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 ~~> a
    Sabc ~~> ac(bc)

where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
how to embed the untyped lambda calculus in CL, so it's no
surprise that evaluation order issues arise in CL.  To illustrate,
we'll use the following definition:

    skomega = SII(SII)
            ~~> I(SII)(I(SII))
            ~~> SII(SII)

We'll use the same symbol, `Ω`, though: in a lambda term, `Ω` refers
to omega, but in a CL term, `Ω` refers to skomega as defined here.

If we consider the term

    KIΩ == KI(SII(SII))

we can choose to reduce the leftmost redex by applying the reduction
rule for `K`, in which case the term reduces to the normal form `I` in
one step; or we can choose to reduce the skomega part, by applying the
reduction rule `S`, in which case we do not get a normal form, and
we're headed towards an infinite loop.

With sum types, we can define terms in CL in OCaml as follows:

    type term = I | S | K | FA of (term * term)

    let skomega = FA (FA (FA (S, I), I), FA (FA (S, I), I))

This recursive type definition says that a term in CL is either one of
the three simple expressions, or else a pair of CL expressions.
Following Heim and Kratzer, `FA` stands for Functional Application.
With this type definition, we can encode skomega, as well as other
terms whose reduction behavior we want to try to control.

Using pattern matching, it is easy to code the one-step reduction
rules for CL:

    let reduce_one_step (t:term):term = match t with
        FA(I,a) -> a
      | FA(FA(K,a),b) -> a
      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
      | _ -> 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 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.

    (II)K ~~> IK ~~> K

That is, we want to be able to first evaluate the redex `II` 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 somewhat subtle.  To
truly understand, 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 examining a 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 return
the result.

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.  We'll do this by mapping the reduction function onto
the parts 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 what we need is access to the subterms, we do pattern matching
on the input term.  If the input is simple (the first three `match`
cases), we return it without further processing.  But if the input is
complex, we first process the subexpressions, and only then see if we
have a redex at the top level.  To understand how this works, follow
the trace carefully:

    # reduce2 (FA(FA(I,I),K));;
    reduce2 <-- FA (FA (I, I), K)

      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
      reduce2 --> I

      reduce2 <-- K           ; third 
      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`.  

There are three recursive calls to the reduce2 function, each of
which gets triggered during the processing of this example.  They have
been marked in the trace.  

The don't quite go in the order in which they appear in the code,
however!  We see from the trace that it begins with the right-hand
expression, `K`.  We didn't explicitly tell it to begin with the
right-hand subexpression, so control over evaluation order is starting
to spin out of our control.  (We'll get it back later, don't worry.)

In any case, in the second main recursive call, we evaluate `II`.  The
result is `I`.  

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 third recursive call checks that there is no more
reduction work to be done (there isn't), and that's our final result.

You can see in more detail what is going on by tracing both reduce2
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.

Running the evaluator with this input leads to an infinite loop, and
the only way to get out is to kill the interpreter with control-c.

Instead of performing the leftmost reduction first, and recognizing 
that this term reduces to the normal form `I`, we get lost endlessly
trying to reduce skomega.

## Laziness is hard to overcome

To emphasize that our evaluation order here is at the mercy of the
evaluation order of OCaml, here is the exact same program translated
into Haskell.  We'll put them side by side to emphasize the exact parallel.

<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Ω`:

    *Main> reduce2 (FA (FA K I) skomega)
    I

Woa!  First of all, this is wierd.  Haskell's evaluation strategy is
called "lazy".  Apparently, Haskell is so lazy that even after we've
asked it to construct t' by evaluating `reduce2 a` and `reduce2 b`, it
doesn't bother computing `reduce2 b`.  Instead, it waits to see if we
ever really need to use the result.

So the program as written does NOT fully determine evaluation order
behavior.  At this stage, we have defined an evaluation order that
still depends on the evaluation order of the underlying interpreter.

There are two questions we could ask: Can we adjust the OCaml
evaluator to exhibit lazy behavior?  and Can we adjust the Haskell
evaluator to exhibit eager behavior?  The answer to the first question
is easy and interesting, and we'll give it right away.  The answer to
the second question is also interesting, but not easy.  There are
various tricks available in Haskell we could use (such as the `seq`
operator), but a fully general, satisifying resolution will have to
wait until we have Continuation Passing Style transforms. 

The answer to the first question (Can we adjust the OCaml evaluator to
exhibit lazy behavior?) is quite simple:

<pre>
let rec reduce3 (t:term):term = match t with
    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'
</pre>

There is only one small difference: instead of setting `t'` to `FA
(reduce a, reduce b)`, we omit one of the recursive calls, and 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?*

[By the way, the evaluators given here are absurdly inefficient computationally.
Some computer scientists have trouble even looking at code this inefficient, but 
the emphasis here is on getting the concepts across as simply as possible.]