Define T to be `(\x. x y) z`. Then T and `(\x. x y) z` are syntactically equal, and we're counting them as syntactically equal to `(\z. z y) z` as well, which we will write as:
-<pre>
-T ≡ `(\x. x y) z` ≡ `(\z. z y) z`
-</pre>
+> T ≡ `(\x. x y) z` ≡ `(\z. z y) z`
This:
-<pre>
-T ~~> `z y`
-</pre>
+ T ~~> z y
means that T beta-reduces to `z y`. This:
-<pre>
-M <~~> T
-</pre>
+ M <~~> T
means that M and T are beta-convertible, that is, that there's something they both reduce to in zero or more steps.
> \x. M x
-> where x does not occur free in `M`, to `M`? 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.
+> where x does not occur free in `M`, to `M`?
+
+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.
MORE on extensionality
/ \ / \
A B C D
-Applicative order evaluation does what's called a "post-order traversal" of the tree: that is, we always go left and down whenever we can, and we process a node only after processing all its children. So `(C D)` gets processed before `((A B) (C D))` does, and `(E F)` gets processed before `((A B) (C D)) (E F)` does.
+Applicative order evaluation does what's called a "post-order traversal" of the tree: that is, we always go down when we can, first to the left, and we process a node only after processing all its children. So `(C D)` gets processed before `((A B) (C D))` does, and `(E F)` gets processed before `((A B) (C D)) (E F)` does.
Normal order evaluation, on the other hand, will substitute the expresion `(C D)` into the abstract that `(A B)` evaluates to, without first trying to compute what `(C D)` evaluates to. That computation may be done later.