X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=cb-notes-lecture-1;fp=cb-notes-lecture-1;h=0000000000000000000000000000000000000000;hp=d5ddbac6ab86676363d83d36e1d2e12f9e1e826f;hb=6fb12ab3468258e6b6035be653e36d05088a5aeb;hpb=b500c9bb373fefbf29123d7b5cf47f26b9b7363e diff --git a/cb-notes-lecture-1 b/cb-notes-lecture-1 deleted file mode 100644 index d5ddbac6..00000000 --- a/cb-notes-lecture-1 +++ /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 -