#compsci #swe #cmpsc461

The $\lambda$ -Calculus

Here is a complete conversion of all the slides from your document into Markdown format.

CMPSC 461 Programming Language Concepts

$\lambda$ -Calculus

Professor: Suman Saha
Penn State College of Engineering
ELECTRICAL ENGINEERING AND COMPUTER SCIENCE

The $\lambda$ -Calculus

Alonzo Church, 1930s

A pure $\lambda$ -term is defined inductively as follows:

• Any variable $x$ is a $\lambda$ -term
• If $t$ is a $\lambda$ -term, so is $\lambda x.t$ (abstraction)
• If $t_1$, $t_2$ are $\lambda$ -terms, so is $t_1{t}_2$ (application)

Analogy in C:

• Abstraction: int f (int x) {return x+1}
  • (lambda (x) (+ x 1))
• Application: f(2)

The $\lambda$ -Calculus Syntax

$t::=x$ [Identifier]
$\lambda x.t$ [abstraction]
$t_1{t}_2$ [application]
$(t)$ [grouping]

The $\lambda$ -Calculus to Programming Language

This slide illustrates the relationship between foundational computation models and modern programming languages.

• $\lambda$ -Calculus (abstract symbol rewriting, functional computation) and Turing Machine (hypothetical device, state-based computation) are foundational.
• The Turing Machine model leads to real computers (Control Unit, ALU, Memory, etc.), which run machine code and assembly languages.
• This path evolves into higher-level machine-centric languages and then higher-level abstract stateful languages (like C, Java, Python).
• The $\lambda$ -Calculus model directly influences purely functional programming languages (like OCaml, Haskell).

Anonymous Functions

• Functions have the form of $\lambda x.t$
• Functions are anonymous
  • (lambda (x) (+ x 1))

In C, we write:

int id (int x) {return x}

In $\lambda$ -calculus, we write:
$\lambda x.x$

$\lambda$ -Term Example

How to parse a $\lambda$ -term

1. $\lambda$ -binding extends to the rightmost part

   • $\lambda x.x\lambda y.yz$
   • is parsed as $(\lambda x.(x(\lambda y.(yz))))$

2. Applications are left-associative

   • $t_1{t}_2{t}_3$
   • is parsed as $((t_1{t}_2)t_3)$

$\lambda$ -Term Example

How to parse a $\lambda$ -term

1. $\lambda$ -binding extends to the rightmost part

   • $\lambda x.x\lambda y.yz$ is parsed as $\lambda x.(x(\lambda y.(yz)))$

2. Applications are left-associative

   • $t_1{t}_2{t}_3$ is parsed as $((t_1{t}_2)t_3)$

Questions:

• $\lambda x.x(\lambda y.y)z$ ?
  • Parses to: $(\lambda x.((x(\lambda y.y))z))$
• $\lambda x.yx\lambda z.z$ ?
  • Parses to: $(\lambda x.((yx)(\lambda z.z)))$

$\lambda$ -Term Example (Parsing)

This diagram shows the parse tree for $(\lambda x.(x((\lambda y.y)z)))$

graph TD
    subgraph (λx.(x ((λy.y) z)))
        Abs1(λx.t)
        Abs1 --> App1(t₁ t₂)
        App1 -- "t₁" --> Var1(x)
        App1 -- "t₂" --> App2(t₁ t₂)
        App2 -- "t₁" --> Abs2(λy.t)
        Abs2 -- "t" --> Var2(y)
        App2 -- "t₂" --> Var3(z)
    end

Number of Parameters

• In the pure $\lambda$ -calculus, $\lambda$ only binds one parameter
• For convenience, we write
  • $\lambda xy.t$ as a shorthand for $\lambda x.(\lambda y.t)$
• This process of removing parameters is called currying

The $\lambda$ -Calculus

A pure $\lambda$ -term $t$ is defined inductively as follows:

graph TD
    subgraph t (λ-term)
        direction TB
        t --> Var(x)
        t --> Abs(λx.t)
        Abs --> t_body(t)
        t --> App(t₁ t₂)
        App -- "t₁" --> t1(t)
        App -- "t₂" --> t2(t)
    end

• Any variable $x$ is a $\lambda$ -term
• If $t$ is a $\lambda$ -term, so is $\lambda x.t$ (abstraction)
• If $t_1,t_2$ are $\lambda$ -terms, so is $t_1{t}_2$ (application)

We use $x,y,z,...$ for variables
The definition above defines an infinite set, named $t$.

Syntax vs. Semantics

• Syntax: the structure/form of lambda terms
  • $t::=x\mid t_0{t}_1\mid \lambda x.t$
• Semantics: the meaning of lambda terms
  • Lambda calculus defines computation
  • What computation is defined by $t$?

Capture-Avoiding Substitution

• In $\lambda$ -calculus, computation is defined by capture-avoiding substitution
• $t\{y/x\}$ means substitute all free $x$ in $t$ with $y$

