]> Witch of Git - mukan/log
mukan
4 years 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.

4 years 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.

4 years 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.

4 years 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.

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

4 years 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.