cb-notes->week1.mdwn
[lambda.git] / cb-notes-lecture-1
diff --git a/cb-notes-lecture-1 b/cb-notes-lecture-1
deleted file mode 100644 (file)
index d5ddbac..0000000
+++ /dev/null
@@ -1,275 +0,0 @@
-Order matters
-
-Declarative versus imperative:
-
-In a pure declarative language, the order in which expressions are
-evaluated (reduced, simplified) does not affect the outcome.
-
-(3 + 4) * (5 + 11) = 7 * (5 + 11) = 7 * 16 = 112
-(3 + 4) * (5 + 11) = (3 + 4) * 16 = 7 * 16 = 112
-
-In an imperative language, order makes a difference.
-
-x := 2
-x := x + 1
-x == 3
-[true]
-
-x := x + 1
-x := 2
-x == 3
-[false]
-
-
-Declaratives: assertions of statements.
-No matter what order you assert true facts, they remain true:
-
-The value is the product of x and y.
-x is the sum of 3 and 4.
-y is the sum of 5 and 11.
-The value is 112.
-
-Imperatives: performative utterances expressing a deontic or bouletic
-modality  ("Be polite", "shut the door")
-Resource-sensitive, order sensitive: 
-
-Make x == 2.
-Add one to x.
-See if x == 3.
-
-----------------------------------------------------
-
-Untype (monotyped) lambda calculus
-
-Syntax:
-
-Variables: x, x', x'', x''', ...
-(Cheat:    x, y, z, x1, x2, ...)
-
-Each variable is a term.
-For all terms M and N and variable a, the following are also terms:
-
-(M N)   The application of M to N
-(\a M)  The abstraction of a over M
-
-Examples of terms:
-
-x
-(y x)
-(x x)
-(\x y)
-(\x x)
-(\x (\y x))
-(x (\x x))
-((\x (x x))(\x (x x)))
-
-Reduction/conversion/equality:
-
-Lambda terms express recipes for combining terms into new terms.
-The key operation in the lambda calculus is beta-conversion.
-
-((\a M) N) ~~>_beta M{a := N}
-
-The term on the left of the arrow is an application whose first
-element is a lambda abstraction.  (Such an application is called a
-"redex".)  The beta reduction rule says that a redex is
-beta-equivalent to a term that is constructed by replacing every
-(free) occurrence of a in M by a copy of N.  For example, 
-
-((\x x) z) ~~>_beta z
-((\x (x x)) z) ~~>_beta (z z)
-((\x x) (\y y)) ~~>_beta (\y y)
-
-Beta reduction is only allowed to replace *free* occurrences of a variable.
-An occurrence of a variable a is BOUND in T if T has the form (\a N).
-If T has the form (M N), and the occurrence of a is in M, then a is
-bound in T just in case a is bound in M; if the occurrence of a is in
-N, than a is bound in T just in case a is bound in N.  An occurrence
-of a variable a is FREE in a term T iff it is not bound in T.
-For instance:
-
-T = (x (\x (\y (x (y z)))))
-
-The first occurrence of x in T is free.  The second occurrence of x
-immediately follows a lambda, and is bound.  The third occurrence of x
-occurs within a form that begins with "\x", so it is bound as well.
-Both occurrences of y are bound, and the only occurrence of z is free.
-
-Lambda terms represent functions.
-All (recursively computable) functions can be represented by lambda
-terms (the untyped lambda calculus is Turning complete).
-For some lambda terms, it is easy to see what function they represent:
-
-(\x x) the identity function: given any argument M, this function
-simply returns M: ((\x x) M) ~~>_beta M.
-
-(\x (x x)) duplicates its argument:
-((\x (x x)) M) ~~> (M M)
-
-(\x (\y x)) throws away its second argument:
-(((\x (\y x)) M) N) ~~> M
-
-and so on.
-
-It is easy to see that distinct lambda terms can represent the same
-function.  For instance, (\x x) and (\y y) both express the same
-function, namely, the identity function.
-
------------------------------------------
-Dot notation: dot means "put a left paren here, and put the right
-paren as far the right as possible without creating unbalanced
-parentheses".  So (\x(\y(xy))) = \x\y.xy, and \x\y.(z y) x =
-(\x(\y((z y) z))), but (\x\y.(z y)) x = ((\x(\y(z y))) x).
-
------------------------------------------
-
-Church figured out how to encode integers and arithmetic operations
-using lambda terms.  Here are the basics:
-
-0 = \f\x.fx
-1 = \f\x.f(fx)
-2 = \f\x.f(f(fx))
-3 = \f\x.f(f(f(fx)))
-...
-
-Adding two integers involves applying a special function + such that 
-(+ 1) 2 = 3.  Here is a term that works for +:
-
-+ = \m\n\f\x.m(f((n f) x))
-
-So (+ 0) 0 =
-(((\m\n\f\x.m(f((n f) x))) ;+
-  \f\x.fx)                 ;0
-  \f\x.fx)                 ;0
-
-~~>_beta targeting m for beta conversion
-
-((\n\f\x.[\f\x.fx](f((n f) x)))
- \f\x.fx)
-
-\f\x.[\f\x.fx](f(([\f\x.fx] f) x))
-
-\f\x.[\f\x.fx](f(fx))
-
-\f\x.\x.[f(fx)]x
-
-\f\x.f(fx)
-
-
-
-----------------------------------------------------
-
-A concrete example: "damn" side effects
-
-1. Sentences have truth conditions.
-2. If "John read the book" is true, then
-   John read something,
-   Someone read the book,
-   John did something to the book, 
-   etc.
-3. If "John read the damn book",
-   all the same entailments follow.
-   To a first approximation, "damn" does not affect at-issue truth
-   conditions.  
-4. "Damn" does contribute information about the attitude of the speaker
-   towards some aspect of the situation described by the sentence.
-
-
-
------------------------------------------
-Old notes, no longer operative:
-
-1. Theoretical computer science is beautiful.
-
-   Google search for "anagram": Did you mean "nag a ram"?
-   Google search for "recursion": Did you mean "recursion"?
-
-   Y = \f.(\x.f (x x)) (\x.f (x x))
-
-
-1. Understanding the meaning(use) of programming languages
-   helps understanding the meaning(use) of natural langauges
-
-      1. Richard Montague. 1970. Universal Grammar. _Theoria_ 34:375--98.
-         "There is in my opinion no important theoretical difference
-         between natural languages and the artificial languages of
-         logicians; indeed, I consider it possible to comprehend the
-         syntax and semantics of both kinds of languages within a
-         single natural and mathematically precise theory."
-
-      2. Similarities: 
-
-         Function/argument structure: 
-             f(x)    
-             kill(it)
-         pronominal binding: 
-             x := x + 1
-             John is his own worst enemy
-         Quantification:
-             foreach x in [1..10] print x
-             Print every number from 1 to 10
-
-      3. Possible differences:
-
-         Parentheses:
-             3 * (4 + 7)
-             ?It was four plus seven that John computed 3 multiplied by
-             (compare: John computed 3 multiplied by four plus seven)
-         Ambiguity:
-             3 * 4 + 7
-             Time flies like and arrow, fruit flies like a banana.
-         Vagueness:
-             3 * 4
-             A cloud near the mountain
-         Unbounded numbers of distinct pronouns:
-             f(x1) + f(x2) + f(x3) + ...
-             He saw her put it in ...
-             [In ASL, dividing up the signing space...]
-         
-         
-2. Standard methods in linguistics are limited.
-
-   1. First-order predicate calculus
-
-        Invented for reasoning about mathematics (Frege's quantification)
-
-        Alethic, order insensitive: phi & psi == psi & phi
-        But: John left and Mary left too /= Mary left too and John left
-
-   2. Simply-typed lambda calculus 
-
-        Can't express the Y combinator
-
-
-3. Meaning is computation.
-
-   1. Semantics is programming 
-
-   2. Good programming is good semantics
-
-      1. Example 
-
-         1. Programming technique
-
-            Exceptions
-              throw (raise)
-              catch (handle)
-
-         2. Application to linguistics
-              presupposition
-              expressives
-
-              Develop application:
-                fn application
-                divide by zero
-                test and repair
-                raise and handle
-
-                fn application
-                presupposition failure
-                build into meaning of innocent predicates?
-                expressives
-                throw
-                handle
-                resume computation