From: Chris Date: Mon, 23 Feb 2015 16:39:21 +0000 (-0500) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=2306723f0538613e28d2adf8f8e69b744242c554 edits --- diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index 4b1bde56..71856f64 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -266,38 +266,39 @@ that even fairly basic recursive computations are beyond the reach of a simply-typed system. -## Montague grammar is a simply-typed +## Montague grammar is based on a simply-typed lambda calculus 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 +fragment---included a simply-typed version of the Predicate Calculus +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 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`. +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`. 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 . +* 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 . -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. +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.