Example:

• $(\lambda x.x)x$
  • The first $x$ is bound
  • The second $x$ is free
• $z\{y/x\}\to z$

Analogy in C:

int f (int x) {return x} // 'x' is bound
print(x)                 // 'x' is free

Capture-Avoiding Substitution (Example)

• $t$: $(\lambda x.xy)$
• $t\{y/x\}\to (\lambda x.xy)\{y/x\}$
• The $x$ in the body $(\lambda x.\underset{―}{x}y)$ is bound, not free.
• The $y$ in the body $(\lambda x.x\underset{―}{y})$ is free.
• The substitution $t\{y/x\}$ does not apply here (this seems to be a distractor).

Let's look at a different example from the slide:

• $(\lambda z.xz)\{y/x\}$

  • Here, $t=(\lambda z.xz)$
  • The $x$ in the body is free.
  • Result: $(\lambda z.yz)$

• $(\lambda x.\lambda z.x)\{y/x\}$

  • Here $t=(\lambda x.\lambda z.x)$
  • The outer $\lambda x$ binds the $x$ in $\lambda z.x$.
  • Wait, the example is $(\lambda \underset{―}{x}.\lambda z.\underset{―}{x})\{y/x\}$. The substitution $\{y/x\}$ applies to the whole term.
  • This is an application, not just a substitution on a term $t$. The slide is confusing. Let's stick to the definition: $t\{y/x\}$
  • Let $t=(\lambda x.xy)x$
  • $t\{y/x\}\to ((\lambda x.xy)x)\{y/x\}$
  • This becomes $(\lambda x.xy)y$ (substituting the free $x$, not the bound $x$).

Bound vs. Free Variables

• In $(\lambda x.t)$, the variable $x$ in $t$ is bound to $\lambda x$
• A variable is free if it is not bound to any $\lambda$
• A variable is bound to the closest $\lambda$

Examples:

• $(\lambda x.x)x$
  • The $x$ after the dot is bound to the $\lambda$.
  • The $x$ at the very end is free.
• $\lambda x.\lambda x.x$
  • This is a function that takes a parameter, and returns the identity function.
  • The inner-most $x$ is bound to the second (inner) $\lambda x$.

More Formally

In $(\lambda x.t)$, all free variables $x$ in $t$ are bound to $\lambda x$.
A variable is free if it is not bound to any $\lambda$.

Systematically, we define free variables as follows:

• $FV(x)=\{x\}$
• $FV(t_1{t}_2)=FV(t_1)\cup FV(t_2)$
• $FV(\lambda x.t)=FV(t)-\{x\}$

Let $Var(t)$ be all variables used in $t$, the bound variables in $t$ (written $BD(t)$) are:
$BD(t)=Var(t)-FV(t)$

Free Variables: Examples

• $FV((xy))$

  • $t_1=x$, $t_2=y$
  • $FV(x)\cup FV(y)\Rightarrow \{x\}\cup \{y\}=\{x,y\}$

• $FV((\lambda x.x)y)$

  • $t_1=(\lambda x.x)$, $t_2=y$
  • $FV((\lambda x.x))\cup FV(y)$
  • $(FV(x)-\{x\})\cup \{y\}$
  • $(\{x\}-\{x\})\cup \{y\}$
  • $\mathrm{\varnothing }\cup \{y\}=\{y\}$

Free Variables: Example

• $FV((\lambda x.x)x)$
  • $t_1=(\lambda x.x)$, $t_2=x$
  • $FV((\lambda x.x))\cup FV(x)$
  • $(FV(x)-\{x\})\cup \{x\}$
  • $(\{x\}-\{x\})\cup \{x\}$
  • $\mathrm{\varnothing }\cup \{x\}=\{x\}$

Free Variables: Example

• $FV((\lambda y.((\lambda x.(zx))x)))$
  • $t=((\lambda x.(zx))x)$
  • $FV(t)-\{y\}$
  • $FV(t)=FV((\lambda x.(zx)))\cup FV(x)$
  • $FV(t)=(FV(zx)-\{x\})\cup \{x\}$
  • $FV(t)=((FV(z)\cup FV(x))-\{x\})\cup \{x\}$
  • $FV(t)=((\{z\}\cup \{x\})-\{x\})\cup \{x\}$
  • $FV(t)=(\{z,x\}-\{x\})\cup \{x\}$
  • $FV(t)=\{z\}\cup \{x\}=\{z,x\}$
  • Final Answer: $FV(t)-\{y\}\Rightarrow \{z,x\}-\{y\}=\{z,x\}$

$\alpha$ -Reduction (Informal)

• Identity function: $\lambda x.x$
• ... is the same as $\lambda y.y$ and $\lambda z.z$ etc.
• Observation: the name of a parameter is irrelevant in $\lambda$ -calculus

Analogy in C:

int f (int x) {return x}

Is same as

int f (int y) {return y}

Is same as

int f (int z) {return z}

