From 17263ec6b2caa7baca47bb3739fa9826f6e420ee Mon Sep 17 00:00:00 2001 From: Chris Date: Sat, 21 Feb 2015 18:27:46 -0500 Subject: [PATCH] edits --- topics/_week5_simply_typed_lambda.mdwn | 43 ++++++++++------------------------ 1 file changed, 13 insertions(+), 30 deletions(-) diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index 1fedd2a3..b1b4d932 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -54,11 +54,10 @@ tells us that "The simple theory of types was suggested as a modification of Russell's ramified theory of types by Leon Chwistek in 1921 and 1922 and by F. P. Ramsey in 1926." This footnote appears in Church's 1940 paper [A formulation of the simple theory of -types](church-simple-types.pdf). In this paper, as Will Starr -mentioned in class, Church does indeed write types by simple -apposition, without the ugly angle brackets and commas used by -Montague. Furthermore, he omits parentheses under the convention that -types associated to the *left*---the opposite of the modern +types](church-simple-types.pdf). In this paper, Church writes types +by simple apposition, without the ugly angle brackets and commas used +by Montague. Furthermore, he omits parentheses under the convention +that types associated to the *left*---the opposite of the modern convention. This is ok, however, because he also reverses the order, so that `te` is a function from objects of type `e` to objects of type `t`. Cool paper! If you ever want to see Church numerals in their @@ -147,7 +146,7 @@ present it here; see Berendregt or Hankin. Since Ω does not have a normal form, it follows that Ω cannot have a type in Λ_T. We can easily see why: - Ω = (\x.xx)(\x.xx) +Ω = (\x.xx)(\x.xx) Assume Ω has type τ, and `\x.xx` has type σ. Then because `\x.xx` takes an argument of type σ and returns @@ -161,36 +160,19 @@ In general, there is no way for a function to have a type that can take itself for an argument. It follows that there is no way to define the identity function in such a way that it can take itself as an argument. Instead, there must be many different identity -functions, one for each type. +functions, one for each type. Some of those types can be functions, +and some of those functions can be (type-restricted) identity +functions; but a simply-types identity function can never apply to itself. #Typing numerals# -Version 1 type numerals are not a good choice for the simply-typed -lambda calculus. The reason is that each different numberal has a -different type! For instance, if zero has type σ, then since -one is represented by the function `\x.x false 0`, it must have type -`b --> σ --> σ`, where `b` is the type of a boolean. But -this is a different type than zero! Because each number has a -different type, it becomes unbearable to write arithmetic operations -that can combine zero with one, since we would need as many different -addition operations as we had pairs of numbers that we wanted to add. +The Church numerals are well behaved with respect to types. They can +all be given the type (σ --> σ) --> σ --> σ. -Fortunately, the Church numerals are well behaved with respect to -types. They can all be given the type (σ --> σ) --> -σ --> σ. - - - -- 2.11.0