week2 tweak

[lambda.git] / week2.mdwn

diff --git a/week2.mdwn b/week2.mdwn
index b186702..ce2df76 100644 (file)
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -56,20 +56,20 @@ In a bit, we'll discuss other systems that lack variables. Those systems will no
 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:
+Define N to be `(\x. x y) z`. Then N 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><code>T &equiv; (\x. x y) z &equiv; (\z. z y) z
+<pre><code>N &equiv; (\x. x y) z &equiv; (\z. z y) z
 </code></pre>
 
 This:
 
-       T ~~> z y
+       N ~~> z y
 
-means that T beta-reduces to `z y`. This:
+means that N beta-reduces to `z y`. This:
 
-       M <~~> T
+       M <~~> N
 
-means that M and T are beta-convertible, that is, that there's something they both reduce to in zero or more steps.
+means that M and N are beta-convertible, that is, that there's something they both reduce to in zero or more steps.
 
 Combinators and Combinatorial Logic
 ===================================
@@ -141,7 +141,7 @@ The reduction rule for K is also straightforward:
 That is, K throws away its second argument.  The reduction rule for S can be constructed by examining 
 the defining lambda term:
 
-    S = \fgx.fx(gx)
+<pre><code>S &equiv; \fgx.fx(gx)</code></pre>
 
 S takes three arguments, duplicates the third argument, and feeds one copy to the first argument and the second copy to the second argument.  So:
 
@@ -189,19 +189,19 @@ Let's check that the translation of the false boolean behaves as expected by fee
 
 Throws away the first argument, returns the second argument---yep, it works.
 
-Here's a more elaborate example of the translation.  The goal is to establish that combinators can reverse order, so we use the T combinator, where `T = \x\y.yx`:
+Here's a more elaborate example of the translation.  The goal is to establish that combinators can reverse order, so we use the **T** combinator, where  <code>T &equiv; \x\y.yx</code>:
 
     [\x\y.yx] = [\x[\y.yx]] = [\x.S[\y.y][\y.x]] = [\x.(SI)(Kx)] = S[\x.SI][\x.Kx] = S(K(SI))(S[\x.K][\x.x]) = S(K(SI))(S(KK)I)
 
 We can test this translation by seeing if it behaves like the original lambda term does.
 The orginal lambda term lifts its first argument (think of it as reversing the order of its two arguments):
 
-   S(K(SI))(S(KK)I) X Y =
-   (K(SI))X ((S(KK)I) X) Y = 
-   SI ((KK)X (IX)) Y = 
-   SI (KX) Y =
-   IY (KX)Y =
-   Y X
+       S(K(SI))(S(KK)I) X Y ~~>
+       (K(SI))X ((S(KK)I) X) Y ~~>
+       SI ((KK)X (IX)) Y ~~>
+       SI (KX) Y ~~>
+       IY (KXY) ~~>
+       Y X
 
 Voil&agrave;: the combinator takes any X and Y as arguments, and returns Y applied to X.