From d573a8cc2162b6664b2d4cfaa7532531ae011ac3 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sun, 12 Sep 2010 18:36:33 -0400 Subject: [PATCH] Notes re lecture 1 --- cb-notes-lecture-1 | 275 +++++++++++++++++++++++++++++++++++++++++++++++++++++ damn.rkt | 14 +++ damn2.rkt | 11 +++ 3 files changed, 300 insertions(+) create mode 100644 cb-notes-lecture-1 create mode 100644 damn.rkt create mode 100644 damn2.rkt diff --git a/cb-notes-lecture-1 b/cb-notes-lecture-1 new file mode 100644 index 00000000..d5ddbac6 --- /dev/null +++ b/cb-notes-lecture-1 @@ -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. +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 + diff --git a/damn.rkt b/damn.rkt new file mode 100644 index 00000000..b7726af2 --- /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 'read + (list 'the + (list (damn) 'book)))))) diff --git a/damn2.rkt b/damn2.rkt new file mode 100644 index 00000000..be328fd9 --- /dev/null +++ b/damn2.rkt @@ -0,0 +1,11 @@ +#lang racket +;(define damn (lambda () 'id)) +(define damn (lambda () (call/cc (lambda (k) + ; (k 'id) + (print "Something's bad") + (k 'id) + )))) + +(list (list 'the (list (damn) 'man)) + (list 'read + (list 'the (list (damn) 'book)))) -- 2.11.0