> In math, "a = a + 1" isn't the same as "1 = 2". The issue isn't equality, it's that you're trying to rebind a bound variable, which isn't possible. "=" means

> In math, "a = a + 1" isn't the same as "1 = 2". The issue isn't equality, it's that you're trying to rebind a bound variable, which isn't possible. "=" means equality in math; a = a + 1 is the same as 1 = 2 because if you subtract a from both sides and add 1 to both sides you get 1 = 2. Lambda calculus has the concept of binding variables, but it doesn't use "=" for that, it uses application of lambda forms. It's the same idea that's applied in some variants of Lisp, where LET is a macro such that (let ((x 1) (y 2)) ...) expands to ((lambda (x y) ...) 1 2). The way it plays out is that rebinding is perfectly fine, because it's not really any different from binding in the first place. The same way that (let ((x 10)) (f x) (setf x (1+ x)) (g x)) can be re-written as ((lambda (x) (f x) (setf x (1+ x)) (g x)) 10) That can itself be re-written as: ((lambda (x) (f x) ((lambda (x) (g x)) (1+ x))) 10) If you'd like to read more about this sort of thing, Sussman and Steele's "Lambda: The Ultimate Imperative" is a good starter: http://repository.readscheme.org/ftp/papers/ai-lab-pubs/AIM-353.pdf http://repository.readscheme.org/ftp/papers/ai-lab-pubs/AIM-...