mukan
20 months agoMake the Bind iterator for AND goals fair develop
Cassie Jones [Mon, 17 Feb 2020 16:52:12 +0000 (17:52 +0100)]
Make the Bind iterator for AND goals fair

Given and(goal_a, goal_b), previously if goal_b could produce an
infinite number of solutions, then goal_a wouldn't get a chance to move
on the to previous. It was doing a sort of dependent Cartesian product
where it would take one step on goal_a in order to find the context for
goal_b, and then completely exhaust goal_b in that context.

Now, we do a diagonal search, keeping a vector of searches in goal_b,
and asking goal_a for a new context each time we loop back around to the
beginning. If goal_a is exhausted, we stop adding new searches, and if
any of the searches in goal_b is exhausted, we remove it from the list
of searches to iterate over.

Some specific things to note: we respect yields in goal_a, so that a
diverging goal_a doesn't get stuck and instead will repeatedly yield,
letting the rest of the program continue its search, interleaved
elsewhere.

This changes performance, making the large Peano addition slower.

20 months agoFormatting fix
Cassie Jones [Mon, 17 Feb 2020 16:10:34 +0000 (17:10 +0100)]
Formatting fix

20 months agoAllow goals to yield to other goals while working
Cassie Jones [Mon, 17 Feb 2020 14:23:35 +0000 (15:23 +0100)]
Allow goals to yield to other goals while working

Previously we searched over streams of states, that provided solutions
to the searched sub-goals. This meant though, that if you attempted to
search in a goal which couldn't make progress like the "unproductive"
rule below, it would block forever with no way to yield back to the rest
of the search without producing a wrong result.

  unproductive(X) :- unproductive(X).

The new search works via iterators over Step instead of over State,
where a Step::Working represents a goal which was unable to produce a
result, and instead decided to yield, and a Step::Soln(State) is a
solution like before.

Currently the only goal which will introduce new Working states into the
stream is the delay constructor, before forcing, since recursive goals
are the only non-terminating goals that are in the core.

20 months agoDerive Eq for Term for performance
Cassie Jones [Mon, 17 Feb 2020 13:15:59 +0000 (14:15 +0100)]
Derive Eq for Term for performance

Eq requires reflexivity, Arc<T: Eq> uses that fact to optimize the
equality check by first comparing the pointers. Unifying deep trees that
might use sharing, this could potentially give a performance benefit by
getting an early out in a deep tree.

20 months agoEvaluate larger peano for performance evaluation
Cassie Jones [Mon, 17 Feb 2020 12:03:23 +0000 (13:03 +0100)]
Evaluate larger peano for performance evaluation

This is mostly just changing the output format for it so that it doesn't
take up the entire screen even when running for the ways to sum to 100.

20 months agoChange Subst to store a single mapping for vars
Cassie Jones [Mon, 17 Feb 2020 11:41:24 +0000 (12:41 +0100)]
Change Subst to store a single mapping for vars

The previous implementation stored a Vector of values mapped, and adding
new mappings shadowed previous ones. I did it like this because the
implementation in the paper used association lists, which has this
shadowing effect. But, the implementation in Clojure simply uses a
dictionary like I'm using, and after doing these examples without seeing
shadowing, I'm convinced that it has the same behavior.

During this change, I also ended up changing a bunch of places with
cloning to pass references instead, which should cut down on reference
counting bookkeeping time.

20 months agoMove the terms out into a separate file
Cassie Jones [Mon, 17 Feb 2020 11:05:01 +0000 (12:05 +0100)]
Move the terms out into a separate file

The term is essentially purely user syntax, and has a decent chunk of
trait implementation boilerplate. It's nice to split it out from the
main chunk of the algorithm.

20 months agoAdd a README
Cassie Jones [Mon, 17 Feb 2020 01:09:56 +0000 (02:09 +0100)]
Add a README

20 months agoWhat a horrible night to have an initial commit
Cassie Jones [Sun, 16 Feb 2020 23:06:21 +0000 (00:06 +0100)]
What a horrible night to have an initial commit

This implements MicroKanren in Rust, based on the original paper:
http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

It's also informative to look at the "microLogic" implementation in
Clojure, which inspired the slightly cleaner unification style and
provides some ideas for what the extension points might need to be in
the future: https://mullr.github.io/micrologic/literate.html

This implementation is based around a "goal" trait, which can be asked
to search for solutions in a given state, producing a stream of new
states. Unlike the implementations above, we use Rust's Iterator trait
to implement the state streams. This might need to change in order to
enable "unproductive" steps in searching to be interleaved with other
searches. Potentially we should just change the iterator to use
Iterator<Item = Step> where Step values are Pending or Sat(State).

Goal is implemented for F: Fn(State) -> impl Iterator<Item = State>,
which means that you can write searches with functions. A goal that
wants to prove "true" would look like:

    |state: State| std::iter::once(state)

and a goal to prove "false" would look like:

    |state: State| std::iter::empty()

The functions and() and or() construct larger goals out of their
sub-goals, although they have more complicated implementations in order
to provide somewhat fair search. The and() goal constructor currently
doesn't produce a fair search, because if the second goal ever produces
infinite streams, then the first goal won't get a chance to advance.
This can be fixed, although it will involve allocation.

The delay() constructor is needed in order to produce recursive
procedures. It takes a thunk that produces a goal, and invokes it only
when it's first searched. Without this, recursive goals would
continually construct larger and larger goals forever. The Rust
implementation needs an additional consideration here: we have to box
the output Goal type. Most of the goal constructors return `impl Goal`
which gives an opaque type that incorporates its contents, including its
code. If you wrote a recursive procedure which directly incorporated
itself without a box in-between, it would have to have a type which
contained its own type, which means an infinite type.

This boxing issue is also what ended up complicating the Clone code.
Goals often need to be cloned, because they need to be able to be used
again and again during search, repeatedly constructing the derived
goals, but if we want a boxed goal that obscures the specific type, then
we needed to use `Box<dyn Goal>`, and so since Clone trait isn't
object-safe, it can't be used as a bound on Goal, and thus we need
`Goal: DynClone` so that the `Box<dyn Goal>` can implement Clone, and
also we need a to write Goal + Clone in lots of places because we need
both bounds.

Some of the constructors use Into<Term> in order to make writing
programs with the terms more convenient. Tuples become pair terms,
integers become literal terms, and variables are wrapped.