January 09, 2013

The biggest problem I see right now with miniKanren is that its search is so hopelessly unguided. MiniKanren’s conde form uses what might be described as “breadth-first”[1] search (as opposed to Prolog’s depth-first approach). This works fine when you’re looking for shallow results, and it even provides a fairly resilient system: because we find shallow answers first, if shallow solutions exist we will find them quickly.

Motivation

Anyone with a few weeks’ education in AI can tell you that breadth-first search is almost always preferable to depth-first search; it’s a more general hammer, and far better as a tool in the general case. But it does break down, and it does so quite often. This is often discussed early on in introductory AI classes, and is soon discarded in favor of A-star search.

Soltuion

The problem with A-star search is that it requires a heuristic, and conde doesn’t lend itself well to this form. So I am writing this article to describe a new form, cond*, which does. The syntax is as follows:

(cond*
(heuristic goal*)
...)

Here, heuristic is a vanilla Scheme (or Clojure) lambda that takes some number of arguments (my thoughts might be a copy of the current substitution, the current search depth (by counting the number of bounces on the trampoline), and the number of ungrounded logic variables currently in existence). This heuristic will return a natural number, and these will be used to order the expansion of clauses.

Examples

To demonstrate, here are some examples:

> (run 1 (q)
(cond*
((lambda (s r f) 1) (== q #t))
((lambda (s r f) 2) (== q #f))))

(#t)

In this example, the first clause has a lower number than the second, so it is run first.

> (run 1 (q)
(cond*
((lambda (s r f) 2) (== q #t))
((lambda (s r f) 1) (== q #f))))

(#f)

In this example, the second clause has a lower number than the second, so it is run first.

Already, this has some nice implications for determining how clauses run (instead of manually reordering the lines themselves). But these priorities are not contained within a single cond*—they should span across every “thread” in the system. Here is another snippet:

> (define demo
(lambda (x)
(cond*
((lambda (s r f) (add1 r)) (demo x))
((lambda (s r f) 2) (== x #f))
((lambda (s r f) 1) (== x #t)))))

> (run 1 (q) (demo q))
(#t)

> (run 4 (q) (demo q))
(#t #t #f #f)

Here, the function uses its recursive depth as the priority value in its heuristic for two goals: the recursive call and the the (== x #f) goal. So the priorities of the goal clauses are as follows:

2 -> (demo x)
2 -> (== x #f)
1 -> (== x #t)

3 -> (demo x)
2 -> (== x #f)
1 -> (== x #t)

We can see that the priorities may be sorted, yielding the answer we got previously. This means that between calls, we can order our search. So if a branch finds a ‘more promising’ goal to try before a shallower branch, it will try the more promising one first!

With well-designed heuristics, we can get incredible control over how miniKanren explores its search space, ultimately yielding more interesting results when asking for only a few answers in a giant search space.

Applications

This idea was originally born when discussing using a miniKanren implementation of a type inferencer. By running a type inferencer backwards, you can get well-typed programs, but simple programs are found first—and there are a lot of simple programs. Using this model, you could, for example, rank answers of significant recursion depth as more promising than shallower answers, meaning that complex programs will be produces long before the shallow, “silly” programs.

Conclusion

I hope this gets added to miniKanren (and core.logic) one day. I’ve fiddled with the implementation before in hopes of adding it, but adding the inter-level recursion requires changing how the bind interacts with mplus, allowing bind to control the order in which mplus* advances goals. Maybe one day…

Footnotes

[1] It has also been said that miniKanren is closest to iterative deepening; I’m not certain, but my work with it seems to indicate that reasoning about conde as breadth-first search works just fine.

Using LaTeX for Programming Language Semantics

LaTex is a fantastic tool for typesetting, but there seem to be a serious gapin documentation for using it to lay out programming semanti...… Continue reading

A Small ALU in Haskell, Part I

Published on April 24, 2015

The Refined Gradual Guarantee and Compilation

Published on April 15, 2015