week1: remove test2.mdwn

[lambda.git] / week1.mdwn

diff --git a/week1.mdwn b/week1.mdwn
index 2c68658..1bc2309 100644 (file)
--- a/week1.mdwn
+++ b/week1.mdwn
@@ -57,7 +57,7 @@ We'll tend to write <code>(&lambda;a M)</code> as just `(\a M)`, so we don't hav
 <strong>Application</strong>: <code>(M N)</code>
 </blockquote>
 
 <strong>Application</strong>: <code>(M N)</code>
 </blockquote>
 

-Some *authors* reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
+Some authors reserve the term "term" for just variables and abstracts. We'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.

 
 Examples of expressions:
 
 
 Examples of expressions:
 


@@ -74,7 +74,7 @@ The lambda calculus has an associated proof theory. For now, we can regard the
 proof theory as having just one rule, called the rule of **beta-reduction** or
 "beta-contraction". Suppose you have some expression of the form:
 
 proof theory as having just one rule, called the rule of **beta-reduction** or
 "beta-contraction". Suppose you have some expression of the form:
 

-       ((\a M) N)
+       ((\ a M) N)

 
 that is, an application of an abstract to some other expression. This compound form is called a **redex**, meaning it's a "beta-reducible expression." `(\a M)` is called the **head** of the redex; `N` is called the **argument**, and `M` is called the **body**.
 
 
 that is, an application of an abstract to some other expression. This compound form is called a **redex**, meaning it's a "beta-reducible expression." `(\a M)` is called the **head** of the redex; `N` is called the **argument**, and `M` is called the **body**.
 


@@ -285,18 +285,16 @@ It's possible to enhance the lambda calculus so that functions do get identified
 
 It's often said that dynamic systems are distinguished because they are the ones in which **order matters**. However, there are many ways in which order can matter. If we have a trivalent boolean system, for example---easily had in a purely functional calculus---we might choose to give a truth-table like this for "and":
 
 
 It's often said that dynamic systems are distinguished because they are the ones in which **order matters**. However, there are many ways in which order can matter. If we have a trivalent boolean system, for example---easily had in a purely functional calculus---we might choose to give a truth-table like this for "and":
 

-<pre><code>
-true and true   = true
-true and true   = true
-true and *      = *
-true and false  = false
-* and true      = *
-* and *         = *
-* and false     = *
-false and true  = false
-false and *     = false
-false and false = false
-</code></pre>
+       true and true   = true
+       true and true   = true
+       true and *      = *
+       true and false  = false
+       * and true      = *
+       * and *         = *
+       * and false     = *
+       false and true  = false
+       false and *     = false
+       false and false = false

 
 And then we'd notice that `* and false` has a different intepretation than `false and *`. (The same phenomenon is already present with the material conditional in bivalent logics; but seeing that a non-symmetric semantics for `and` is available even for functional languages is instructive.)
 
 
 And then we'd notice that `* and false` has a different intepretation than `false and *`. (The same phenomenon is already present with the material conditional in bivalent logics; but seeing that a non-symmetric semantics for `and` is available even for functional languages is instructive.)
 


@@ -603,7 +601,6 @@ Here's how it looks to say the same thing in various of these languages.
 
        It's easy to be lulled into thinking this is a kind of imperative construction. *But it's not!* It's really just a shorthand for the compound "let"-expressions we've already been looking at, taking the maximum syntactically permissible scope. (Compare the "dot" convention in the lambda calculus, discussed above.)
 
 
        It's easy to be lulled into thinking this is a kind of imperative construction. *But it's not!* It's really just a shorthand for the compound "let"-expressions we've already been looking at, taking the maximum syntactically permissible scope. (Compare the "dot" convention in the lambda calculus, discussed above.)
 

-

 9.     Some shorthand
 
        OCaml permits you to abbreviate:
 9.     Some shorthand
 
        OCaml permits you to abbreviate:


@@ -674,9 +671,8 @@ Here's how it looks to say the same thing in various of these languages.
 
        and there's no more mutation going on there than there is in:
 
 
        and there's no more mutation going on there than there is in:
 

-       <pre>
-       <code>&forall;x. (F x or &forall;x (not (F x)))</code>
-       </pre>
+       <pre><code>&forall;x. (F x or &forall;x (not (F x)))
+       </code></pre>

 
        When a previously-bound variable is rebound in the way we see here, that's called **shadowing**: the outer binding is shadowed during the scope of the inner binding.
 
 
        When a previously-bound variable is rebound in the way we see here, that's called **shadowing**: the outer binding is shadowed during the scope of the inner binding.