MiniKanren with finite-domain constraints in Java.
Logish is a Java 8+ implementation of miniKanren, an embedded sub-language (domain-specific language) for relational programming. Logish aims at emulating the key benefits of fully-fledged Constraint Logic Programming (CLP) systems based on Prolog in a Java-only environment at an acceptable performance.
-
Small and compact, single external dependency: Logish internally uses Java Vavr library for immutable functional data structures in Java.
-
Simple usage: for basic use it suffices to import static method
Logish.run, and all static members ofLogish.StdGoals. -
Queries return a
Streamof objects (no need to specify upfront how many solutions to look for). -
Constraint solving over finite (integer) domains, with linear constraints. The underlying mechanism for constraint solving are attributed variables, allowing coexistence of multiple constraint solvers.
import static org.cellx.logish.Logish.run;
import static org.cellx.logish.Logish.StdGoals.*;
public class MinimalLogish {
public static void main(String[] argv) {
run(q -> unify(q, "World"))
.forEach(o -> System.out.println("Hello, " + o + "!"));
}
}In this example, method run() executes a query over a logical variable
named q, and returns a stream of values for q that satisfy a
logical goal to the right of q ->. Here, the goal is unify(q, "World"), which unifies (asserts logical equality between)
the query variable q and string literal "World".
Technically, the argument to run() is a function that accepts a logic variable
created by run() and returns a goal that uses the variable(to the right of -> in
our example). What run() does next is to execute (i.e., try to satisfy) the goal,
which may result in zero or more solutions. For each solution, run() puts the
value of the logic variable in the resulting stream. This is done lazily: only when the
code accessing the stream tries to get the next element, the next solution of the goal
is computed. Since a goal may succeed infinitely many times, the resulting stream may
be infinite.
Java expression run(q -> unify(q, "World") can be read as a question: `Which values of q
make goal unify(q, "World") true?' The only solution for q is equal
to the string literal "World", and therefore resulting
stream of values for q has exactly one member. The program therefore prints
"Hello, World!" ands stops.
A logic variable is an instance of class Logish.Var. Like a
mathematical variable, it serves as a placeholder for a value (an
object). Unlike Java variables, a logic variable is not a mutable location in
memory that stores the value: after its value has become known, it
never changes. And it also differs from a final variable, because its value
is initially unknown and may become known only in the process of executing a logic goal.
In logic programming, and therefore in Logish, the
computation is effectively a search for values of the variables that
satisfy the goal.
As an example, a query:
run(q -> element(q, List.of(1, 2, 3)))
returns (a stream of) all values of variable q for which goal element(q, List.of(1, 2, 3)) succeeds. Note that List.of(1, 2, 3) is a Java
expression that creates an immutable list (an instance of
io.vavr.collection.List) whose elements are integers 1, 2, and 3. So, for
which q is this goal satisfied? There are three solutions: q=1, q=2,
and q=3, and so the resulting stream has three elements, 1, 2, and 3.
As in mathematics, logic variables remember when they refer to the same value: if we know that x=y, then as soon as we learn y=3, we automatically have x=3 as well. In the following query:
run(q -> fresh(x -> seq(unify(q, x), element(x, List.of(1, 2, 3)))))
we have two new elements. The first one is fresh(x -> G) that creates a
fresh variable x (with initially unknown value) and passes it to G. Next,
seq(G1, G2) is a composite goal that succeeds exactly
when both G1 and G2 succeed (one after another). Goal unify(q, x) has the same
meaning as q=x in mathematics, which is different from the meaning of =
(assignment) or == (object identity check) in Java. Since x=q, this query unsurprisingly
produces exactly the same solutions as the previous one.
Goal unify(X, Y) is technically called the unification of X and
Y. Unification behaves exactly as Java's java.util.Objects.equals(X, Y), except
for these three cases:
- When both X and Y are free variables. In this case, Logish proceeds by making sure that any mention of X is synonymous with Y and vice-versa.
- When X is a free variable, and Y is not. In this case Logish proceeds by making sure that any mention of X is synonymous with the value Y. The symmetrical case where Y is a free variable and X is not is treated analogously.
- When both X and Y are instances of a special class Logish.Cons. This is treated as structural unification, and will be described later in the text.
It is, of course, perfectly possible to satisfy the goal without instantiating the variable. For instance, query:
run(q -> success())
uses goal success() that always succeeds exactly once, which means that it
returns a stream with a single element. But what is that element like? It is
a logical variable corresponding to q itself (instance of Logish.Var),
whose toString() is "_0". This reflects the general rule: variables that
are instantiated are replaced by their values, while free variables remain in
the result. The non-negative integer following the underscore in the string
representation of a free variable (which can be obtained using method
Logish.Var.seq() on the variable) serves to globally distinguish distinct
variables in the result. The symbolic variable names, such as q, exist only
at Java compile time, and are not available at run-time.
Each run() query gives one variable "for free", which is reported back. As
seen before, if we need more variables, we can use fresh(). But, to make
fresh variables really usable, we need to look at Logish.Cons.
member(q -> fresh((x, y) -> seq(
element(x, List.of(-1, 0, 1)),
element(y, List.of(2, 3, 4)),