Simple and Fair Backtracking Computations

Translated to F# from the fair and terminating backtracking monad and monad transformer by Oleg Kiselyov.

Sequence expressions in F# can be seen as backtracking computations. For example,

let backtrack =
    seq {   for i in 1..10 do
            for j in 1..10 do
            if i*j > 10 then yield (i,j) }

will yield one by one (i.e. lazily) all the tuples i,j that satisfy the guard i*j>10. In Haskell, you would use list comprehensions to much the same effect. Once the values of j are exhausted for a given i, the computation backtracks, takes the next value for i and retries all values for j. Don’t mistake the syntactic sugar for nested loops  – there is really a computation builder behind this that translates to something like

1..10 >>= (fun i –> 1..10 >>= (fun j –> …))

where (>>=) represents monadic bind. This translations shows more clearly that the binds are really doing backtracking. It’s just F#’s syntactic sugar for computation expressions that makes the computation look like a nested loop.

Unfortunately, this simplicity has some drawbacks.

let infinite =
    seq {   for i in 1..10 do
            for j in Seq.initInfinite id do
            if i > 5 then yield (i,j) }

will never return any results, although there is an infinite number of solutions. The reason is that generation gets stuck on j – an infinite stream that will never yield a solution as long as the computation does not backtrack and tries new values for i. The computation is unfair in its choice of values to try – it always chooses the last stream until that is exhausted.

The thing to realize is that, if viewed as a backtracking computation, there are basically two operations that are important: choice and bind.

Choice gives the computation a range of elements to choose from. In the example above, we have an element i that can be chosen from the interval [1,10] and an element j that can be chosen from the interval [0,Infinity]. It can be viewed as logical disjunction: for i, choose 1 or 2 or 3 or 4 or…

Bind gives the computation a number of sub-computations that all need to return a value if the complete computation is to return a value. It can be understood as logical conjunction: in the example above, i should be chosen from [1,10] and j should be chosen from [0,Infinity] and i should be > 5.

Theoretically, it does not matter in which order these kinds of generate-and-test computations are executed. However, for performance and once you start using infinite streams, it becomes important that the computation is fair – in the sense that the choices it makes give every option consideration, even if once choice has not been exhausted yet. The results of all backtracking computations should be equivalent modulo the order in which the results are returned.

So, can we make an alternative computation builder for which this kind of computation returns results?

Fair streams

Let’s start by making a new datatype of streams, that we can use to make fairer choices, and that also can be suspended so that infinite streams can be supported:

type Stream<'a> = 
    | Nil                               //empty
    | One of 'a                         //one element
    | Choice of 'a * Stream<'a>         //one element, and maybe more
    | Incomplete of Lazy<Stream<'a>>    //suspended stream

 

Using this stream, we can code a fair choice function:

let rec choice r r' = 
    match r with
    | Nil -> r' //first empty-> try the second
    | One a -> Choice (a,r') //Put in front of the new stream
    | Choice (a,rs) -> Choice (a,choice r' rs) //interleave r and r' here
    | Incomplete i ->
        match r' with
        | Nil -> r
        | One b -> Choice (b,r)
        | Choice (b,rs') -> Choice (b,choice r rs') 
        | Incomplete j -> Incomplete (lazy (choice i.Value j.Value))

The important thing here is the switch of argument order in the recursive call to choice in the third case. This ensures that, in contrary to normal sequences, a choice will choose alternatively from the first and second stream (and so on, recursively, for more streams). Choice is actually somewhat equivalent to concatenate on sequences, only it interleaves the elements so that the choice is fair.

Bind is more straightforward:

let rec bind m f =
    match m with
        | Nil -> Nil
        | One a -> (f a)
        | Choice (a,r) -> choice (f a) (Incomplete (lazy bind r f))
        | Incomplete i -> Incomplete (lazy bind i.Value f)

This is what you would expect from a normal monadic bind on a list like type: a variant of map – concat on each element of the first stream. Note in the third case that we take care to encode the resulting stream as a number of choices that we can choose from fairly.

We now have the important elements to make a computation builder:

type FairStream() =
    member x.Return a = One a
    member x.Yield a = One a
    member x.Bind (m, f) = bind m f
    member x.Zero() = Nil
    member x.Combine (r,r') = choice r r'
    member x.Delay (f:unit->Stream<_>) = Incomplete (Lazy.Create f)

   
let bt = FairStream()

I called it bt, short for backtracking. Now we need a function to run our computation:

let rec run d st =
    match (d,st) with
    | _,Nil -> Seq.empty
    | _,One a -> seq { yield a }
    | _,Choice (a,r) -> seq { yield a; yield! run d r }
    | Some 0,Incomplete i -> Seq.empty //exhausted depth
    | d,Incomplete (Lazy r) -> let d' = Option.map ((-) 1) d in run d' r

The run function takes an optional parameter to bound the number of backtracking steps, which may be useful to help with termination.

A few examples

First, let’s define a stream of numbers [0,Infinity]:

let rec number() = bt { yield 0
                        let! n = number() in yield n+1 }

Nothing really amazing here – you could do something similar with sequences as well. However, if we use the choice constructor explicitly, we can define number as a left-recursive function:

let rec number() = choice (bt { let! n = number() in return n+1 }) (bt {return 0})

Both number functions yield the same results.

Now for something a bit more spectacular.

let guard assertion = 
    bt { if assertion then return () }

let pythagoreanTriples =
    bt{ let! i = number()
        do! guard (i > 0)
        let! j = number()
        do! guard (j > 0) 
        let! k = number()
        do! guard (k > 0)
        do! guard (i*i + j*j = k*k)
        return (i,j,k) }

This computation will never yield any results in a standard sequence expression, but with the fair streams it works, even if you leave off the guards.

The discerning reader might wonder why we can’t write:

let rec number() = 
    bt { let! n = number() in return n+1
         return 0 }

which is a left recursive version in a computation expression style. I don’t know the answer myself – some details are lost in the translation to the methods on the computation builder, but I’m guessing it has something to do with the bind not being lazy enough, and/or the choice function not getting inserted in the appropriate place. I’ve tried various approaches, but couldn’t get it to work. So I guess there’s some homework for you :) In the mean time, I think I’m going to work through Backtracking, Interleaving, and Terminating Monad Transformers by Kiselyov et al…

Technorati: F#,computation builder,backtracking,monads

Share this post :

Technet!

del.icio.us it!

del.iri.ous!

digg it!

dotnetkicks it!

reddit!

technorati!