Lambda Calculus

Untyped Lambda Calculus

• :
  • start with a (infinite) set of variables $\mathcal{V} = {a, b, c, ...}$
  • $\lambda$-Calculus is a set of terms formed according to these three rules
    • 1. naming :: if $x \in \mathcal{V}$, then $x$ is a term in the $\lambda$-Calculus
    • 2. abstraction :: if $T$ is a term and $x \in \mathcal{V}$, then $\lambda x. T$ is a term
    • 3. application :: if $T_1$ and $T_2$ are terms, then $T_1 T_2$ is a term
• it’s a model for general computation
• application and term rewriting:
  • for $T_1 T_2$, when $T_1$ is an abstraction, we allow re-write applications by substituting $T_2$ for $x$ through $T_1$
  • eg for abstraction select-first, $\lambda x. \lambda y. x$, its application is like
    • $(\lambda x. \lambda y. x\ a)\ b \to$
    • $(\lambda y. a)\ b \to$
    • $a$
• eg: make-pair $\lambda x. \lambda y. \lambda z\ ((z\ x)\ y)$
  • when applies to $a$ and $b$
  • we got: $\lambda z\ ((z\ a)\ b)$
  • its a term that encodes $a$ and $b$
  • it expects an abstraction
• Alpha Equivalence: free and bound variables
  • : bound variables are “placeholders” that can be re-named at will without changing the essential meaning of a term.
  • in a term, there are 3 categories of variable occurrences
    • 1. binding: on the left side of $.$ in an abstraction
    • 2. bound
    • 3. free: in $\lambda x. M$, $x$ is bound in $M$
  • rules: …
  • it allows $\lambda x. (x\ \lambda x. x)\ y$ to make sense: inner $x$ and outer $x$ are different
  • the operation of renaming: $M^{x \to y}$ denotes the result of replacing every free occurrence of $x$ in $M$ with $y$
• Beta Reduction
  • : the process of applying a function (an abstraction) to an argument (another term)
  • $(\lambda x. M)\ N$ is called a redex (reducible expression)
  • rule
    • : substitute every occurrence of the bound variable $x$ inside the function body $M$ with the argument $N$
    • notation for substitution: $M[x := N]$
    • the rule can be written as $(\lambda x. M)\ N \to_{\beta} M[x := N]$
• $\beta$-normal: when is $\beta$-reduction done?
  • We say that a term $M$ is in $\beta$-normal form ($\beta$-nf) if $M$ contains no redex, ie, there’s no way to perform beta-reduction to reduce it to a simpler form

Simply Typed Lambda Calculus $\lambda_{\to}$

• :
  • in addition to ordinary variables $\mathcal{V}$ in untyped lambda calculus, we now have another set of type variables $\mathbb{V} = {\alpha, \beta, \gamma, ...}$, and we can define the set of all simple types $\mathbb{T}$ as:
    • 1. if $\alpha \in \mathbb{V}$, then $\alpha \in \mathbb{T}$
    • 2. if $\alpha, \tau \in \mathbb{V}$, then $\alpha \to \tau \in \mathbb{T}$
  • we write $M: \sigma$ for “term $M$ has type $\sigma$”
  • we assume each ordinary variable has an unique type
  • we denote abstraction more fully as $\lambda x: \sigma. M: \sigma \to \tau$
• context: a collection of type statements $x: \sigma$, $y: \tau$, $z: \upsilon$
• judgement: a statement $\Gamma \vdash M: \sigma$, where they are a context, a term, and a type respectively
• derivation
  • : we can validate a judgement by derivation
  • 3 derivation rules
    • 1. var: $\Gamma \vdash x : \sigma$ if $x : \sigma \in \Gamma$
    • 2. appl: $\frac{\Gamma \vdash M: \sigma \to \tau \Gamma \vdash N: \sigma}{\Gamma \vdash MN : \tau}$
    • 3. abst: $\frac{\Gamma, x: \sigma \vdash M : \tau}{\Gamma \vdash \lambda x: \sigma. M: \sigma \to \tau}$
  • Each rule tells us what we can conclude so long as we know certain things
  • A derivation is collection of applications of these rules, arranged in an inverted tree where the “root”, at the bottom, is the statement we are justifying.
• Questions we can ask now:
  • 1. well-typedness / typability: given a term, is it legal in some context?
  • 2. type checking: given a judgement, is it true?
  • 3. term finding: is there a term of the given type in the given context?
    • previous 2 are decidable, this one is undecidable
    • under Curry-Howard, term finding is equivalent to proof finding
• We can now rule out misbehaving terms. All terms are strongly normalizing as their reduction to normal form is guaranteed to terminate.
  • downside: it’s not very expressive

Second-order Lambda Calculus - $\lambda 2$ - Polymorphic Lambda Calculus - System F

• All above names are referring to the same thing
• $\land$

Reference

• https://www.unwoundstack.com/blog/the-lambda-calculus.html
• https://www.unwoundstack.com/blog/the-simply-typed-lambda-calculus.html