LING419 Categorial and Typelogical Grammars
In this course, we will discuss categorial approaches to natural language grammars, exploring the common core of a variety of different theories, together with their semantic components. We will then investigate some of the drawbacks that simple categorial grammars have, particularly in how they address common syntactic phenomena such as binding constraints and islands, and augment them with richer typetheoretic devices. In the process, we will become familiar with formal, prooftheoretic techniques using Natural Deduction and the Sequent Calculus.
Course Information
Lecture Notes
 A Proof Primer
 The proof primer contains a written up version of what we discussed on the first day of class, providing a quick and dirty introduction to proof systems via three toy systems.
 Chapters 12 (pp137) (B/W version)
 Chapter 1 sketches an overview of what "normal syntax" is like, and how it relates to CG/TLG. Chapter 2 provides an introduction to Natural Deduction for Intuitionistic Logic, as well as the Sequent Calculus for Intuitionistic Logic.
 Inference Rules Cheat Sheet for Chapter 2 (B/W version)
 The cheat sheet provides a list of all the inference rules, with no surrounding commentary or explanations, for reference when proving things. This version currently has only the inference rules for Natural Deduction (both the nonlocal and local versions), but I'll add the rules for the Sequent Calculus when we introduce them.
 Answer key for Chapter 2 (B/W version)
 This provides answers to the proof problems from chapter 2.
 Chapter 3 (B/W version)
 Chapter 3 introduces the Associative Lambek Calculus
Team Project
Resources
 OPLSS 2012 videos
 Frank Pfenning has great lectures that are worth looking at.
Homework, Readings, and Prep Exercises
 Reading 1 and Prep Exercise 1 (due 9 Sep 2013)
 Read up to page 8 in the lecture notes. Do exercises 2.1.3 #1 and #2. Send at least one question to me before class.
 Reading 2 and Prep Exercise 2 (due 11 Sep 2013)
 Read pages 9 to 11, and also 13 to 15. Send at least one question to be before class by 1pm.
 Reading 3 and Prep Exercise 3 (due 16 Sep 2013)
 In class, we proved that from an assumption of (A ∧ B) ∧ C we could derive A ∧ (B ∧ C). Prove the reverse.
 Prove that from an assumption of (A → B) → C we can derive A → B → C. Provide a partial proof of the reverse, going as far as you can get, and showing that you get stuck.
 Do 2.2.4 #7, #8ad, #9a, #10ab, #11a.
 Send questions!
 Reading 4 and Prep Exercise 4 (due 23 Sep 2013)
 Read the intro to section 2.3, and also subsections 2.3.12.3.5 (pp2030). Send questions.
 Prep Exercise 5 (due 25 Sep 2013)
 Prove the following using proof terms (that is to say, give proofs that let you fill in proof terms for the ?'s):
 ⊢ ? : (A → B) → A ∧ C → B ∧ C
 ⊢ ? : (A → B) → A ∨ C → B ∨ C
 Check that the following proof terms do in fact prove the given propositions:
 ⊢ λp.〈snd p, fst p〉: A ∧ B → B ∧ A
 ⊢ λd. case d of { inl x ↦ inr x ; inr y ↦ inl y } : A ∨ B → B ∨ A
 Redo exercise 2.2.4 #10 using proof terms.
 Prove any 3 propositions from 2.2.4 #8 (fq).
 Do exercise 2.3.7 #15 and #16.
 Prove the following using proof terms (that is to say, give proofs that let you fill in proof terms for the ?'s):
 Reading 6 (due 2 Oct 2013) and Homework 1 (due 7 Oct 2013)
 Read section 2.3.6 and send questions.
 Do homework 1 (B/W version).
 Reading 7 (due 7 Oct 2013)
 Read section 2.4 (you can ignore the rules for ∨ and ⊥). Try to do some proofs using this system, e.g. 2.4.4 #20a/b. You don't have to turn anything in, but practice will be useful for the class discussion.
 Midterm (due 21 Oct 2013)
 Do the midterm (B/W version)
 Reading 8 and Prep 6 (due 23 Oct 2013)
 Read pages 3844 of chapter 3, do the exercises in section 3.2.2, and send questions.
 Reading 9 (due 28 Oct 2013)
 Read section 3.3 (pp4448).
 Reading 10 and Prep 7 (due 4 Nov 2013)
 Read section 3.4 (pp4850), do exercise 30 in 3.4.2.
 Homework 2 (due 6 Nov 2013)
 Do exercise 31 in 3.4.2.
 Reading 11
 Read section 3.5.
 Prep 8 (due 18 Nov 2013)

 Give axioms and a proof for the syntax/semantics of the sentence "Sinclair gave the pilot an order".
 What might we want to say the axiom for "skillfully" is, to make sense of the sentence "Ivanova flew the Starfury skillfully"? Be sure to consider the semantics.
 Consider the following sentences: "Sinclair and Ivanova spoke", "Ivanova met each and every ambassador", "Ivanova met and greeted the ambassadors", "Sinclair travelled to and from the station". If 'Sinclair' and 'Ivanova' are both NP's, 'each' and 'every' are both NP/N's, 'greeted' and 'met' are both (NP\S)/NP's, and 'to' and 'from' are both ((S\NP)\(S\NP))/NP's, it would seem we need multiple 'and's for each imaginable type. Can we assign a single type to 'and' that works for all of these?