From: jim Date: Thu, 19 Feb 2015 15:24:56 +0000 (-0500) Subject: more formatting X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6ab7cbb2cf51690a92426413b1dced12fa8de3ea more formatting --- diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn index 4f2691e7..14bba4c9 100644 --- a/topics/_week4_fixed_point_combinator.mdwn +++ b/topics/_week4_fixed_point_combinator.mdwn @@ -457,23 +457,23 @@ more, non-equivalent fixed-point combinators.) Two of the simplest: -
Θ′ ≡ (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n))
-Y′ ≡ \f. (\u. f (\n. u u n)) (\u. f (\n. u u n))
+ Θ′ ≡ (\u f. f (\n. u u f n)) (\u f. f (\n. u u f n)) + Y′ ≡ \f. (\u. f (\n. u u n)) (\u. f (\n. u u n)) -Θ′ has the advantage that f (Θ′ f) really *reduces to* Θ′ f. Whereas f (Y′ f) is only *convertible with* Y′ f; that is, there's a common formula they both reduce to. For most purposes, though, either will do. +`Θ′` has the advantage that `f (Θ′ f)` really *reduces to* `Θ′ f`. Whereas `f (Y′ f)` is only *convertible with* `Y′ f`; that is, there's a common formula they both reduce to. For most purposes, though, either will do. -You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u f n` inside Θ′ to just `u u f`? And similarly for Y′? +You may notice that both of these formulas have eta-redexes inside them: why can't we simplify the two `\n. u u f n` inside `Θ′` to just `u u f`? And similarly for `Y′`? Indeed you can, getting the simpler: -
Θ ≡ (\u f. f (u u f)) (\u f. f (u u f))
-Y ≡ \f. (\u. f (u u)) (\u. f (u u))
+ Θ ≡ (\u f. f (u u f)) (\u f. f (u u f)) + Y ≡ \f. (\u. f (u u)) (\u. f (u u)) -I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of Θ (\self. BODY) and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will. +I stated the more complex formulas for the following reason: in a language whose evaluation order is *call-by-value*, the evaluation of `Θ (\self. BODY)` and `Y (\self. BODY)` will in general not terminate. But evaluation of the eta-unreduced primed versions will. -Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for Ψ in: +Of course, if you define your `\self. BODY` stupidly, your formula will never terminate. For example, it doesn't matter what fixed point combinator you use for `Ψ` in: -
Ψ (\self. \n. self n)
+ Ψ (\self. \n. self n) When you try to evaluate the application of that to some argument `M`, it's going to try to give you back: @@ -491,7 +491,7 @@ You've written an infinite loop! However, when we evaluate the application of our: -
Ψ (\self (\xs. (empty? xs) 0 (succ (self (tail xs))) ))
+ Ψ (\self (\xs. (empty? xs) 0 (succ (self (tail xs))) )) to some list `L`, we're not going to go into an infinite evaluation loop of that sort. At each cycle, we're going to be evaluating the application of: @@ -505,7 +505,7 @@ to *the tail* of the list we were evaluating its application to at the previous There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators. -I used Ψ above to stand in for an arbitrary fixed-point combinator. I don't know of any broad conventions for this. But this seems a useful one. +I used `Ψ` above to stand in for an arbitrary fixed-point combinator. I don't know of any broad conventions for this. But this seems a useful one. As we said, there are many other fixed-point combinators as well. For example, Jan Willem Klop pointed out that if we define `L` to be: @@ -635,17 +635,16 @@ sentence in which it occurs, the sentence denotes a fixed point for the identity function. Here's a fixed point for the identity function: -
Y I
-(\f. (\h. f (h h)) (\h. f (h h))) I
-(\h. I (h h)) (\h. I (h h)))
-(\h. (h h)) (\h. (h h)))
-ω ω
-&Omega
-
+ Y I + (\f. (\h. f (h h)) (\h. f (h h))) I + (\h. I (h h)) (\h. I (h h))) + (\h. (h h)) (\h. (h h))) + ω ω + Ω Oh. Well! That feels right. The meaning of *This sentence is true* in a context in which *this sentence* refers to the sentence in which -it occurs is Ω, our prototypical infinite loop... +it occurs is `Ω`, our prototypical infinite loop... What about the liar paradox? @@ -677,7 +676,7 @@ rather than recursive functions. You should be cautious about feeling too comfortable with these results. Thinking again of the truth-teller paradox, yes, -Ω is *a* fixed point for `I`, and perhaps it has +`Ω` is *a* fixed point for `I`, and perhaps it has some a privileged status among all the fixed points for `I`, being the one delivered by Y and all (though it is not obvious why Y should have any special status).