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