X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=61033f5602f114fcbc33eb8ea03e6949733f3907;hp=e6bab7a1d8aafb2d4d70d0620851fe074e09da0d;hb=bfc18dfc2a8f9fee385b4f6f2b31fc99c155c728;hpb=ec55bd71ab1beda4348105a40324947d8753f4e3 diff --git a/week4.mdwn b/week4.mdwn index e6bab7a1..61033f56 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -1,9 +1,6 @@ [[!toc]] -#These notes return to the topic of fixed point combiantors for one more return to the topic of fixed point combinators# - -#Q: How do you know that every term in the untyped lambda calculus has -a fixed point?# +#Q: How do you know that every term in the untyped lambda calculus has a fixed point?# 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 <~~> @@ -171,3 +168,8 @@ so A 4 x is to A 3 x as hyper-exponentiation is to exponentiation... * 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? + +