I'm working through Simon Peyton Jones' "The Implementation of Functional Programming Languages" and on page 20 I see:

IF TRUE ((λp.p) 3) ↔ IF TRUE 3         (per β red)   (1)
                   ↔ (λx.IF TRUE 3 x)  (per η red)   (2)
                   ↔ (λx.3)                          (3)

Step 1 to 2 is explained as η-conversion. But from 2 to 3 it says "The final step is the reduction rule for IF." I'm not sure what this reduction rule is.


The reduction rule you ask for is the usual one for IF statements. It consists of two computation rules and one context rule:

  • $\text{IF TRUE}$ $a$ $b$ $\to$ $a$

  • $\text{IF FALSE}$ $a$ $b$ $\to$ $b$

  • $\dfrac{a\to a'}{\text{IF}~a\ b\ c\to \text{IF}~a'\ b\ c}$

In both the call-by-value (strict) and call-by-need (lazy) settings, both $a$ and $b$ can be arbitrary expressions. They need not be values.

Rules of this kind, that reduce specific functions (here IF), are often called delta rules.

Now, the reason step (2) above is necessary is so that the reduction rules for $\text{IF}$ can apply. $\text{IF}$ requires 3 arguments, but in the original term it has only two, so cannot be reduced. ($\text{IF}$ is being partially applied, just like any function in Haskell. This means that only part of its arguments need to be supplied.) The use of $\eta$-expansion provides the additional argument, without changing the semantics.

  • 1
    $\begingroup$ I would add IF a b c -> IF a' b c with a-> a' $\endgroup$ – fabiofili2pi May 1 '12 at 12:18
  • $\begingroup$ Yes but should η-conversion not be adding conditions? It seems that going from IF TRUE 3 to λx.IF TRUE 3 x (excuse my omission of x on the original post) -- if then used in the next step as conforming to IF reduction -- is not exactly honest, because we added the x just to be the quasi ELSE half. For example, what if the problem been IF FALSE 3? Could we have η-conversion-ed it into λx.IF FALSE 3 x? Then step 3 would have been λx.x, which doesn't seem right... Odd, this. The point was to prove IF TRUE ((λp.p) 3) is equivalent to (λx.3) This has me confused. $\endgroup$ – galaxybeing May 1 '12 at 14:52
  • $\begingroup$ @galaxybeing: I've added a a comment regarding why you use $\eta$-expansion. Ultimately, it is so that IF has two arguments, and therefore its reduction rules can be applied. $\endgroup$ – Dave Clarke May 1 '12 at 15:35
  • $\begingroup$ @galaxybeing IF FALSE 3 is equivalent to \x -> IF FALSE 3 x (assuming partial application of IF is allowed). IF FALSE 3 needs one more argument to be reduced to a value; applying it to x yields IF FALSE 3 x, which reduces to simply x. So IF FALSE 3 is indeed equivalent to \x -> x, as long as we're using the untyped lambda calculus; if you try this out in Haskell (by defining a function if' :: Bool -> a -> a so you can partially apply it) then you get the id function specialised to whatever type Haskell infers for the 3. $\endgroup$ – Ben May 31 '12 at 0:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.