From d03fe382641cc8bc266184561d3c484deeb12ca1 Mon Sep 17 00:00:00 2001 From: Chris Date: Mon, 23 Feb 2015 11:25:14 -0500 Subject: [PATCH] added discussion of Montague's PTQ --- topics/_week5_simply_typed_lambda.mdwn | 37 ++++++++++++++++++++++++++++++++++ topics/_week5_system_F.mdwn | 4 ++-- 2 files changed, 39 insertions(+), 2 deletions(-) diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index 14e21729..4b1bde56 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -264,3 +264,40 @@ the structure of the Church numbers (and lists). Most importantly for the discussion of the simply-typed lambda calculus, it demonstrates that even fairly basic recursive computations are beyond the reach of a simply-typed system. + + +## Montague grammar is a simply-typed + +Systems based on the simply-typed lambda calculus are the bread and +butter of current linguistic semantic analysis. One of the most +influential modern semantic formalisms---Montague's PTQ +fragment---involved a simply-typed version of the Predicate Calculus +with lambda abstraction. More specifically, Montague called the +semantic part of the PTQ fragment `Intensional Logic'. Montague's IL +had three base types: `e`, for individuals, `t`, for truth values, and +`s` for evaluation indicies (world-time pairs). The set of types was +defined recursively: + + e, t, s are types + if a and b are types, is a type + if a is a type, is a type + +So `>` and `,t>>` are types, but `` is not a +type. As mentioned, this paper is the source for the convention in +linguistics that a type of the form `` corresponds to a +functional type that we will write `a -> b`. + +Montague gave rules for the types of various logical formulas. Of +particular interest here, he gave the following typing rules for +functional application and for lambda abstracts: + +* If *α* is an expression of type *a*, and *β* is an +expression of type b, then *α(β)* has type *b*. +* If *α* is an expression of type *a*, and *u* is a variable of +type *b*, then *λuα* has type . + +In future discussions about monads, we will investigate Montague's +treatment of intensionality in some detail. In the meantime, +Montague's PTQ fragment is responsible for making the simply-typed +lambda calculus the baseline semantic analysis for linguistics. + diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn index 684f42be..86f1c75b 100644 --- a/topics/_week5_system_F.mdwn +++ b/topics/_week5_system_F.mdwn @@ -18,10 +18,10 @@ System F is due (independently) to Girard and Reynolds. It enhances the simply-typed lambda calculus with quantification over types. In System F, you can say things like -`Γ α (\x.x):(α -> α)` +`Λ α (\x.x):(α -> α)` This says that the identity function maps arguments of type α to -results of type α, for any choice of α. So the Γ is +results of type α, for any choice of α. So the Λ is a universal quantifier over types. -- 2.11.0