Lambda Calculus

• lambda calculus is a fully expressive (Turing complete) language of computable functions
• definition of $\lambda$-terms: $M ::=$$x | \lambda.x|MM$

  where x is a variable, $\lambda.x$ is an abstraction, MN is the application of function M to argument N .
• redex means reducible expression, which can be reduced within a term, ie $(\lambda x.M)N$
• free variable: a variable that is not bound to any other variable in the program

  bound variable: a variable that is used in a calculation but is not stored in memory
• alpha-conversion: how to rename variables

  This technique is used to avoid variable capture

  ie M[y/x] is “M with x renamed to y”
• $\beta$-reduction: Substitution of terms
• Proof by Induction

  (To prove that something ( P ) holds for every lambda-term N)

  1. Base case: P holds for x
  2. Inductive step 1: if P holds for N , then it holds for λx.N .
  3. Inductive step 2: prove it holds for MN
• Church’s thesis: A function of positive integers is computable if and only if lambda-definable
• Turing’s thesis: Something is computable if and only if a Turing Machine can compute it.
• Turing shows: Something is lambda-definable if and only if a Turing Machine can compute it
• True

  $true≜\lambda x.\lambda y.x, false≜\lambda x.\lambda y.y$
• if...then...else...

  $ifthenelse≜\lambda b. \lambda x. \lambda y. bxy$
• Conjunction (and): $\lambda b_1.\lambda b_2.ifthenelse$ $b_1b_2false$

  Disjunction (or): $\lambda b_1.\lambda b_2.ifthenelse$ $b_1true$$b_2$
• Church numerals:

  $0≜\lambda f.\lambda x.x$

  $1≜\lambda f.\lambda x.fx$

  $2≜\lambda f.\lambda x.f(fx)$

  ...
• successor

  $succ≜\lambda n.\lambda f.\lambda x.f(nfx)$
• preceder

  $pred≜\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)$
• fixed point for F is a λ-term M such that $M=$$_\beta FM$
• Y-combinator: $Y≜\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$
• multiply

  $mul≜\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x$
• exponentiation

  $exp≜\lambda m.\lambda n.\lambda f.\lambda x.nmfx$
• Y-combinator exploits self-application to deliver fixed points
• Types for λ-terms:

  $\tau ::=$$o | \tau \to \tau$


  o is a fixed type called the base case
• Types for λ-terms are right-associative
• simply-typed lambda-calculus:

  $M::=$$x|\lambda x^{\tau}.x|MM$
• computation of simply-typed lambda-calculus:

  $(\lambda x^{\tau}.M)N \to_{\beta} M[N/x]$
• A (typing) context Γ is a finite function from variables to types

  $\Gamma =$$x_1:\tau_1, x_2:\tau_2,..., x_n:\tau_n$
• By $\Gamma, x:\tau$ means the context that is the same as Γ, but extended so that x has type τ
• A (typing) judgement$\Gamma\vdash M:\tau$says that M has type τ in

  context Γ : “if each variable $x_i$ has type $\tau_i$ then M has type τ
• true typing judgements:

  1. $\over{\Gamma , x: \tau \vdash x: \tau}$
  2. ${\Gamma , x: \tau \vdash M: \sigma}\over{\Gamma , \lambda x^\tau.M: \tau \to\sigma}$
  3. ${\Gamma , M: \tau \to\sigma , \space\space\space\space\space\space\space\space\Gamma , M: \tau}\over{\Gamma , MN: \sigma}$
• A term M is well-typed if there is a true judgement Γ ⊢M : τ

  and all subterms of M are also well-typed
• addition

  $add≜\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$
• Proof by Induction(To prove that something ( P ) holds for every lambda-term N)

  1. Base case: P holds for any variable
  2. Inductive step 1: if P holds for N, then it holds for abstraction
  3. Inductive step 2: prove it holds for application
• transitive closure $\to_\beta ^ +$


  have at least one reduction step
• reflexive–transitive closure $\to_\beta ^ *$


  have reduction steps with zero or more
• reflexive–transitive–symmetric closure $=$$_R$


  reduction steps can go forward or backwards
• An equivalence (relation) or equational theory is a relation that is reflexive, symmetric, and transitive.
• alpha -equivalence : terms equivalent modulo variable names
• beta -equivalence : terms equivalent modulo computation
• A beta-expansion is a beta-reduction in reverse
• Terms M and N are α -equivalent, written M =α N , if N can be obtained from M by renaming bound variables.