Lambda Calculus
Like SKI Calculus, its a language of functions; unlike SKI Calculus, there are variables.
\begin{equation} e\to x \mid \lambda x.e \mid ee \mid (e) \end{equation}
meaning, we have:
- a variable \(x\)
- an abstraction \(\lambda x . e\) (a function definition)
- an application \(e_1 e_2\)
we call \((\lambda x . e)e’\) (a function and its argument, ready for reduction) a redex.
abstraction
def f(x) = e
can be written as:
\begin{equation} \lambda x.e \end{equation}
this is just an anonymous function—it can be returned, etc.
syntax
Association to the left: \(f x y z = ((f(x))y)z\). An lambda abstraction extends as far right as possible:
\begin{equation} \lambda x.x \lambda y.y \to \lambda x.(x \lambda y . y) \end{equation}
substitution
variables requires us being able to substitute things.
- \(x [x:=e] = e\) — similar to \(I\)
- \(y [x:=e] = y\) — similar to \(K\)
- \((e_1 e_2) [x := e] = (e_1 [x:= e]) (e_2 [x:= e])\) — similar to \(S\)
- \((\lambda x . e_1) [x := e] = \lambda x . e_1\) — shadowing; that is, during a function application if shadowing occurs, we don’t use substitution
- \((\lambda y . e_1) [x:= e] = \lambda y . (e_1 [x:= e])\), if \(x \neq y\) and \(y\not \in FV(e)\); that is, we can only substitute if the contents of our substitution is not going to be changed by new variable bindings
- if we got caught by this rule, use an alpha reduction
the last rule?!
\((\lambda y . e_1) [x:= e] = \lambda y . (e_1 [x:= e])\), if \(x \neq y\) and \(y\) doesn’t appear free in \(e\)
Consider:
\begin{equation} (\lambda y . x) [x:= y] \end{equation}
it would not make sense to substitute \(x\) inside the function for \(y\).
free variables
The free variables are variables not bound in an application:
- \(FV(x) = \{x\}\)
- \(FV(e_1 e_2) = FV(e_1) \cup FV(e_2)\)
- \(FV(\lambda x.e) = FV(e) - \qty {x}\)
reductions
we can mostly ignore alpha reduction and eta reduction be rephrasing as “rename variables to avoid collision whenever needed”.
beta reduction
\((\lambda x.e_1)e_2 \to e_1[x:=e_2]\), we replace every occurrence of \(x\) in \(e_1\) with \(e_2\); we call \(x\) the formal parameter, and \(e_2\) the actual argument
alpha reduction
we can rename variables to avoid collision; \(\lambda x. e = \lambda z . e [x := z]\), with a fresh \(z\) (to avoid conflicting variables).
eta reduction
\(e = \lambda x . e x\), \(x \not \in FV(e)\)
evaluation order
- call-by-name (for correct termination): evaluate the arguments only when the function can be reduced
- call-by-value (more efficient): it evaluates the arguments one time (even if the function makes copies of the arguments, we don’t evaluate it again)
Church-Rosser Theorem
programming time
non terminating expression
\begin{equation} (\lambda x . x x) (\lambda x . x x) = (\lambda x . x x) (\lambda x . x x) \end{equation}
y-combinator
\begin{equation} Y = \lambda f . (\lambda x . f (x x)) (\lambda x . f ( x x)) \end{equation}
let’s do it a few times:
\begin{equation} Y g a \to (\lambda x . g (x x)) (\lambda x g ( x x)) a \to g ((\lambda x g ( x x)) (\lambda x g ( x x))) a \end{equation}
booleans
- \(True\ x\ y = x\)
- \(False \ x\ y = y\)
to abstract this to combinators, we just put \(\lambda\) in front of each argument and we are done:
- \(True= \lambda x . \lambda y. x\)
- \(False = \lambda x. \lambda y .y\)
we can recycle the combinator-based definitions for SKI to deal with the rest of the boolean logic: conditionals
pairs
- \(pair = \lambda a. \lambda b . \lambda f . f a b\)
- \(fst = \lambda x. \lambda y. x\)
- \(snd = \lambda x. \lambda y. y\)
numbers
- \(0 f x = x\), so \(0 = \lambda f . \lambda x . x\)
- \(succ\ n\ f\ x = f(nfx)\), so \(succ = \lambda n . \lambda f . \lambda x. f (n f x)\)
factorial
p = λp. pair (mul (p fst) (p snd)) (succ (p snd)) ! = λn.(n p (pair one one) fst)
Algebraic Data Type
Type T = constructor1 Type11 Type12 ... Type1n |
constructor2 Type21 Type22 ... Type 2m |
...
- algebraic: because the constructor packages up the arguments
- the constructor is a “tad” naming the case of the ADT being used
- deconstructors recovers the arguments of the constructor to use it
Type List = nil |
cons Nat List
encoding ADTs in lambda calculus
Consider an ADT \(T\) with \(n\) constructors; let each constructor have \(k\) arguments; so—here’s an example constructor:
\begin{equation} \lambda a_1 . \lambda a_2 \dots \lambda a_{k}. \lambda f_1 . \lambda f_2 \dots \lambda f_{n} f_i a_1 a_2 \dots a_{k} \end{equation}
each constructor must have \(n\)
natural numbers
Type Nat = succ Nat | 0we have two constructors—
\begin{equation} succ = \lambda n . \lambda f. \lambda x. f(n f x) \end{equation}
\begin{equation} 0 = \lambda f . \lambda x. x \end{equation}
examples
- identity \(I\): \(\lambda x . x\)
- constant \(K\): \(\lambda z . \lambda y . z\)