`~~>`_{β}

) or whether both beta- and eta-reduction is allowed (`~~>`_{βη}

).
+
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 `M ≡ N`

iff `M` and `N` behave the same with respect to every possible sequence of arguments.
-That is, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments `L`_{1}, ..., L_{n}

such that:
+This implies that, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments `L`_{1}, ..., L_{n}

such that:
`M L`_{1} ... L_{n} x y ~~> x
N L_{1} ... L_{n} x y ~~> y

-That is, closed normal forms that are not just beta-reduced but also fully eta-reduced, will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
+So closed beta-plus-eta-normal forms will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
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.
+See Hindley and Seldin, Chapters 7-8 and 14, for discussion of what should count as capturing the "extensionality" of these systems, and some outstanding issues.
+
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).
@@ -430,6 +436,7 @@ But is there any method for doing this in general---for telling, of any given co
* [Scooping the Loop Snooper](http://www.cl.cam.ac.uk/teaching/0910/CompTheory/scooping.pdf), a proof of the undecidability of the halting problem in the style of Dr Seuss by Geoffrey K. Pullum
+Interestingly, Church also set up an association between the lambda calculus and first-order predicate logic, such that, for arbitrary lambda formulas `M` and `N`, some formula would be provable in predicate logic iff `M` and `N` were convertible. So since the right-hand side is not decidable, questions of provability in first-order predicate logic must not be decidable either. This was the first proof of the undecidability of first-order predicate logic.
##[[Lists and Numbers]]##