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.
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)