lambda-calc.md

Introducing the lambda calculus

The following function:

fn(x) { t }

can be written using this weird notation devised by Church in the 40s:

λx. t

where:

- `x` is an argument
- `t` represents a 'term' that will be returned

Multiple arguments

The lambda calculus has no notion of multiple arguments. Hence we use currying:

fn(x) {
    fn(y) { t }
}

This can be written like:

λx.λy. t

Church Booleans

Booleans can be defined as the following terms:

tru = λt.λf. t
fls = λt.λf. f

These definitions may look strange at first, but they begin to make sense after we define some logical operators:

And

and = λb.λc. b c fls

   and tru tru
=  (λb.λc. b c fls) tru tru
-> (λc. tru c fls) tru
-> tru tru fls
=  (λt.λf. t) tru fls
-> (λf. tru) fls
-> tru

and tru tru -> (λb.λc. b c fls) tru tru -> tru tru fls -> tru
and tru fls -> (λb.λc. b c fls) tru fls -> tru fls fls -> fls
and fls tru -> (λb.λc. b c fls) fls tru -> fls tru fls -> fls
and fls fls -> (λb.λc. b c fls) fls fls -> fls fls fls -> fls

Or

or = λb.λc. b tru c

   or tru fls
=  (λb.λc. b tru c) tru fls
-> (λc. tru tru c) fls
-> tru tru fls
=  (λt.λf. t) tru fls
-> (λf. tru) fls
-> fls

or tru tru -> (λb.λc. b tru c) tru tru -> tru tru tru -> tru
or tru fls -> (λb.λc. b tru c) tru fls -> tru tru fls -> tru
or fls tru -> (λb.λc. b tru c) fls tru -> fls tru tru -> tru
or fls fls -> (λb.λc. b tru c) fls fls -> fls tru fls -> fls

Not

not = λb.λc. b c fls

   not fls
=  (λb. b fls tru) fls
-> fls fls tru
=  (λt.λf. f) fls tru
-> (λf. f) tru
-> tru

not tru -> (λb. b fls tru) tru -> tru fls tru -> fls
not fls -> (λb. b fls tru) fls -> fls fls tru -> tru