Some Lambda Calculus Notes

some_lambda_calc_notes.mkd

Lambda Calculus

A programming language, with ONLY functions.

Consists of

• Name (kind of like a variable)
• Lambda functions (kind of like normal functions)
• Application (how we apply functions)

Terms:

• Name: a-z
• Lambda: λx.x
• Application: T1 T2

Examples

Identity function :)

Typically is called just I, defined as λx.x.

In c, this might look like the following

a I(a value) {
  return value;
}

In c, you'd apply it like this:

I(42);

In lambda calculus:

(λx.x) 42

You can think of this as reducing as follows

(λx.x) 42
(λ.42)
42

K === (λ x y . x)

Another example of application

(λxy.x) (λa.a) (λb.b)
(λy.(λa.a))  (λb.b)
(λ.(λa.a))
λa.a

Equality is interesting... λa.a ======== λb.b ========= λx.x

Tuples

Let's build (I, K)

(λx y z . z x y) I K
(λy z . z I y) K
(λz . z I K)

To access the first value you use K (λa b . a)

(λz . z I K) K
(λ. K I K)
K I K
(λa b . a) I K
(λb . I) K
(λ. I)
I

To access the second value you use `(λa b . b)`

READ THIS: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf


0 ≡ λs z . z
1 ≡ λs z . s(z)
2 ≡ λs z . s(s(z))
3 ≡ λs z . s(s(s(z)))

S = get the successor!

(λn . (λa b . a (n a b)))

(λn a b . a (n a b)) 0
(λa b . a ((λs z . z) a b))
(λa b . a (b))
(λa b . a(a(b)))


(λa b . a(a(b)))

N represented, actually is a special function that means apply
the function `a` `N` times against `b`

int factorial(int n) {
  if ...

  ...
  return n * factorial(n - 1);
}