Search code examples
functional-programminglambda-calculus

How to understand the boolean expression in lambda expression?


In the textbook, this is the expression of "True": λxy.x, so what's that mean? (do I need to replace x or y?). And the "IFELSE" expression: λfxy.fxy, I have no idea what is f and how to understand this expression.


Solution

  • It seems like the textbook is describing Church Booleans. They are one of the possible encodings of the values true and false.

    If you are confused about what λ x y. x means - this is simply a shorthand for λ x. λ y. x. Here's what happens when you apply the booleans to some variables:

    true a b = (λ x. λ y. x) a b = (λ y. a) b = a
    false a b = (λ x. λ y. y) a b = (λ y. y) b = b
    

    So, basically, true is encoded as a lambda taking two parameters and selecting the first one, and false selects the second one.

    As for why ifelse is defined like that, it helps to look at its intended usage:

    ifelse true a b = (λ f. λ x. λ y. f x y) (λ x'. λ y'. x') a b =
    = (λ x. λ y. (λ x'. λ y'. x') x y) a b = (λ y. (λ x'. λ y'. x') a y) b =
    = (λ x'. λ y'. x') a b = ... = a
    

    Similarly, ifelse false a b = b. So, the f in its definition is supposed to be substituted with either true or false.

    Notice also how ifelse does not actually do anything interesting. It does not have to, because the booleans are already defined in such a way that ifelse c x y is equivalent to just c x y. (a concept related to this observation is eta-reduction, I believe your textbook mentions this somewhere)