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:

two good things about this

- the order of evaluation is explicit
- every intermediate result is now named