Lambda Calculus

Definition

Each lambda term is built with the CFG:

  1. v is some variable ( evaluates to )
  2. Defines a function that takes in variable and outputs (in Scala, { v => e })
  3. Two expressions next to each other (e(e), function call)

You may also include the production , but I guess this can be done implicitly or whatever.

β-Reductions

Definition

calling a function is just putting the parameter in its body and "running" its body.

The notation means substitute for (can't get away from SE212), so the whole output means the expression with all occurrences of substituted with .

It's common for the brackets around the argument to be omitted: .

Example

we have a function that takes some parameter and outputs twice, then we call it with argument .

To make functions that take multiple params, we can curry them:

which is the same as:

Example -reductions:

Variable Capture and α-Reductions

Consider the function:

if you just blindly replace the (the outermost substituted into ), then you get:

which is very bad, since this changes the meaning.

We can use ALPHA RENAMING (NO WAY) to fix this:

now our substitution is ok (yay):

George does not support alpha-renaming.

Formally:

Definition

obviously