Reduce lambda-expressions in WHNF

Question

I have to reduce the following lambda-expression into WHNF, but I am not quite sure how to do it:

(λx y. x 3) (+ 4) (+ 6 7)

So, how do I do it? Call-By-Name Reduction?

Is this expression(other example) (λz x. (λx. x) z) x in WHNF yet?

Answer 1

WHNF (Weak Head Normal Form) means that you either have a value (e.g. an integer) or a the expression is of the kind (λx . e(x)) where e(x) is an expression that may contain references to x, so basically you have that the result is a function.

In your case the expression you have contains some applications that need to be reduced:

(λx . λy. x 3) (+ 4) (+ 6 7) = (λy . (+ 4) 3) (+ 6 7)
                             = (+ 4)  3
                             = 7

Note that in this case y does not appear in the body of the function, and thus the + 6 7 "disappears" during reduction.

---

No, (λz x. (λx. x) z) x is not in WHNF because the "top operator" is still an application. Note that the reduction in this case is a bit tricky because you have a free variable x outside and the λ also binds x. However we can first do some renaming: (λz k. (λt. t) z) x and now perform the reduction: (λk. (λt. t) x) and this is now in WHNF. Note that we do not reduce the application (λt. t) x because it is inside a λ.

---

to check if an expression is in WHNF you have to look at it as a syntactic tree. Let's consider the two examples above, and let's denote the application explicitly by $. Remember that the application f x y is equivalent to (f x) y.

In the first case the expression was:

                            |
              +-------------$-----------+
              |                         |
        +---- $ ----               +---(+)---+
        |          |               |         |
       λx         λt               6         7
        |          |
       λy       +-(+)-+
        |       |     |
    +---$---+   t     4
    |       |
    x       3

As you can see the root of the tree is a $, so we have to perform the application. In order to do this we must first reduce the left-hand side, which is again a $ so this must be reduced first, obtaining:

                            |
              +-------------$-----------+
              |                         |
              |                    +---(+)---+
              |                    |         |
              |                    6         7
              |          
             λy      
              |    
          +---$---+  
          |       |
         λt       3
          |
       +-(+)-+
       |     |
       t     4

Now on the left we have a λ so we can reduce the outermost application $:

              |
          +---$---+  
          |       |
         λt       3
          |
       +-(+)-+
       |     |
       t     4

And now the root is still a $ so we have to reduce that one too:

          |
       +-(+)-+
       |     |
       3     4

The root is a +, so we reduce again obtaining:

|
7

And now we are done.

In the second case we have the expression (λz . λk. ((λt. t) z)) x which becomes the tree:

             |
     +-------$-----------------+
     |                         |
     λz                        x
     |
     λk
     |
+----$----+
|         |
λt        z
|
t

Again the root is a $ so we have to reduce it:

     λk
     |
+----$----+
|         |
λt        x
|
t

Now we have a tree whose root is λ, and this means that the expression is in WHNF so we stop.