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:

pairs

• Constructor: \(\qty(e,e’)\)
• Destructor: \(p.l, p.r\) or \(fst\ p\), \(snd\ p\)
• Type: \(A * B\)

currying

Consider a function from pairs to a thing: \(A * B \to C\)

We can instead construct a function: \(A \to B \to C: \lambda a . \lambda b. f(a,b)\)

state and exception

Both state and exceptions create “side information”—-the side information is threaded through computation in a specific order; we create new primitives for manipulating side information.

Object

The functional core still stays:

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

Records

Named fields with values:

\begin{equation} [flag = False, value = 42] \end{equation}

“each element of the tuple has a name, and order is unimportant”

If the fields are fixed, they are basically just ADTs.

Record Type

All functions are types, and so are the methods; so we can just add more types for the methods as well. So here’s two properties and a method:

Problem: because Object Calculus and Lambda Calculus really can’t be resolved in into one system, we have to decide either extending objects with lambda (Java, C++), or extend lambda with objects (OCaml, Haskell).

memory safety

This is a problem introduced during manual memory management: pointers or references needs to be checked whether they point to a thing of the correct type — key problem in C/C++ (double free, wild pointer, out of bounds accesses).