author Chris Barker Sun, 12 Sep 2010 22:36:33 +0000 (18:36 -0400) committer Chris Barker Sun, 12 Sep 2010 22:36:33 +0000 (18:36 -0400)
 cb-notes-lecture-1 [new file with mode: 0644] patch | blob damn.rkt [new file with mode: 0644] patch | blob damn2.rkt [new file with mode: 0644] patch | blob

diff --git a/cb-notes-lecture-1 b/cb-notes-lecture-1
new file mode 100644 (file)
index 0000000..d5ddbac
--- /dev/null
@@ -0,0 +1,275 @@
+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.
+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 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
diff --git a/damn.rkt b/damn.rkt
new file mode 100644 (file)
index 0000000..b7726af
--- /dev/null
+++ b/damn.rkt
@@ -0,0 +1,14 @@
+#lang racket
+;((lambda () (list 'John (list 'read (list 'the (list ((lambda () 'id)) 'book))))))
+
+;(define damn (lambda () 'id))
+
+(define damn (lambda () (call/cc (lambda (k) (raise (list "Something's bad" k))))))
+
+(call-with-exception-handler
+ (lambda (e) (print (first e)) ((second e) 'id)) ; this is the exception handler
+ (lambda ()
+   (list (list 'the (list (damn) 'man))
+               (list 'the
+                     (list (damn) 'book))))))
diff --git a/damn2.rkt b/damn2.rkt
new file mode 100644 (file)
index 0000000..be328fd
--- /dev/null
+++ b/damn2.rkt
@@ -0,0 +1,11 @@
+#lang racket
+;(define damn (lambda () 'id))
+(define damn (lambda () (call/cc (lambda (k)
+                                  ; (k 'id)