SELF_APPLY = Ls.(s s) (SELF_APPLY IDENTITY) (Ls.(s s) Lx.x) (Lx.x Lx.x) Lx.x (SELF_APPLY SELF_APPLY) (Ls.(s s) Ls.(s s)) (Ls.(s s) Ls.(s s)) (Ls.(s s) Ls.(s s)) (Ls.(s s) Ls.(s s)) Infinite loop in the lambda calculus APPLY = Lf.La.(f a) ((APPLY a) b) My intention here is to apply function a to argument b ((Lf.La.(f a) a) b) (La.(a a) b) (b b) <== which is not what I wanted alpha-renaming: In L. The after the L and all free occurrences of in can be replaced with provided that name2 is not free in L. Lx.x and Ly.y are the same function. When you are applying an expression to an existing function and you want to take care that the intention, just replace the bound with a new name not yet used. ((APPLY a) b) ((Lf.La.(f a) a) b) ((Lf.Lc.(f c) a) b) (Lc.(a c) b) (a b) ==> which is I want: applying function a to argument b SELECT_FIRST = Lx.Ly.x SELECT_SECOND = Lx.Ly.y ((SELECT_FIRST arg1) arg2) ((Lx.Ly.x arg1) arg2) (Ly.arg1 arg2) arg1 ((SELECT_SECOND arg1) arg2) ((Lx.Ly.y arg1) arg2) (Ly.y arg2) arg2 MAKE_PAIR = Lx.Ly.Lf.((f x) y) //this corresponds the ordered pair (x,y) in math. ((MAKE_PAIR arg1) arg2) ((Lx.Ly.Lf.((f x) y) arg1) arg2) (Ly.Lf.((f arg1) y) arg2) Lf.((f arg1) arg2) (((MAKE_PAIR arg1) arg2) SELECT_FIRST) (Lf.((f arg1) arg2) SELECT_FIRST) ((SELECT_FIRST arg1) arg2) arg1 Applying MAKE_PAIR to SELECT_SECOND would give you arg2. This is an ordered pair. Applying the order to SELECT_FIRST or SELECT_SECOND will give the first or second value in there. TRUE = SELECT_FIRST FALSE = SELECT_SECOND COND = Le1.Le2.Lc.((c e1) e2) You can think of c as a "boolean" but of course c is a function because everything is. (((COND e1) e2) TRUE) (((Le1.Le2.Lc.((c e1) e2) e1) e2) TRUE) ((Le2.Lc.((c e1) e2) e2) TRUE) (Lc.((c e1) e2) TRUE) ((TRUE e1) e2) ((SELECT_FIRST e1) e2) (((COND e1) e2) TRUE) evaluates to e1 (((COND e1) e2) FALSE) evaluates to e2 This is why we chose SELECT_FIRST and SELECT_SECOND to be TRUE and FALSE. So that we that we can choose which of the two expressions we want. So, we've just written ?: the ternary operator in lambda calculus. NOT = Lx.((x FALSE) TRUE) (NOT TRUE) = (NOT SELECT_FIRST) = ( (SELECT_FIRST FALSE) TRUE) = FALSE (NOT FALSE) = (NOT SELECT_SECOND) = ((SELECT_SECOND FALSE) TRUE) = TRUE AND = Lx.Ly.((x y) FALSE) OR = Lx.Ly.(x TRUE) y) Notice how AND words. if x is FALSE, then the SELECT_SECOND guarantees us an answer of FALSE. if x is TRUE, the answer is whatever y is. In OR, if x is TRUE, then the OR is TRUE, the SELECT_FIRST will choose the TRUE. If x is FALSE, then the OR is whatever the Y is.