index.iki

   1 # Seminar in Semantics / Philosophy of Language #
   2
   3 or: **What Philosophers and Linguists Can Learn From Theoretical Computer Science But Didn't Know To Ask**
   4
   5 This course is co-taught by [Chris Barker](http://homepages.nyu.edu/~cb125/) and [Jim Pryor](http://www.jimpryor.net/). Linguistics calls it "G61.3340-002" and Philosophy calls it "G83.2296-001."
   6 The seminar meets on Mondays from 4-6, in
   7 the Linguistics building at 10 Washington Place, in room 104 (back of the first floor).
   8 One student session will be held every Wednesday from 3-4 on the
   9 fourth floor at 10 Washington Place.
  10
  11 Here is $some^2 x^{e \pi} + 3y$ math, and $$here_{is} some + more$$ End of math.
  12 Except I want to add this: $\frac{-b\pm\sqrt{b^2-4ac}}{2a\pi^i}$ Okay now I'm finished.
  13
  14 Here is a test:
  15
  16
  17 > [[!format  python """
  18 def f(x):
  19     if x:
  20         print "hello, world\n"
  21     else:
  22         return False
  23 """]]
  24
  25 End of test.
  26
  27 ## Announcements ##
  28
  29 <!--
  30 *       This is the time of the semester when some people start slipping
  31 behind with the homework.  Don't.
  32 -->
  33
  34 *       We've added a page on [[Translating between OCaml Scheme and Haskell]]
  35
  36 *       We've added some [commentary](/hints/assignment_6_commentary) on some common issues in your solutions to [[Assignment6]].
  37
  38 *       We've added a [[Monad Library]] for OCaml.
  39
  40 *       We've posted a [[State Monad Tutorial]].
  41
  42 [[Older Announcements]]
  43
  44 ##[[Lambda Evaluator]]##
  45
  46 Usable in your browser. It can help you check whether your answer to some of
  47 the homework questions works correctly.
  48
  49 There is also now a [library](/lambda_library) of lambda-calculus
  50 arithmetical and list operations, some relatively advanced.
  51
  52 ##[[Monad Library]]##
  53
  54
  55 ## Lecture Notes and Assignments ##
  56
  57 (13 Sept) Lecture notes for [[Week1]]; [[Assignment1]].
  58
  59 >       Topics: [[Applications]], including [[Damn]]; Basics of Lambda Calculus; Comparing Different Languages
  60
  61 (20 Sept) Lecture notes for [[Week2]]; [[Assignment2]].
  62
  63 >       Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; [[Lists and Numbers]]
  64
  65 (27 Sept) Lecture notes for [[Week3]];  [[Assignment3]];
  66 an evaluator with the definitions used for homework 3
  67 preloaded is available at [[assignment 3 evaluator]].
  68
  69 >       Topics: [[Evaluation Order]]; Recursion with Fixed Point Combinators
  70
  71 (4 Oct) Lecture notes for [[Week4]]; [[Assignment4]].
  72
  73 >       Topics: More on Fixed Points; Sets; Aborting List Traversals; [[Implementing Trees]]
  74
  75
  76 (18 Oct, 25 Oct) Lecture notes for [[Week5]] and [[Week6]]; [[Assignment5]].
  77
  78 >       Topics: Types, Polymorphism, Unit and Bottom
  79
  80 (1 Nov) Lecture notes for [[Week7]]; [[Assignment6]].
  81
  82 >       Topics: Monads; [[Reader Monad for Variable Binding]]; [[Reader Monad for Intensionality]]
  83
  84 (8 Nov) Lecture notes for [[Week8]].
  85
  86 >       Topics: Reader Monad for Jacobson's Variable-Free Semantics
  87
  88 (15 Nov) Lecture notes for [[Week9]]; [[Assignment7]]. Everyone auditing in the class is encouraged to do this assignment, or at least work through the substantial "hints".
  89
  90 >       Topics: Mutable Variables; Passing by Reference; [[State Monad Tutorial]] (added recently)
  91
  92 (22 Nov) Lecture notes for [[Week10]]
  93
  94 >       Topics: Calculator Improvements, including mutation
  95
  96 (30 Nov) Lecture notes for [[Week11]]; [[Assignment8]].
  97
  98 >       Topics: [[Tree and List Zippers]]; [[Coroutines and Aborts]]; [[From List Zippers to Continuations]]
  99
 100 (6 Dec) Lecture notes for [[Week12]]; [[Assignment9]].
 101
 102 >       Topics: [[List Monad as Continuation Monad]]; [[Manipulating Trees with Monads]] (updated); [[Monad Transformers]] (added recently)
 103
 104 (13 Dec) Lecture notes for Week13; [[Assignment10]].
 105
 106 >       Topics: [[CPS and Continuation Operators]]; Curry-Howard
 107
 108 [[Advanced Topics]]
 109
 110 >       Topics: Version 4 lists, Monads in Category Theory
 111
 112 ##Scheme and OCaml##
 113
 114 See [below](#installing) for how to get the programming languages running on your computer.
 115
 116 *       Links for help [[learning Scheme]]
 117
 118 *       Links for help [[learning OCaml]]
 119
 120 *       [[Translating between OCaml Scheme and Haskell]]
 121
 122
 123 ##[[Offsite Reading]]##
 124
 125 There's lots of links here already to tutorials and encyclopedia entries about many of the notions we'll be dealing with.
 126
 127
 128
 129 ## Course Overview ##
 130
 131 The goal of this seminar is to introduce concepts and techniques from
 132 theoretical computer science and show how they can provide insight
 133 into established philosophical and linguistic problems.
 134
 135 This is not a seminar about any particular technology or software.
 136 Rather, it's about a variety of conceptual/logical ideas that have been
 137 developed in computer science and that linguists and philosophers ought to
 138 know, or may already be unknowingly trying to reinvent.
 139
 140 Philosphers and linguists tend to reuse the same familiar tools in
 141 ever more (sometime spectacularly) creative ways.  But when your only
 142 hammer is classical logic, every problem looks like modus ponens.  In
 143 contrast, computer scientists have invested considerable ingenuity in
 144 studying tool design, and have made remarkable progress.
 145
 146 "Why shouldn't I reinvent some idea X for myself? It's intellectually
 147 rewarding!" Yes it is, but it also takes time you might have better
 148 spent elsewhere. After all, you can get anywhere you want to go by walking, but you can
 149 accomplish more with a combination of walking and strategic subway
 150 rides.
 151
 152 More importantly, the idiosyncrasies of your particular
 153 implementation may obscure what's fundamental to the idea you're
 154 working with. Your implementation may be buggy in corner cases you
 155 didn't think of; it may be incomplete and not trivial to generalize; its
 156 connection to existing literature and neighboring issues may go
 157 unnoticed. For all these reasons you're better off understanding the
 158 state of the art.
 159
 160 The theoretical tools we'll be introducing aren't very familiar to
 161 everyday programmers, but they are prominent in academic computer science,
 162 especially in the fields of functional programming and type theory.
 163
 164 Of necessity, this course will lay a lot of logical groundwork. But throughout
 165 we'll be aiming to mix that groundwork with real cases
 166 in our home subjects where these tools play central roles. Our aim for the
 167 course is to enable you to make these tools your own; to have enough
 168 understanding of them to recognize them in use, use them yourself at least
 169 in simple ways, and to be able to read more about them when appropriate.
 170
 171 Once we get up and running, the central focii of the course will be
 172 **continuations**, **types**, and **monads**. One of the on-going themes will
 173 concern evaluation order and issues about how computations (inferences,
 174 derivations) unfold in (for instance) time.  The key analytic technique is to
 175 form a static, order-independent model of a dynamic process. We'll be
 176 discussing this in much more detail as the course proceeds.
 177
 178 The logical systems we'll be looking at include:
 179
 180 *       the pure/untyped lambda calculus
 181 *       combinatorial logic
 182 *       the simply-typed lambda calculus
 183 *       polymorphic types with System F
 184 *       some discussion of dependent types
 185 *       if time permits, "indeterministic" or "preemptively parallel" computation and linear logic
 186
 187
 188 <!--
 189 Other keywords:
 190         recursion using the Y-combinator
 191         evaluation-order stratgies
 192         normalizing properties
 193         the Curry-Howard isomorphism(s)
 194         monads in category theory and computation
 195 -->
 196
 197 ## Who Can Participate? ##
 198
 199 The course will not presume previous experience with programming.  We
 200 will, however, discuss concepts embodied in specific programming
 201 languages, and we will encourage experimentation with running,
 202 modifying, and writing computer programs.
 203
 204 The course will not presume lots of mathematical or logical background, either.
 205 However, it will demand a certain amount of comfort working with such material; as a result,
 206 it will not be especially well-suited to be a first graduate-level course
 207 in formal semantics or philosophy of language. If you have concerns about your
 208 background, come discuss them with us.
 209
 210 This class will count as satisfying the logic requirement for Philosophy
 211 PhD students; however if this would be your first or only serious
 212 engagement with graduate-level formal work you should consider
 213 carefully, and must discuss with us, (1) whether you'll be adequately
 214 prepared for this course, and (2) whether you'd be better served by
 215 taking a logic course (at a neighboring department, or at NYU next year)
 216 with a more canonical syllabus.
 217
 218
 219 Faculty and students from outside of NYU Linguistics and Philosophy are welcome
 220 to audit, to the extent that this coheres well with the needs of our local
 221 students.
 222
 223
 224 ## Recommended Software ##
 225
 226 During the course, we'll be encouraging you to try out various things in Scheme
 227 and Caml, which are prominent *functional programming languages*. We'll explain
 228 what that means during the course.
 229
 230 *       **Scheme** is one of two major dialects of *Lisp*, which is a large family
 231 of programming languages. Scheme
 232 is the more clean and minimalistic dialect, and is what's mostly used in
 233 academic circles.
 234 Scheme itself has umpteen different "implementations", which share most of
 235 their fundamentals, but have slightly different extensions and interact with
 236 the operating system differently. One major implementation used to be called
 237 PLT Scheme, and has just in the past few weeks changed their name to Racket.
 238 This is what we recommend you use. (If you're already using or comfortable with
 239 another Scheme implementation, though, there's no compelling reason to switch.)
 240
 241         Racket stands to Scheme in something like the relation Firefox stands to HTML.
 242
 243 *       **Caml** is one of two major dialects of *ML*, which is another large
 244 family of programming languages. Caml has only one active implementation,
 245 OCaml, developed by the INRIA academic group in France.
 246
 247 *       Those of you with some programming background may have encountered a third
 248 prominent functional programming language, **Haskell**. This is also used a
 249 lot in the academic contexts we'll be working through. Its surface syntax
 250 differs from Caml, and there are various important things one can do in
 251 each of Haskell and Caml that one can't (or can't as easily) do in the
 252 other. But these languages also have a lot in common, and if you're
 253 familiar with one of them, it's not difficult to move between it and the
 254 other.
 255
 256 <a name=installing></a>
 257 [[How to get the programming languages running on your computer]]
 258
 259 [[Family tree of functional programming languages]]
 260
 261 [[Translating between OCaml Scheme and Haskell]]
 262
 263 ## What is Functional Programming? ##
 264
 265 Here's a [survey conducted at Microsoft](http://research.microsoft.com/apps/pubs/default.aspx?id=141506) asking programmers what they understand "functional programming" to be. Don't take their responses to be authoritative... this is a just a "man in the street" (seat?) poll.
 266
 267 Read more about the [uptake of Haskell](http://steve-yegge.blogspot.com/2010/12/haskell-researchers-announce-discovery.html) among programmers in the street.
 268
 269
 270 ## Recommended Books ##
 271
 272 It's not necessary to purchase these for the class. But they are good ways to get a more thorough and solid understanding of some of the more basic conceptual tools we'll be using.
 273
 274 *       *An Introduction to Lambda Calculi for Computer Scientists*, by Chris
 275 Hankin, currently $17 on
 276 [Amazon](http://www.amazon.com/dp/0954300653).
 277
 278 *       (Another good book covering the same ground as the Hankin book, but
 279 more thoroughly, and in a more mathematical style, is *Lambda-Calculus and Combinators:
 280 an Introduction*, by J. Roger Hindley and Jonathan P. Seldin, currently $52 on [Amazon](http://www.amazon.com/dp/0521898854). If you choose to read
 281 both the Hankin book and this book, you'll notice the authors made some different
 282 terminological/notational choices. At first, this makes comprehension slightly slower,
 283 but in the long run it's helpful because it makes the arbitrariness of those choices more salient.)
 284
 285 *       (Another good book, covering some of the same ground as the previous two, but also delving much deeper into typed lambda calculi, is *Types and Programming Languages*, by Benjamin Pierce, currently $61 on [Amazon](http://www.amazon.com/dp/0262162091). This book has many examples in OCaml.)
 286
 287 *   *The Little Schemer, Fourth Edition*, by Daniel P. Friedman and Matthias
 288 Felleisen, currently $23 on [Amazon](http://www.amazon.com/exec/obidos/ASIN/0262560992).
 289 This is a classic text introducing the gentle art of programming, using the
 290 functional programming language Scheme. Many people love this book, but it has
 291 an unusual dialog format that is not to everybody's taste. **Of particular
 292 interest for this course** is the explanation of the Y combinator, available as
 293 a free sample chapter [at the MIT Press web page for the
 294 book](http://www.ccs.neu.edu/home/matthias/BTLS/).
 295
 296 *       *The Seasoned Schemer*, also by Daniel P. Friedman and Matthias Felleisen, currently $28
 297 on [Amazon](http://www.amazon.com/Seasoned-Schemer-Daniel-P-Friedman/dp/026256100X)
 298
 299 *       *The Little MLer*, by Matthias Felleisen and Daniel P. Friedman, currently $27
 300 on [Amazon](http://www.amazon.com/Little-MLer-Matthias-Felleisen/dp/026256114X).
 301 This covers some of the same introductory ground as The Little Schemer, but
 302 this time in ML. It uses another dialect of ML (called SML), instead of OCaml, but there are only
 303 superficial syntactic differences between these languages. [Here's a translation
 304 manual between them](http://www.mpi-sws.org/~rossberg/sml-vs-ocaml.html).
 305
 306
 307
 308 ----
 309
 310 All wikis are supposed to have a [[SandBox]], so this one does too.
 311
 312 This wiki is powered by [[ikiwiki]].
 313
 314