lpetrich
Contributor
I was inspired by this video: Lambda Calculus - Computerphile - YouTube - YouTube
It was invented by mathematician Alonzo Church in his investigations into the foundations of mathematics. Its name comes from the Greek letter λ commonly used in writing expressions in it. I'll use L for convenience. It essentially expresses everything as a function:
f(x) = operations on x
f = Lx.(operations on x)
The possible valid return values of a function are defined recursively:
(Valid return value) = (a variable) or (a function of valid return values)
Thus, one can do a function of a function of a function... though it must be a finite number of function evaluations.
Multiple arguments can be expressed similarly:
f(x,y) ... f = Lx.Ly. ... f = Lxy
Multiple-argument functions can be expressed as a chain of single-argument functions that get data from their surroundings, a process called currying.
Much of that video discussed the lambda calculus rather abstractly, but a later part of it introduced some definitions of some boolean operations: true, false, not. Alonzo Church himself showed that one can define true and false in the lambda calculus by treating them as if-then-else evaluations:
TRUE = Lx.Ly.x
FALSE = Lx.Ly.y
or
TRUE(x,y) = x
FALSE(x,y) = y
What makes the lambda calculus mathematically useful is the ability to pass functions to functions. That enables us to define "NOT"
NOT = Lp.p FALSE TRUE
NOT(p) = p(FALSE,TRUE)
It should be easy to show that NOT(TRUE) = FALSE and NOT(FALSE) = TRUE.
One can continue with more Boolean-algebra operations:
AND = Lp.Lq.p q p
OR = Lp.Lq.p p q
XOR = Lp.Lq.p (NOT q) q
EQUIV = Lp.Lq.p q (NOT q)
IMPLIES = Lp.Lq.OR (NOT p) q
IFTHENELSE = Lp.Lx.Ly.p x y
It was invented by mathematician Alonzo Church in his investigations into the foundations of mathematics. Its name comes from the Greek letter λ commonly used in writing expressions in it. I'll use L for convenience. It essentially expresses everything as a function:
f(x) = operations on x
f = Lx.(operations on x)
The possible valid return values of a function are defined recursively:
(Valid return value) = (a variable) or (a function of valid return values)
Thus, one can do a function of a function of a function... though it must be a finite number of function evaluations.
Multiple arguments can be expressed similarly:
f(x,y) ... f = Lx.Ly. ... f = Lxy
Multiple-argument functions can be expressed as a chain of single-argument functions that get data from their surroundings, a process called currying.
Much of that video discussed the lambda calculus rather abstractly, but a later part of it introduced some definitions of some boolean operations: true, false, not. Alonzo Church himself showed that one can define true and false in the lambda calculus by treating them as if-then-else evaluations:
TRUE = Lx.Ly.x
FALSE = Lx.Ly.y
or
TRUE(x,y) = x
FALSE(x,y) = y
What makes the lambda calculus mathematically useful is the ability to pass functions to functions. That enables us to define "NOT"
NOT = Lp.p FALSE TRUE
NOT(p) = p(FALSE,TRUE)
It should be easy to show that NOT(TRUE) = FALSE and NOT(FALSE) = TRUE.
One can continue with more Boolean-algebra operations:
AND = Lp.Lq.p q p
OR = Lp.Lq.p p q
XOR = Lp.Lq.p (NOT q) q
EQUIV = Lp.Lq.p q (NOT q)
IMPLIES = Lp.Lq.OR (NOT p) q
IFTHENELSE = Lp.Lx.Ly.p x y