lambda_calc.md

Introducing the lambda calculus

λx. t

This could be expressed in a 'hypothetical conventional language' as:

fn(x) { t }

Multiple arguments

Lambda functions can only technically take one argument, but they can be curried to provide the same functionality:

λx.λy. t

This could be expressed in our hypothetical language as:

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

Church Booleans

Booleans can be defined as the following functions:

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. b fls tru

   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

Church Numerals

The natural numbers can be represented by applying a successor function s multiple times to a zero function z.

c₀ = λs.λz. z
c₁ = λs.λz. s z
c₂ = λs.λz. s (s z)
c₃ = λs.λz. s (s (s z))
...

It is interesting to note that the definition of c₀ is the same as the definition of fls.

Successor function

We can form a successor function scc by adding an additional application of s to a number n:

scc = λn.λs.λz. s (n s z)

Here is a demonstration of how scc c₂ evaluates to its successor, c₃:

   scc c₂
=  (λn.λs.λz. s (n s z)) c₂
-> λs.λz. s (c₂ s z)
=  λs.λz. s ((λs.λz. s (s z)) s z)
-> λs.λz. s (s (s z)))
=  c₃

Addition

add = λm.λn.λs.λz. m s (n s z)

You can think of this like dopping replacing z at the end of m with the number n.

   add c₂ c₁
=  (λm.λn.λs.λz. m s (n s z)) c₂ c₁
-> (λn.λs.λz. c₂ s (n s z)) c₁
-> λs.λz. c₂ s (c₁ s z)
=  λs.λz. (λs.λz. s (s z)) s ((λs.λz. s z) s z)
-> λs.λz. (λs.λz. s (s z)) s (s z)
-> λs.λz. s (s (s z))
=  c₃

Multiplication

   mul = λm.λn.λs.λz. m (add n) c₀

Here we apply add n an m number of times to c₀ to obtain the product.

   mul c₃ c₂
=  (λm.λn.λs.λz. m (add n) c₀) c₃ c₂
-> λs.λz. c₃ (add c₂) c₀

Semantics

TaPL, Figure 5.3:

Syntax

t   ::=                 terms:
        x               variable
        λx. t           abstraction
        t t             application

v   ::=                 values:
        λx. t           abstraction value

Evaluation

    t₀ ⟶ t'₀
─────────────────── (T-App1)
 t₀ t₁ ⟶ t'₀ t₁

    t₁ ⟶ t'₁
─────────────────── (T-App2)
 v₀ t₁ ⟶ v₀ t'₁

(λx. t₀₁)v₁ ⟶ [x ⟼ v₁]t₀₁  (E-AppAbs)