X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=8fe37ad2be182d92c8cc1298794ced2cc6a99b9d;hp=e01db2e857d5550eee64aa84f99860658b2fea47;hb=c3998b2b5a85bd4b5a47c1b2518739fe9948807f;hpb=72af25c790aaa979710ffc2b7fab823ffaf94b05 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,