A third way to think is to identify the lambda formula not with classes of alphabetic sequences, but rather with abstract structures that we might draw like this:
-<pre><code>λ
- ... ___ ...
-^ |
-|______|
+<pre><code>
+ λ ... ___ ...
+ ^ |
+ |______|
</code></pre>
Here there are no bound variables, but there are *bound positions*. We can regard formula like (a) and (b) as just helpfully readable ways to designate these abstract structures.
With regard to Q3, it should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when eta-reduction is added to the proof theory is importantly different from the one where only beta-reduction is permitted.
+If we answer Q2 by permitting reduction inside abstracts, and we also permit eta-reduction, then where none of <code>y<sub>1</sub>, ..., y<sub>n</sub> occur free in M, this:
+
+<pre><code>\x y<sub>1</sub>... y<sub>n</sub>. M y<sub>1</sub>... y<sub>n</sub></code></pre>
+
+will eta-reduce by n steps to:
+
+ \x. M
+
The logical system you get when eta-reduction is added to the proof system has the following property:
> if `M`, `N` are normal forms with no free variables, then <code>M ≡ N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.
So the proof theory with eta-reduction added is called "extensional," because its notion of normal form makes syntactic identity of closed normal forms coincide with extensional equivalence.
-If we answer Q2 by permitting reduction inside abstracts, and we also permit eta-reduction, then where neither `y` nor `z` occur in M, this:
-
- \x y z. M y z
-
-will eta-reduce by two steps to:
-
- \x. M
-
The evaluation strategy which answers Q1 by saying "reduce arguments first" is known as **call-by-value**. The evaluation strategy which answers Q1 by saying "substitute arguments in unreduced" is known as **call-by-name** or **call-by-need** (the difference between these has to do with efficiency, not semantics).
When one has a call-by-value strategy that also permits reduction to continue inside unapplied abstracts, that's known as "applicative order" reduction. When one has a call-by-name strategy that permits reduction inside abstracts, that's known as "normal order" reduction. Consider an expression of the form: