Avik’s Ruminations

I’ve been reading Raymond Smullyan’s amazing book of puzzles, To Mock a Mockingbird. The book takes us on a journey around combinatorial logic, using the metaphor of birds. Obviously, my first reaction was that it would be interesting to follow along by implementing the  combinators in Ruby. So I’ve recently started doing just that.  (The code will be on my github)

After writing some basic combinators, I wanted to use them to demonstrate some of the solutions to the puzzles in the book. However, many of the proofs have an element of self-reference in them, and that quickly results in a stack overflow error in a procedural language without lazy evaluation.

For example, here is how Smullyan proves that given the existence of a composition operator $latex Cx = A(Bx)&s=-2$, and a Mockingbird $latex Mx = xx&s=-2$, there will exist a fixed point (or, in terms of the allegory of the book, a bird A is fond of bird B, when, if you call out B to A, A will call the same bird B back to you).

Take any bird A. Then there is a bird C that composes A with the Mockingbird M, since there exists a composition operator for all birds. Thus, for any bird x, Cx = A(Mx), or its equivalent, A(Mx) = Cx.  Since this holds for all birds x, we can substitute C for x, thus getting A(MC) = CC.  But MC = CC , by the definition of the Mockingbird M. Substituting, A(CC) = CC, which means A is fond of bird CC. QED.

Now if we convert this series of logical steps into Ruby, the point where we introduce self-reference, by applying C to itself, blows up with a stack overflow.

#Composition
Compose = lambda {| x, y|
    return lambda {|z|
    x.call(y.call(z))}
}

#The Mocking bird
M = lambda { |x| return x.call(x)}

#For any random lambda x
x=lambda { |x| return x }

c = Compose.call( b , M)
cc = c.call(c)  #Self reference, and stack overflow!
## Show b is fond of CC
assert ( b.call(cc) == cc )

Here is a situation where lazy evaluation would have made things work the way we would have expected it to. I suppose this could be fixed by wrapping things with another lambda, but we wouldn’t have to jump through hoops to follow a series of logical steps.

Taking this thought further, in the next chapter, Smullyan defines a fixed point combinator, calling it an oracle bird: $latex x(\Theta x) = \Theta x&s=-1$. A naïve translation to ruby once again, blows up with a stack overflow. (See here for a working Y combinator in ruby)

Y = lambda{ |x|
	x.call(Y.call(x))
}

However, the definition in Haskell is satisfyingly elegant.

y f = f (y f)