Lambda Calculus

Like SKI Calculus, its a language of functions; unlike SKI Calculus, there are variables.

\begin{equation} e\to x \mid \lambda x.e \mid ee \mid (e) \end{equation}

meaning, we have:

• a variable \(x\)
• an abstraction \(\lambda x . e\) (a function definition)
• an application \(e_1 e_2\)

we call \((\lambda x . e)e’\) (a function and its argument, ready for reduction) a redex.

abstraction

def f(x) = e

can be written as:

\begin{equation} \lambda x.e \end{equation}

Lambda Calculus, typing

hyperstrict

aggressively reduce everything

call-by-value

we recursively evaluate the argument before reducing the function application

implementing lambda calculus

we can implement Lambda Calculus through abstracting it into SKI Calculus:

observe that \(\lambda x.e \implies A(E, x)\); for each expression \(e\), we replace the innermost lambda expression \(\lambda x.e’\) in \(e\) by \(A(e’, x)\).

simply typed Lambda Calculus

Recall normal lambda calculus:

\begin{equation} e \to x | \lambda x.e | e e \end{equation}

more on types

Remember: when we say \(e: t\), this means that as we evaluate \(e\), after all reductions we will get a thing of type \(t\).

type checking

1. start at the leaves, integers and variables
2. for each one above, match the expression to the type rules

a* type inference

1. for every distinct lambda variable, we name a new type
2. then, for function applications, we have then also substitute the output type of the function with a type variable

then, to saturating the constraint, we solve them using:

Lambda Calculus, review

Grammar:

\begin{equation} e \to (x | \lambda x.e | e e) \end{equation}

and beta reductions:

\begin{equation} (\lambda x . e_1) e_2 \to e_1 [x := e_2] \end{equation}

structural operational semantics

“why can’t we have logical rules to explain how programs execute?”

bold

type judgment

\begin{equation} A \vdash e :t \end{equation}

“under environment \(A\) for the free variables of \(e\), the entirety of \(e\) has type \(t\)”

value judgment

\begin{equation} E \vdash e \to v \end{equation}

Lambda calculus, now with sums:

\begin{equation} e \to (x | \lambda \lambda x.e | e e | i | e+e) \end{equation}

explicit evaluation order

write \(e + e’\) as….

\(( \lambda x . ((\lambda y . (\lambda z.z) (x + y)) e’)) e\)

in a call by value world, this would explicitly specify the order that we add \(x\) and \(y\) together.

Notice! We can also write this with let notation: