From c3998b2b5a85bd4b5a47c1b2518739fe9948807f Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sat, 2 Oct 2010 20:59:00 -0400 Subject: [PATCH] edits --- week4.mdwn | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) 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, -- 2.11.0