+Now we can allow ourselves to introduce λ-expressions in the following way. If a λ-expression is applied to an argument, as in: `(`λ `x.` φ`) M`, for any (simple or complex) expressions φ and `M`, this means the same as: `let x be M in` φ. That is, the argument to the λ-expression provides (when evaluated) a value for the variable `x` to be bound to, and then the result of the whole thing is whatever φ evaluates to, under that binding to `x`.
+
+If we restricted ourselves to only that usage of λ-expressions, that is when they were applied to all the arguments they're expecting, then we wouldn't have moved very far from the decidable fragment of arithmetic we began with.
+
+However, it's tempting to help ourselves to the notion (at least partly) *unapplied* λ-expressions, too. If I can make sense of what:
+
+ (λ x. x + 1) 5
+
+means, then I can make sense of what:
+
+ (λ x. x + 1)
+
+means, too. It's just *the function* that waits for an argument and then returns the result of `x + 1` with `x` bound to that argument.
+