From: Chris Date: Sun, 22 Feb 2015 14:46:45 +0000 (-0500) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=4d2c89f1c1993a93eeac0bf2887ad8cbbd94a937 edits --- diff --git a/topics/_week5_simply_typed_lambda.mdwn b/topics/_week5_simply_typed_lambda.mdwn index cee3f916..a2cb3f5f 100644 --- a/topics/_week5_simply_typed_lambda.mdwn +++ b/topics/_week5_simply_typed_lambda.mdwn @@ -174,23 +174,25 @@ To see this, consider the first three Church numerals (starting with zero): \s z . s (s z) Given the internal structure of the term we are using to represent -zero, its type must have the form ρ --> σ --> $sigma; for +zero, its type must have the form ρ --> σ --> σ for some ρ and σ. This type is consistent with term for one, but the structure of the definition of one is more restrictive: -because the first argument `s` must apply to the second argument `z`, -the type of the first argument must describe a function from -expressions of type σ to some other type. So we can refine ρ -by replacing it with the more specific type σ --> τ. At -this point, the overall type is (σ --> τ) --> σ --> +because the first argument (`s`) must apply to the second argument +(`z`), the type of the first argument must describe a function from +expressions of type σ to some result type. So we can refine +ρ by replacing it with the more specific type σ --> τ. +At this point, the overall type is (σ --> τ) --> σ --> σ. Note that this refined type remains compatible with the -definition of zero. Finally, by examinine the definition of two, we +definition of zero. Finally, by examinining the definition of two, we see that expressions of type τ must be suitable to serve as -arguments to functions of type σ --> τ. The most general +arguments to functions of type σ --> τ, since the result of +applying `s` to `z` serves as the argument of `s`. The most general way for that to be true is if τ ≡ σ. So at this -point, we have the overall type of (σ --> σ) --> σ --> -σ. - +point, we have the overall type of (σ --> σ) --> σ +--> σ. + ## Predecessor and lists are not representable in simply typed lambda-calculus ##