From: Chris Barker Date: Sun, 3 Oct 2010 00:59:00 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=c3998b2b5a85bd4b5a47c1b2518739fe9948807f;hp=72af25c790aaa979710ffc2b7fab823ffaf94b05 edits --- diff --git a/week4.mdwn b/week4.mdwn index e01db2e8..8fe37ad2 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -192,11 +192,10 @@ are also forbidden, so recursion is neither simple nor direct. #Types# -We will have at least one ground type, `o`. From a linguistic -point of view, thing of the ground types as the bar-level 0 -categories, the lexical types, such as Noun, Verb, Preposition -(glossing over the internal complexity of those categories in modern -theories). +We will have at least one ground type, `o`. From a linguistic point +of view, think of the ground types as the bar-level 0 categories, that +is, the lexical types, such as Noun, Verb, Preposition (glossing over +the internal complexity of those categories in modern theories). In addition, there will be a recursively-defined class of complex types `T`, the smallest set such that @@ -218,7 +217,7 @@ and so on. #Typed lambda terms# -Given a set of types `T`, we define the set of typed lambda terms `&Lamda;_T`, +Given a set of types `T`, we define the set of typed lambda terms &Lamda;_T, which is the smallest set such that * each type `t` has an infinite set of distinct variables, {x^t}_1,