Похоже, что в учебнике описываются Церковные логические значения . Это одна из возможных кодировок значений true и false.
Если вы не понимаете, что означает λ x y. x - это просто сокращение для λ x. λ y. x. Вот что происходит, когда вы применяете логические значения к некоторым переменным:
true a b = (λ x. λ y. x) a b = (λ y. a) b = a
false a b = (λ x. λ y. y) a b = (λ y. y) b = b
Итак, в основном, true кодируется как лямбда, которая принимает два параметра и выбирает первый, а false выбирает второй. .
Что касается того, почему ifelse определяется так, это помогает понять его предполагаемое использование:
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
Аналогично, ifelse false a b = b. Итак, f в его определении предполагается заменить на true или false.
Обратите внимание также на то, что ifelse на самом деле не делает ничего интересного. Это не обязательно, потому что логические значения уже определены таким образом, что ifelse c x y эквивалентно просто c x y. (концепция, связанная с этим наблюдением: эта-редукция , я думаю, в вашем учебнике это где-то упоминается)