Continuing Sudoku 7
Your mission, should you choose to accept it, is to explain what the following code does:
class Amb
def initialize
@error = Exception.new("Ran out of possibilities")
@failure_continuation = lambda {|v| @error}
end
def assert(assertion)
if !assertion
self.fail
end
end
def deny(assertion)
assert !assertion
end
def fail
@failure_continuation.call(nil)
end
def maybe
one_of [true, false]
end
def one_of(collection = [])
k_prev = @failure_continuation
callcc do |k_entry|
collection.each do |item|
callcc do |k_next|
@failure_continuation = lambda do |v|
@failure_continuation = k_prev
k_next.call(v)
end
k_entry.call(item)
end
end
result = k_prev.call(nil)
if result == @error
raise @error.message
end
end
end
def all_values(&a_block)
k_prev = @failure_continuation
results = []
callcc do |k_retry|
@failure_continuation = lambda {|v| k_retry.call(false)}
results << a_block.call
k_retry.call(true)
end && fail
@failure_continuation = k_prev
results
end
end
Easy? Now explain how it does it.
Usage
Maybe if I show you how it’s used:
amb = Amb.new
a = amb.one_of(1..20)
b = amb.one_of(1..20)
h = amb.one_of(1..20)
amb.assert((a*a + b*b) == h*h)
puts "A triangle with sides #{a}, #{b} and #{h} has a right angle"
If you run that, you'll get:
@A triangle with sides 3, 4 and 5 has a right angle@
In English: we choose a number between 1 and 20. And then two more. Then we assert that the sum of the squares on two of the sides is equal to the square on the third and print the values. And we get the classic 3, 4, 5 Pythagorean triple. How did that happen? Where's the loops?
One clue might be to add a line like: @puts "#{a}:#{b}:#{h}"@ just before the @amb.assert(...)@ line. You'll see a whole pile of numbers spooling away until @a@, @b@ and @h@ reach the values @3@, @4@ and @5@ respectively. It seems that, between them, @Amb#one_of@ and @Amb#assert@ are hiding a depth first search.
Welcome to the weird and wonderful world of continuations. Let's take a look at a slightly simpler example and see if we can explain what's going on.
<code><pre>
amb = Amb.new
x = amb.one_of(1..10)
amb.assert(x > 5)
puts x # => 6
</pre></code>
Most of the magic happens in the implementation of @one_of@. Here's a heavily commented version of it:
<code><pre>
def one_of(collection)
# Capture the previous failure continuation. If we exhaust the collection we need
# somewhere else to fail to.
k_prev = @failure_continuation
# callcc sets a 'bookmark' that we can return to later. See below
# Essentially calling 'k_entry' resets the call stack to what it was when
# callcc got called, and makes it look as though callcc just returned
# that value.
callcc do |k_entry|
# loop through the collection
collection.each do |item|
# save our place in the loop. Taking the k_next continuation is akin to
# simply doing 'next', but you can do it from anywhere...
callcc do |k_next|
# Push a new failure 'continuation' on the fail stack. If #fail gets called
# this will restore the old failure continuation and resume the loop
@failure_continuation = lambda do |v|
@failure_continuation = k_prev
k_next.call(v)
end
# Instead of carrying on with the loop, we return the current item through
# the entry continuation. The loop will only get resumed if 'fail' gets called
k_entry.call(item)
end
# <== k_next points here
end
# If we get here, the loop has come to an end, we've got no more values, so we'll just
# take the old failure continuation.
result = k_prev.call(nil)
# If we get here, that means k_prev didn't take a continuation at all, which means we've
# completely run out of possibilities. So, if the return value is the @error fence we set up
# in initialise, we'll throw an exception.
if result == @error
raise @error.message
end
end
# <== k_prev points to here
end
</pre></code>
Essentially, @one_of@ iterates over the collection you pass it, but then freezes the iteration and 'proposes' the first value. Later on, an assertion (say @amb.assert(x > 5)@) might be false for the first value proposed. The assertion calls 'fail', which jumps back into @one_of@'s iteration, which proceeds to get the next value. @one_of@ effectively says "Did I say 1? Sorry about that. I meant 2, obviously. No? 3 then? 4? 5? 6!" and the program continues on its merry way.
Admittedly, it's not easy to understand how Amb[1] does its magic, but, frankly, most of the time that doesn't matter. You can use it to set up some remarkably complex searches without having to worry about any of the backtracking book keeping yourself.
It helps to have some idea of what's going on behind the scenes though, or you can end setting up a _huge_ search space when a bit of thought in choosing your conditions etc could pay off big time. For instance, say you wanted to find all the Pythagorean triples whose hypotenuse is <= 100. A simple minded setup would look like:
<code><pre>
amb = Amb.new
triples = amb.all_values do
a = amb.one_of(1..100)
b = amb.one_of(1..100)
h = amb.one_of(1..100)
amb.assert((a*a + b*b) = h*h)
[a,b,h]
end
</pre></code>
And it _would_ find all the pythagorean triples in that range. But it would consider some 1,000,000 cases, are @[3,4,5]@ and @[4,3,5]@ _really_ distinct?
A bit of thought gives:
<code><pre>
amb = Amb.new
triples = amb.all_values do
h = amb.one_of(1..100)
a = amb.one_of(1..(h-1))
b = amb.one_of(([a, h-a+1].max)..(h-1))
amb.assert((a*a + b*b) == h*h)
[a,b,h]
end
</pre></code>
Obviously, @a@ can't be longer than the hypotenuse, since the hypotenuse is, by definition the longest side of the triangle. The lower bound for @b@'s a little less obvious, but it derives from the fact that, in any triangle any side is shorter than the sum of the other two sides. However, @b@ should also be larger than @a@, that way we avoid checking 'mirror' cases.
Now, instead of searching 1,000,000 cases, we search 76,625, which is a substantial improvement don't you think?
I have to admit, finding Pythagorean triples isn't the reason I ported Amb from Squeak to ruby (not that it took that long), I ported it because I wanted to use it to solve Sudokus. I'm not going to post the Sudoku implementation just yet; it's in dire need of refactoring and clarification, but, following a first cut which would probably have kept on running 'til the heat death of the universe I have something which will do:
<code><pre>
s = Sudoku.new(<<EOS)
34.....28
.....19..
...64....
.....24..
51.....97
..61.....
....76...
..32.....
62.....39
EOS
puts "Solving Sudoku:"
puts s.unsolved_state
puts "Solution is:"
puts s.solution
</pre></code>
and get output like:
<code><pre>
Solving Sudoku:
3 4 . . . . . 2 8
. . . . . 1 9 . .
. . . 6 4 . . . .
. . . . . 2 4 . .
5 1 . . . . . 9 7
. . 6 1 . . . . .
. . . . 7 6 . . .
. . 3 2 . . . . .
6 2 . . . . . 3 9
Solution is:
3 4 1 7 9 5 6 2 8
7 6 5 8 2 1 9 4 3
2 8 9 6 4 3 1 7 5
8 3 7 9 5 2 4 1 6
5 1 2 4 6 8 3 9 7
4 9 6 1 3 7 8 5 2
9 5 4 3 7 6 2 8 1
1 7 3 2 8 9 5 6 4
6 2 8 5 1 4 7 3 9
</pre></code>
within a sensible amount of time. It's quite remarkable really; ruby's not the fastest of languages, and its continuations are far from the fastest bit of the language.
The great thing about this approach is that, because Amb handles the bookkeeping, I can concentrate on reducing the search space.
fn1. You will note, I'm sure that at no point do I explain what a continuation _is_. Mostly because, for the life of me, I can't find the words - it's all I can do to show you what they do.
