Lambda Calculus

#PL #Logic

• $\alpha$-equivalent/conversion
  • rename var $\lambda x.x⟺\lambda d.d$
• $\lambda$-equivalent
  • $x\mapsto M⟺\lambda x.M$
• $\beta$-reduction
  • substitute
  • $(\lambda x.x+1)3{\to }_{\beta }3+1$
  • $(\lambda x.M)N{\to }_{\beta }M[N\text{substituted}forx]$ with abbreviated to $M[N/x]$
  • Beta normal form is when you cannot beta reduce (apply lambdas to arguments) the terms any further.

Syntax

• Variables: x, y...
• $\lambda$-Abstractions: $\lambda x.M:A\to B$
  • where $x:A,M:B$
• Applications: $MM$

Computation

• $(\lambda x.M)N{\to }_{\beta }M[N/x]$

That's it. We can do anything a computer can do. Without loops, booleans, data structures...

• Church-Turing Thesis
  Which we must call a new concept, Higher-order
• Functions can be passed as inputs to functions
• Functions can return functions as output
• like $(\lambda x.\lambda y.x+y)12{\to }_{\beta }(\lambda y.1+y)2{\to }_{\beta }1+2$

and a new concept flows out, Currying

• $(\lambda x.\lambda y.L)MN{\to }_{\beta }(\lambda y.L[M/x])N{\to }_{\beta }L[M/x][N/y]$

How can we represent booleans or conditionals?

• True = $\lambda x.\lambda y.x$
• False = $\lambda x.\lambda y.y$
• if then =. $\lambda b.\lambda x.\lambda y.bxy$

Types need to be limited.

#Curry–Howard correspondence