SU-CS242 OCT032024 — Jemoka Knowledge Base

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) - \left\{x\right\} 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 Lambda Calculus 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 | 0 we 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 numbers