From afd5e8a2bbf0e38016e57652115230219d501782 Mon Sep 17 00:00:00 2001
From: Chris
Date: Mon, 23 Feb 2015 13:02:39 0500
Subject: [PATCH] incorporated discussion of Ty2

topics/_week5_simply_typed_lambda.mdwn  43 ++++++++++++++++++++
1 file changed, 25 insertions(+), 18 deletions()
diff git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn
index 71856f64..e15a34d8 100644
 a/topics/_week5_simply_typed_lambda.mdwn
+++ b/topics/_week5_simply_typed_lambda.mdwn
@@ 272,33 +272,40 @@ Systems based on the simplytyped lambda calculus are the bread and
butter of current linguistic semantic analysis. One of the most
influential modern semantic formalismsMontague's PTQ
fragmentincluded a simplytyped version of the Predicate Calculus
with lambda abstraction.
+with lambda abstraction.
Montague called the semantic part of his PTQ fragment *Intensional
Logic*. Montague's IL had three base types: `e`, for individuals,
`t`, for truth values, and `s` for evaluation indicies (worldtime
pairs). The set of types was defined recursively:

 e, t, s are base types
+Logic*. Without getting too fussy about details, we'll present the
+popular Ty2 version of the PTQ types, roughly as proposed by Gallin
+(1975). [See Zimmermann, Ede. 1989. Intensional logic and twosorted
+type theory. *Journal of Symbolic Logic* ***54.1***: 6577 for a
+precise characterization of the correspondence between IL and
+twosorted Ty2.]
+
+We'll need three base types: `e`, for individuals, `t`, for truth
+values, and `s` for evaluation indicies (worldtime pairs). The set
+of types is defined recursively:
+
+ the base types e, t, and 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 we have 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 here as `a > b`.
+So `>` and `,t>>` are types. As we have 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 here as `a > b`. So the type `` is the type of a function
+that maps objects of type `a` onto objects of type `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 **, 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
.
+expression of type b, then *α(β)* has type *b*.
When we talk 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 simplytyped lambda calculus
the baseline semantic analysis for linguistics.
+* If α* is an expression of type *a*, and *u* is a variable of
+*type b*, then *λuα* has type
.
+When we talk about monads, we will consider Montague's treatment of
+intensionality in some detail. In the meantime, Montague's PTQ is
+responsible for making the simplytyped lambda calculus the baseline
+semantic analysis for linguistics.

2.11.0