Skip to content

Lambda calculus

Lambda calculus

“Church” notation

overview:

λ input . output(s)\lambda~input~.~output(s)

an increment function:

λx.x+1\lambda x.x+1

a sum function (note that this takes two inputs):

λx.λy.x+y\lambda x.\lambda y.x+y

demonstration of increment function:

(λx.x+1) 5  λ5.5+1  6 (\lambda x.x+1)~5\\ \rarr~~ \lambda 5.5+1\\ \rarr~~ 6

encoding “true” and “false”:

True   λx.λy.xFalse   λx.λy.yTrue ~\rarr~~ \lambda x.\lambda y.x\\ False ~\rarr~~ \lambda x.\lambda y.y

“not” operator (note, FALSE and TRUE are outputs):

λb.b  FALSE  TRUE\lambda b.b ~~FALSE~~TRUE

applying the “not” operator to TRUE:

(λb.b  FALSE  TRUE)  TRUE(\lambda b.b ~~FALSE~~TRUE) ~~TRUE

  λ(λx.λy.x).λx.λy.x  FALSE  TRUE\rarr ~~\lambda (\lambda x.\lambda y.x).\lambda x.\lambda y.x ~~FALSE~~TRUE

  FALSE\rarr ~~FALSE