X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=bd3d8e5c6e0deac02d0954379f67b4d393ab2bc8;hp=ca6eb4ca12cbf35e5920a73434cf73da73c89f53;hb=ee659ed0921805be0db5de5658290b6dc1222eee;hpb=b496658969b421a22742f4d77317fef2f8928d7d diff --git a/week4.mdwn b/week4.mdwn index ca6eb4ca..bd3d8e5c 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -6,296 +6,56 @@ A: That's easy: let `T` be an arbitrary term in the lambda calculus. If `T` has a fixed point, then there exists some `X` such that `X <~~> TX` (that's what it means to *have* a fixed point). -
```-let W = \x.T(xx) in
-let X = WW in
-X = WW = (\x.T(xx))W = T(WW) = TX
-```
+
``````let L = \x. T (x x) in
+let X = L L in
+X ≡ L L ≡ (\x. T (x x)) L ~~> T (L L) ≡ T X
+``````
Please slow down and make sure that you understand what justified each of the equalities in the last line. -#Q: How do you know that for any term `T`, `YT` is a fixed point of `T`?# +#Q: How do you know that for any term `T`, `Y T` is a fixed point of `T`?# A: Note that in the proof given in the previous answer, we chose `T` -and then set `X = WW = (\x.T(xx))(\x.T(xx))`. If we abstract over -`T`, we get the Y combinator, `\T.(\x.T(xx))(\x.T(xx))`. No matter -what argument `T` we feed Y, it returns some `X` that is a fixed point +and then set `X = L L = (\x. T (x x)) (\x. T (x x))`. If we abstract over +`T`, we get the Y combinator, `\T. (\x. T (x x)) (\x. T (x x))`. No matter +what argument `T` we feed `Y`, it returns some `X` that is a fixed point of `T`, by the reasoning in the previous answer. #Q: So if every term has a fixed point, even `Y` has fixed point.# A: Right: - let Y = \T.(\x.T(xx))(\x.T(xx)) in - Y Y = \T.(\x.T(xx))(\x.T(xx)) Y - = (\x.Y(xx))(\x.Y(xx)) - = Y((\x.Y(xx))(\x.Y(xx))) - = Y(Y((\x.Y(xx))(\x.Y(xx)))) - = Y(Y(Y(...(Y(YY))...))) +
``````let Y = \T. (\x. T (x x)) (\x. T (x x)) in
+Y Y ≡ \T. (\x. T (x x)) (\x. T (x x)) Y
+~~> (\x. Y (x x)) (\x. Y (x x))
+~~> Y ((\x. Y (x x)) (\x. Y (x x)))
+~~> Y (Y ((\x. Y (x x)) (\x. Y (x x))))
+~~> Y (Y (Y (...(Y (Y Y))...)))``````
```-A(m,n) =
-    | when m == 0 -> n + 1
-    | else when n == 0 -> A(m-1,1)
-    | else -> A(m-1, A(m,n-1))
-
-let A = Y (\A m n. isZero m (succ n) (isZero n (A (pred m) 1) (A (pred m) (A m (pred n))))) in
-```
- -For instance, - - A 1 2 - = A 0 (A 1 1) - = A 0 (A 0 (A 1 0)) - = A 0 (A 0 (A 0 1)) - = A 0 (A 0 2) - = A 0 3 - = 4 - -A 1 x is to A 0 x as addition is to the successor function; -A 2 x is to A 1 x as multiplication is to addition; -A 3 x is to A 2 x as exponentiation is to multiplication--- -so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation... - -#Q. What other questions should I be asking?# - -* What is it about the variant fixed-point combinators that makes - them compatible with a call-by-value evaluation strategy? - -* How do you know that the Ackerman function can't be computed - using primitive recursion techniques? - -* What *exactly* is primitive recursion? - -* I hear that `Y` delivers the *least* fixed point. Least - according to what ordering? How do you know it's least? - Is leastness important? - - -##The simply-typed lambda calculus## - -The uptyped lambda calculus is pure computation. It is much more -common, however, for practical programming languages to be typed. -Likewise, systems used to investigate philosophical or linguistic -issues are almost always typed. Types will help us reason about our -computations. They will also facilitate a connection between logic -and computation. - -Soon we will consider polymorphic type systems. First, however, we -will consider the simply-typed lambda calculus. There's good news and -bad news: the good news is that the simply-type lambda calculus is -strongly normalizing: every term has a normal form. We shall see that -self-application is outlawed, so Ω can't even be written, let -alone undergo reduction. The bad news is that fixed-point combinators -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, 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 - -* ground types, including `o`, are in `T` - -* for any types σ and τ in `T`, the type σ --> - τ is in `T`. - -For instance, here are some types in `T`: - - o - o --> o - o --> o --> o - (o --> o) --> o - (o --> o) --> o --> o - -and so on. - -#Typed lambda terms# - -Given a set of types `T`, we define the set of typed lambda terms `Λ_T`, -which is the smallest set such that - -* each type `t` has an infinite set of distinct variables, {x^t}_1, - {x^t}_2, {x^t}_3, ... - -* If a term `M` has type σ --> τ, and a term `N` has type - σ, then the application `(M N)` has type τ. - -* If a variable `a` has type σ, and term `M` has type τ, - then the abstract `λ a M` has type σ --> τ. - -The definitions of types and of typed terms should be highly familiar -to semanticists, except that instead of writing σ --> τ, -linguists (following Montague, who followed Church) write <σ, -τ>. We will use the arrow notation, since it is more iconic. - -Some examples (assume that `x` has type `o`): - - x o - \x.x o --> o - ((\x.x) x) o - -Excercise: write down terms that have the following types: - - o --> o --> o - (o --> o) --> o --> o - (o --> o --> o) --> o - -#Associativity of types versus terms# - -As we have seen many times, in the lambda calculus, function -application is left associative, so that `f x y z == (((f x) y) z)`. -Types, *THEREFORE*, are right associative: if `f`, `x`, `y`, and `z` -have types `a`, `b`, `c`, and `d`, respectively, then `f` has type `a ---> b --> c --> d == (a --> (b --> (c --> d)))`. - -It is a serious faux pas to associate to the left for types. You may -as well use your salad fork to stir your tea. - -#The simply-typed lambda calculus is strongly normalizing# - -If `M` is a term with type τ in Λ_T, then `M` has a -normal form. The proof is not particularly complex, but we will not -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) - -Assume Ω has type τ, and `\x.xx` has type σ. Then -because `\x.xx` takes an argument of type σ and returns -something of type τ, `\x.xx` must also have type `σ --> -τ`. By repeating this reasoning, `\x.xx` must also have type -`(σ --> τ) --> τ`; and so on. Since variables have -finite types, there is no way to choose a type for the variable `x` -that can satisfy all of the requirements imposed on it. - -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. - -#Typing numerals# +
``````let succ = \n s z. s (n s z) in
+let X = (\x. succ (x x)) (\x. succ (x x)) in
+succ X
+≡ succ ( (\x. succ (x x)) (\x. succ (x x)) )
+~~> succ (succ ( (\x. succ (x x)) (\x. succ (x x))))
+≡ succ (succ X)
+``````
-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 `false` -has type τ --> τ --> &tau, for some τ. Since one is -represented by the function `\x.x false 0`, one must have type (τ ---> τ --> &tau) --> &sigma --> σ. But this is a different -type than zero! Because each number has a different type, it becomes -impossible to write arithmetic operations that can combine zero with -one. We would need as many different addition operations as we had -pairs of numbers that we wanted to add. +You should see the close similarity with `Y Y` here. -Fortunately, the Church numberals are well behaved with respect to -types. They can all be given the type (σ --> σ) --> -σ --> σ.