From: Chris Date: Mon, 23 Feb 2015 18:02:39 +0000 (-0500) Subject: incorporated X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=afd5e8a2bbf0e38016e57652115230219d501782 incorporated discussion of Ty2 --- 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 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---included a simply-typed 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 (world-time -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 two-sorted +type theory. *Journal of Symbolic Logic* ***54.1***: 65--77 for a +precise characterization of the correspondence between IL and +two-sorted Ty2.] + +We'll need three base types: `e`, for individuals, `t`, for truth +values, and `s` for evaluation indicies (world-time 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 simply-typed 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 simply-typed lambda calculus the baseline +semantic analysis for linguistics.