X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=index.mdwn;h=1d090eb60ebb388cb0e638064f5018ee20ed933f;hp=abbef74e5c3627e2f1c5b61bf2099b86f5e2f251;hb=49e6889d3ceb77526298a84549df44871caaf7a0;hpb=c159fd528fb88720ed649cfd51dd001b3373b3cb diff --git a/index.mdwn b/index.mdwn index abbef74e..1d090eb6 100644 --- a/index.mdwn +++ b/index.mdwn @@ -1,13 +1,276 @@ -Welcome to your new wiki. +# Seminar in Semantics / Philosophy of Language # -All wikis are supposed to have a [[SandBox]], so this one does too. +or: **What Philosophers and Linguists Can Learn From Theoretical Computer Science But Didn't Know To Ask** + +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." +The seminar meets on Mondays from 4-6, in +the Linguistics building at 10 Washington Place, in room 104 (back of the first floor). +One student session will be held every Wednesday from 3-4 on the +fourth floor at 10 Washington Place. + +## Announcements ## + +* This is the time of the semester when some people start slipping + behind with the homework. Don't. + +[[Older Announcements]] + +##[[Lambda Evaluator]]## + +Usable in your browser. It can help you check whether your answer to some of +the homework questions works correctly. + +There is also now a [library](/lambda_library) of lambda-calculus +arithmetical and list operations, some relatively advanced. + + +## Lecture Notes and Assignments ## + +(13 Sept) Lecture notes for [[Week1]]; [[Assignment1]]. + +> Topics: [[Applications]], including [[Damn]]; Basics of Lambda Calculus; Comparing Different Languages + +(20 Sept) Lecture notes for [[Week2]]; [[Assignment2]]. + +> Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; [[Lists and Numbers]] + +(27 Sept) Lecture notes for [[Week3]]; [[Assignment3]]; +an evaluator with the definitions used for homework 3 +preloaded is available at [[assignment 3 evaluator]]. + +> Topics: [[Evaluation Order]]; Recursion with Fixed Point Combinators + +(4 Oct) Lecture notes for [[Week4]]; [[Assignment4]]. + +> Topics: More on Fixed Points; Sets; Aborting List Traversals; [[Implementing Trees]] + + +(18 Oct, 25 Oct) Lecture notes for [[Week5]] and [[Week6]]; [[Assignment5]]. + +> Topics: Types, Polymorphism, Unit and Bottom + +(1 Nov) Lecture notes for [[Week7]]; [[Assignment6]]. + +> Topics: Monads; [[Reader Monad for Variable Binding]]; [[Reader Monad for Intensionality]] + +(8 Nov) Lecture notes for [[Week8]]. + +> Topics: Reader Monad for Jacobson's Variable-Free Semantics + +(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". + +> Topics: Mutable Variables; Passing by Reference + +(22 Nov) Lecture notes for [[Week10]] + +> Topics: Calculator Improvements, including mutation + +(30 Nov) Lecture notes for [[Week11]]; [[Assignment8]]. + +> Topics: [[Tree and List Zippers]]; [[Coroutines and Aborts]]; [[From List Zippers to Continuations]]. + +(6 Dec) Lecture notes for [[Week12]] + +> Topics: [[List Monad as Continuation Monad]]; [[Manipulating Trees with Monads]]; ... + +(13 Dec) Lecture notes for Week13 + +[[Upcoming topics]] + +[[Advanced Topics]] + +> Topics: Version 4 lists, Monads in Category Theory, Calculator Improvements + +##Scheme and OCaml## + +See [below](#installing) for how to get the programming languages running on your computer. + +* Links for help [[learning Scheme]] + +* Links for help [[learning OCaml]] + + +##[[Offsite Reading]]## -Sample content. +There's lots of links here already to tutorials and encyclopedia entries about many of the notions we'll be dealing with. + + + +## Course Overview ## + +The goal of this seminar is to introduce concepts and techniques from +theoretical computer science and show how they can provide insight +into established philosophical and linguistic problems. + +This is not a seminar about any particular technology or software. +Rather, it's about a variety of conceptual/logical ideas that have been +developed in computer science and that linguists and philosophers ought to +know, or may already be unknowingly trying to reinvent. + +Philosphers and linguists tend to reuse the same familiar tools in +ever more (sometime spectacularly) creative ways. But when your only +hammer is classical logic, every problem looks like modus ponens. In +contrast, computer scientists have invested considerable ingenuity in +studying tool design, and have made remarkable progress. + +"Why shouldn't I reinvent some idea X for myself? It's intellectually +rewarding!" Yes it is, but it also takes time you might have better +spent elsewhere. After all, you can get anywhere you want to go by walking, but you can +accomplish more with a combination of walking and strategic subway +rides. + +More importantly, the idiosyncrasies of your particular +implementation may obscure what's fundamental to the idea you're +working with. Your implementation may be buggy in corner cases you +didn't think of; it may be incomplete and not trivial to generalize; its +connection to existing literature and neighboring issues may go +unnoticed. For all these reasons you're better off understanding the +state of the art. + +The theoretical tools we'll be introducing aren't very familiar to +everyday programmers, but they are prominent in academic computer science, +especially in the fields of functional programming and type theory. + +Of necessity, this course will lay a lot of logical groundwork. But throughout +we'll be aiming to mix that groundwork with real cases +in our home subjects where these tools play central roles. Our aim for the +course is to enable you to make these tools your own; to have enough +understanding of them to recognize them in use, use them yourself at least +in simple ways, and to be able to read more about them when appropriate. + +Once we get up and running, the central focii of the course will be +**continuations**, **types**, and **monads**. One of the on-going themes will +concern evaluation order and issues about how computations (inferences, +derivations) unfold in (for instance) time. The key analytic technique is to +form a static, order-independent model of a dynamic process. We'll be +discussing this in much more detail as the course proceeds. + +The logical systems we'll be looking at include: + +* the pure/untyped lambda calculus +* combinatorial logic +* the simply-typed lambda calculus +* polymorphic types with System F +* some discussion of dependent types +* if time permits, "indeterministic" or "preemptively parallel" computation and linear logic + + + + +## Who Can Participate? ## + +The course will not presume previous experience with programming. We +will, however, discuss concepts embodied in specific programming +languages, and we will encourage experimentation with running, +modifying, and writing computer programs. + +The course will not presume lots of mathematical or logical background, either. +However, it will demand a certain amount of comfort working with such material; as a result, +it will not be especially well-suited to be a first graduate-level course +in formal semantics or philosophy of language. If you have concerns about your +background, come discuss them with us. + +This class will count as satisfying the logic requirement for Philosophy +PhD students; however if this would be your first or only serious +engagement with graduate-level formal work you should consider +carefully, and must discuss with us, (1) whether you'll be adequately +prepared for this course, and (2) whether you'd be better served by +taking a logic course (at a neighboring department, or at NYU next year) +with a more canonical syllabus. + + +Faculty and students from outside of NYU Linguistics and Philosophy are welcome +to audit, to the extent that this coheres well with the needs of our local +students. + + +## Recommended Software ## + +During the course, we'll be encouraging you to try out various things in Scheme +and Caml, which are prominent *functional programming languages*. We'll explain +what that means during the course. + +* **Scheme** is one of two major dialects of *Lisp*, which is a large family +of programming languages. Scheme +is the more clean and minimalistic dialect, and is what's mostly used in +academic circles. +Scheme itself has umpteen different "implementations", which share most of +their fundamentals, but have slightly different extensions and interact with +the operating system differently. One major implementation used to be called +PLT Scheme, and has just in the past few weeks changed their name to Racket. +This is what we recommend you use. (If you're already using or comfortable with +another Scheme implementation, though, there's no compelling reason to switch.) + + Racket stands to Scheme in something like the relation Firefox stands to HTML. + +* **Caml** is one of two major dialects of *ML*, which is another large +family of programming languages. Caml has only one active implementation, +OCaml, developed by the INRIA academic group in France. + +* Those of you with some programming background may have encountered a third +prominent functional programming language, **Haskell**. This is also used a +lot in the academic contexts we'll be working through. Its surface syntax +differs from Caml, and there are various important things one can do in +each of Haskell and Caml that one can't (or can't as easily) do in the +other. But these languages also have a lot in common, and if you're +familiar with one of them, it's not difficult to move between it and the +other. + + +[[How to get the programming languages running on your computer]] + +[[Family tree of functional programming languages]] + + +## Recommended Books ## + +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. + +* *An Introduction to Lambda Calculi for Computer Scientists*, by Chris +Hankin, currently $17 on +[Amazon](http://www.amazon.com/dp/0954300653). + +* (Another good book covering the same ground as the Hankin book, but +more thoroughly, and in a more mathematical style, is *Lambda-Calculus and Combinators: +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 +both the Hankin book and this book, you'll notice the authors made some different +terminological/notational choices. At first, this makes comprehension slightly slower, +but in the long run it's helpful because it makes the arbitrariness of those choices more salient.) + +* (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.) + +* *The Little Schemer, Fourth Edition*, by Daniel P. Friedman and Matthias +Felleisen, currently $23 on [Amazon](http://www.amazon.com/exec/obidos/ASIN/0262560992). +This is a classic text introducing the gentle art of programming, using the +functional programming language Scheme. Many people love this book, but it has +an unusual dialog format that is not to everybody's taste. **Of particular +interest for this course** is the explanation of the Y combinator, available as +a free sample chapter [at the MIT Press web page for the +book](http://www.ccs.neu.edu/home/matthias/BTLS/). + +* *The Seasoned Schemer*, also by Daniel P. Friedman and Matthias Felleisen, currently $28 +on [Amazon](http://www.amazon.com/Seasoned-Schemer-Daniel-P-Friedman/dp/026256100X) + +* *The Little MLer*, by Matthias Felleisen and Daniel P. Friedman, currently $27 +on [Amazon](http://www.amazon.com/Little-MLer-Matthias-Felleisen/dp/026256114X). +This covers some of the same introductory ground as The Little Schemer, but +this time in ML. It uses another dialect of ML (called SML), instead of OCaml, but there are only +superficial syntactic differences between these languages. [Here's a translation +manual between them](http://www.mpi-sws.org/~rossberg/sml-vs-ocaml.html). -More content added by git. -Enabled "lockedit" plugin: testing that admins can still edit pages. ---- +All wikis are supposed to have a [[SandBox]], so this one does too. + This wiki is powered by [[ikiwiki]]. + +