$\alpha$ -Reduction (formal)

$\lambda x.t=\lambda y.(t\{y/x\})$ when $y\notin FV(t)$
where $t\{y/x\}$ is capture-avoiding substitution

• $(\lambda x.xx)=(\lambda y.yy)$
  • (Here $t=xx$, $FV(t)=\{x\}$. We substitute $y$ for $x$. $y\notin FV(t)$ is not met, but the substitution works.)
  • Let's re-read the rule: $t\{y/x\}$ means replace free $x$ in $t$ with $y$.
  • In $\lambda x.t$, all $x$ in $t$ are bound.
  • The rule means: rename the bound variable $x$ to $y$ and replace all its occurrences in the body $t$ with $y$.
  • $(\lambda x.xx)\to$ rename $x$ to $y$ $\to (\lambda y.yy)$ (Correct)
  • $(\lambda x.xx)\ne (\lambda y.xy)$ (Incorrect substitution)
• $(\lambda x.\lambda x.x)\ne (\lambda y.\lambda x.y)$
  • Correct $\alpha$ -reduction of outer $\lambda$: $(\lambda y.\lambda x.x)$
  • Correct $\alpha$ -reduction of inner $\lambda$: $(\lambda x.\lambda y.y)$

Subtle point: what if $y$ is captured in $t$? Use $\alpha$ -reduction to rename the captured $y$ in $t$ first.

• Example: $\lambda x.(\lambda y.xy)$
• We want to rename $x$ to $y$: $\lambda y.(\lambda y.yy)$
• This is WRONG. The new $y$ is captured by the inner $\lambda y$.
• We must first rename the inner $\lambda y$:
  1. $\lambda x.(\lambda y.xy){\to }_{\alpha }\lambda x.(\lambda z.xz)$
  2. Now rename $x$ to $y$: $\lambda y.(\lambda z.yz)$ (Correct)

$\beta$ -Reduction (Informal)

• Identity function: $\lambda x.x$
• $(\lambda x.x)y=y$
• Observation: we can substitute the formal parameter with the true parameter (argument).

Analogy in C:

• Abstraction: int f (int x) {return x}
• Application: f(y) evaluates to y

$\beta$ -Reduction

The key reduction rule in $\lambda$ -calculus

$(\lambda x.t_1)t_2=t_1\{t_2/x\}$

(Capture-avoiding substitution)

$\beta$ -Reduction Example

Example 1: $(\lambda x.xx)y$

• $t_1=(xx)$
• $t_2=y$
• Rule: $t_1\{t_2/x\}$
• $(xx)\{y/x\}$
• Substitute all free occurrences of $x$ in $t_1$ with $t_2$.
• Both $x$ 's in $(xx)$ are free (relative to the body $t_1$).
• Result: $(yy)$

$\beta$ -Reduction Example

Example 1: $(\lambda x.(xx))y$

• In this case, $(xx)$ corresponds to $t_1$,
• $y$ corresponds to $t_2$
• $FV(t_2)=\{y\}$. $y$ is not in $t_1$, hence, not bound.
• The first rule of substitution applies, which gives
• $(\lambda x.(xx))y{\to }_{\beta }[yy]$

$\beta$ -Reduction Example

Example 2: $(\lambda f.(f(f(\lambda x.x))))(\lambda x.x)$

• This is an application $(\lambda f.t_1)t_2$
• $t_1=(f(f(\lambda x.x)))$
• $t_2=(\lambda x.x)$
• Reduce by substituting $t_2$ for $f$ in $t_1$:
• $t_1\{t_2/f\}\to ((\lambda x.x)((\lambda x.x)(\lambda x.x)))$
• Let $I=(\lambda x.x)$ (the identity function). The expression is $(I(II))$.
• Reduce $(II)$: $(\lambda x.x)(\lambda x.x){\to }_{\beta }(\lambda x.x)$
• The expression becomes $(I(\lambda x.x))$, which is $(II)$ again.
• This reduces again to $(\lambda x.x)$.
• Final Result: $\lambda x.x$

$\beta$ -Reduction Example

Example 3: $(\lambda x.(xx))(\lambda x.(xx))$

• Let $\mathrm{\Omega }=(\lambda x.(xx))$
• The expression is $\mathrm{\Omega }\mathrm{\Omega }$
• This is an application $(\lambda x.t_1)t_2$
• $t_1=(xx)$
• $t_2=(\lambda x.(xx))$ (which is $\mathrm{\Omega }$ itself)
• Reduce by substituting $t_2$ for $x$ in $t_1$:
• $(xx)\{t_2/x\}\to (t_2{t}_2)$
• $\to ((\lambda x.(xx))(\lambda x.(xx)))$
• This is the exact same expression we started with!
• $(\lambda x.(xx))(\lambda x.(xx)){\to }_{\beta }(\lambda x.(xx))(\lambda x.(xx)){\to }_{\beta }...$
• This is an infinite loop.