Lambda calculus

Lambda calculus was invented by Alonzo Church

Lambda calculus concerns the nature of a function from a computational perspective
 “what is a function, from a computational perspective?”

Analogous to Turing’s state machine, except functional (not statebased)
 any Turing machine program can be converted into a lambda calculus program

A function is a small machine that takes an input, processes it, and produces an output

Functions are “black boxes”, so we don’t know or care about what happens inside, just what goes in and comes out

Functions are pure, so they have no internal state or side effects, simply producing an output from an input
“Church” notation
; overview:
λ<input>.<output(s)>
; an increment function:
λx.x+1
; a sum function (note that this takes two inputs):
λx.λy.x+y
; demonstration of increment function:
(λx.x+1) 5
=> λ5.5+1
=> 6
; encoding "true" and "false":
TRUE = λx.λy.x
FALSE = λx.λy.y
; "not" operator (note, `FALSE` and `TRUE` are outputs):
λb.b FALSE TRUE
; applying the "not" operator to TRUE:
(λb.b FALSE TRUE) TRUE
; expanded:
=> λ(λx.λy.x).λx.λy.x FALSE TRUE
; result:
=> FALSE

These definitions of true and false functions represent the concept of choosing between one thing and another

They can be used to implement all of the logical operators, not just the “not” operator

The most popular lambda calculus expression is the “Y combinator”
 invented by Haskell Curry
 a way to implement recursion in lambda calculus