There is very much an "if-statement" in lambda calculus. The basic idea is, in the Church Booleans, we think of true as a function which takes a then clause an

There is very much an "if-statement" in lambda calculus. The basic idea is, in the Church Booleans, we think of true as a function which takes a then clause and an else clause, and returns the then clause (T=\lambda xy.x), and false as a function which takes a then clause and an else clause and returns the else clause (F=\lambda x y.y). Then we get our if statement just by applying a predicate (which returns F or T) to a then clause and an else clause. Indeed, that is very much a way to get recursion to step -- the typical Church-numeral definition of the factorial function works that way. By the way, one sure-fire way to get evaluation of a lambda expression to terminate if possible is leftmost-reduction -- that is, reducing the leftmost redex first. Intuitively, the leftmost redex is the "outermost," and any other reduction preserves it, so it must be reduced at some point.