more assignment1 tweaks
[lambda.git] / cb-notes-lecture-1
1 Order matters
2
3 Declarative versus imperative:
4
5 In a pure declarative language, the order in which expressions are
6 evaluated (reduced, simplified) does not affect the outcome.
7
8 (3 + 4) * (5 + 11) = 7 * (5 + 11) = 7 * 16 = 112
9 (3 + 4) * (5 + 11) = (3 + 4) * 16 = 7 * 16 = 112
10
11 In an imperative language, order makes a difference.
12
13 x := 2
14 x := x + 1
15 x == 3
16 [true]
17
18 x := x + 1
19 x := 2
20 x == 3
21 [false]
22
23
24 Declaratives: assertions of statements.
25 No matter what order you assert true facts, they remain true:
26
27 The value is the product of x and y.
28 x is the sum of 3 and 4.
29 y is the sum of 5 and 11.
30 The value is 112.
31
32 Imperatives: performative utterances expressing a deontic or bouletic
33 modality  ("Be polite", "shut the door")
34 Resource-sensitive, order sensitive: 
35
36 Make x == 2.
37 Add one to x.
38 See if x == 3.
39
40 ----------------------------------------------------
41
42 Untype (monotyped) lambda calculus
43
44 Syntax:
45
46 Variables: x, x', x'', x''', ...
47 (Cheat:    x, y, z, x1, x2, ...)
48
49 Each variable is a term.
50 For all terms M and N and variable a, the following are also terms:
51
52 (M N)   The application of M to N
53 (\a M)  The abstraction of a over M
54
55 Examples of terms:
56
57 x
58 (y x)
59 (x x)
60 (\x y)
61 (\x x)
62 (\x (\y x))
63 (x (\x x))
64 ((\x (x x))(\x (x x)))
65
66 Reduction/conversion/equality:
67
68 Lambda terms express recipes for combining terms into new terms.
69 The key operation in the lambda calculus is beta-conversion.
70
71 ((\a M) N) ~~>_beta M{a := N}
72
73 The term on the left of the arrow is an application whose first
74 element is a lambda abstraction.  (Such an application is called a
75 "redex".)  The beta reduction rule says that a redex is
76 beta-equivalent to a term that is constructed by replacing every
77 (free) occurrence of a in M by a copy of N.  For example, 
78
79 ((\x x) z) ~~>_beta z
80 ((\x (x x)) z) ~~>_beta (z z)
81 ((\x x) (\y y)) ~~>_beta (\y y)
82
83 Beta reduction is only allowed to replace *free* occurrences of a variable.
84 An occurrence of a variable a is BOUND in T if T has the form (\a N).
85 If T has the form (M N), and the occurrence of a is in M, then a is
86 bound in T just in case a is bound in M; if the occurrence of a is in
87 N, than a is bound in T just in case a is bound in N.  An occurrence
88 of a variable a is FREE in a term T iff it is not bound in T.
89 For instance:
90
91 T = (x (\x (\y (x (y z)))))
92
93 The first occurrence of x in T is free.  The second occurrence of x
94 immediately follows a lambda, and is bound.  The third occurrence of x
95 occurs within a form that begins with "\x", so it is bound as well.
96 Both occurrences of y are bound, and the only occurrence of z is free.
97
98 Lambda terms represent functions.
99 All (recursively computable) functions can be represented by lambda
100 terms (the untyped lambda calculus is Turning complete).
101 For some lambda terms, it is easy to see what function they represent:
102
103 (\x x) the identity function: given any argument M, this function
104 simply returns M: ((\x x) M) ~~>_beta M.
105
106 (\x (x x)) duplicates its argument:
107 ((\x (x x)) M) ~~> (M M)
108
109 (\x (\y x)) throws away its second argument:
110 (((\x (\y x)) M) N) ~~> M
111
112 and so on.
113
114 It is easy to see that distinct lambda terms can represent the same
115 function.  For instance, (\x x) and (\y y) both express the same
116 function, namely, the identity function.
117
118 -----------------------------------------
119 Dot notation: dot means "put a left paren here, and put the right
120 paren as far the right as possible without creating unbalanced
121 parentheses".  So (\x(\y(xy))) = \x\y.xy, and \x\y.(z y) x =
122 (\x(\y((z y) z))), but (\x\y.(z y)) x = ((\x(\y(z y))) x).
123
124 -----------------------------------------
125
126 Church figured out how to encode integers and arithmetic operations
127 using lambda terms.  Here are the basics:
128
129 0 = \f\x.fx
130 1 = \f\x.f(fx)
131 2 = \f\x.f(f(fx))
132 3 = \f\x.f(f(f(fx)))
133 ...
134
135 Adding two integers involves applying a special function + such that 
136 (+ 1) 2 = 3.  Here is a term that works for +:
137
138 + = \m\n\f\x.m(f((n f) x))
139
140 So (+ 0) 0 =
141 (((\m\n\f\x.m(f((n f) x))) ;+
142   \f\x.fx)                 ;0
143   \f\x.fx)                 ;0
144
145 ~~>_beta targeting m for beta conversion
146
147 ((\n\f\x.[\f\x.fx](f((n f) x)))
148  \f\x.fx)
149
150 \f\x.[\f\x.fx](f(([\f\x.fx] f) x))
151
152 \f\x.[\f\x.fx](f(fx))
153
154 \f\x.\x.[f(fx)]x
155
156 \f\x.f(fx)
157
158
159
160 ----------------------------------------------------
161
162 A concrete example: "damn" side effects
163
164 1. Sentences have truth conditions.
165 2. If "John read the book" is true, then
166    John read something,
167    Someone read the book,
168    John did something to the book, 
169    etc.
170 3. If "John read the damn book",
171    all the same entailments follow.
172    To a first approximation, "damn" does not affect at-issue truth
173    conditions.  
174 4. "Damn" does contribute information about the attitude of the speaker
175    towards some aspect of the situation described by the sentence.
176
177
178
179 -----------------------------------------
180 Old notes, no longer operative:
181
182 1. Theoretical computer science is beautiful.
183
184    Google search for "anagram": Did you mean "nag a ram"?
185    Google search for "recursion": Did you mean "recursion"?
186
187    Y = \f.(\x.f (x x)) (\x.f (x x))
188
189
190 1. Understanding the meaning(use) of programming languages
191    helps understanding the meaning(use) of natural langauges
192
193       1. Richard Montague. 1970. Universal Grammar. _Theoria_ 34:375--98.
194          "There is in my opinion no important theoretical difference
195          between natural languages and the artificial languages of
196          logicians; indeed, I consider it possible to comprehend the
197          syntax and semantics of both kinds of languages within a
198          single natural and mathematically precise theory."
199
200       2. Similarities: 
201
202          Function/argument structure: 
203              f(x)    
204              kill(it)
205          pronominal binding: 
206              x := x + 1
207              John is his own worst enemy
208          Quantification:
209              foreach x in [1..10] print x
210              Print every number from 1 to 10
211
212       3. Possible differences:
213
214          Parentheses:
215              3 * (4 + 7)
216              ?It was four plus seven that John computed 3 multiplied by
217              (compare: John computed 3 multiplied by four plus seven)
218          Ambiguity:
219              3 * 4 + 7
220              Time flies like and arrow, fruit flies like a banana.
221          Vagueness:
222              3 * 4
223              A cloud near the mountain
224          Unbounded numbers of distinct pronouns:
225              f(x1) + f(x2) + f(x3) + ...
226              He saw her put it in ...
227              [In ASL, dividing up the signing space...]
228          
229          
230 2. Standard methods in linguistics are limited.
231
232    1. First-order predicate calculus
233
234         Invented for reasoning about mathematics (Frege's quantification)
235
236         Alethic, order insensitive: phi & psi == psi & phi
237         But: John left and Mary left too /= Mary left too and John left
238
239    2. Simply-typed lambda calculus 
240
241         Can't express the Y combinator
242
243
244 3. Meaning is computation.
245
246    1. Semantics is programming 
247
248    2. Good programming is good semantics
249
250       1. Example 
251
252          1. Programming technique
253
254             Exceptions
255               throw (raise)
256               catch (handle)
257
258          2. Application to linguistics
259               presupposition
260               expressives
261
262               Develop application:
263                 fn application
264                 divide by zero
265                 test and repair
266                 raise and handle
267
268                 fn application
269                 presupposition failure
270                 build into meaning of innocent predicates?
271                 expressives
272                 throw
273                 handle
274                 resume computation
275