{{ message }}

Instantly share code, notes, and snippets.

# brendanzab/lambda_calc.md

Created Apr 2, 2014

## 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₃
``````

``````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)
``````