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