From 40a9e529a03f11246b1f6fba8e98a670c4631639 Mon Sep 17 00:00:00 2001 From: Chris Date: Tue, 17 Feb 2015 16:56:13 -0500 Subject: [PATCH] edits --- topics/_week4_fixed_point_combinator.mdwn | 35 +++++++++++++++++++++++++------ 1 file changed, 29 insertions(+), 6 deletions(-) diff --git a/topics/_week4_fixed_point_combinator.mdwn b/topics/_week4_fixed_point_combinator.mdwn index b430f2fd..da2771a0 100644 --- a/topics/_week4_fixed_point_combinator.mdwn +++ b/topics/_week4_fixed_point_combinator.mdwn @@ -360,29 +360,52 @@ Works! Let's do one more example to illustrate. We'll do `K`, since we wondered above whether it had a fixed point. +Before we begin, we can reason a bit about what the fixed point must +be like. We're looking for a fixed point for `K`, i.e., `\xy.x`. `K` +ignores its second argument. That means that no matter what we give +`K` as its first argument, the result will ignore the next argument +(that is, `KX` ignores its first argument, no matter what `X` is). So +if `KX <~~> X`, `X` had also better ignore its first argument. But we +also have `KX == (\xy.x)X ~~> \y.X`. This means that if `X` ignores +its first argument, then `\y.X` will ignore its first two arguments. +So once again, if `KX <~~> X`, `X` also had better ignore at least its +first two arguments. Repeating this reasoning, we realize that `X` +must be a function that ignores an infinite series of arguments. +Our expectation, then, is that our recipe for finding fixed points +will build us a function that somehow manages to ignore an infinite +series of arguments. + h := \xy.x H := \f.h(ff) == \f.(\xy.x)(ff) ~~> \fy.ff H H := (\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff) -Ok, it doesn't have a normal form. But let's check that it is in fact -a fixed point: +Let's check that it is in fact a fixed point: K(H H) == (\xy.x)((\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff) Yep, `H H` and `K(H H)` both reduce to the same term. -This fixed point is bit wierd. Let's reduce it a bit more: +To see what this fixed point does, let's reduce it a bit more: H H == (\fy.ff)(\fy.ff) ~~> \y.(\fy.ff)(\fy.ff) ~~> \yy.(\fy.ff)(\fy.ff) ~~> \yyy.(\fy.ff)(\fy.ff) -It appears that where `K` is a function that ignores (only) the second -argument you feed to it, the fixed point of `K` ignores an endless, -infinite series of arguments. It's a write-only memory, a black hole. +Sure enough, this fixed point ignores an endless, infinite series of +arguments. It's a write-only memory, a black hole. + +Now that we have one fixed point, we can find others, for instance, + + (\fy.fff)(\fy.fff) + ~~> \y.(\fy.fff)(\fy.fff)(\fy.fff) + ~~> \yy.(\fy.fff)(\fy.fff)(\fy.fff)(\fy.fff) + ~~> \yyy.(\fy.fff)(\fy.fff)(\fy.fff)(\fy.fff)(\fy.fff) +Continuing in this way, you can now find an infinite number of fixed +points, all of which have the crucial property of ignoring an infinite +series of arguments. ##What is a fixed point for the successor function?## -- 2.11.0