author Jim Pryor Thu, 16 Sep 2010 21:15:22 +0000 (17:15 -0400) committer Jim Pryor Thu, 16 Sep 2010 21:15:22 +0000 (17:15 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
 week2.mdwn patch | blob | history

index 6f15799..1cabf64 100644 (file)
@@ -3,21 +3,15 @@ Syntactic equality, reduction, convertibility

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 &equiv; `(\x. x y) z` &equiv; `(\z. z y) z`
-</pre>
+>      T &equiv; `(\x. x y) z` &equiv; `(\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.

@@ -98,7 +92,9 @@ This question highlights that there are different choices to make about how eval

>              \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

@@ -130,7 +126,7 @@ Its syntax has the following tree:
/  \  /  \
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.