Logish

MiniKanren with finite-domain constraints in Java.

Introduction

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.

Features

• 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 of Logish.StdGoals.

• Queries return a Stream of 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.

Basic use

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.

Logic variables and goals

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.

Unification

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.

Consing

member(q -> fresh((x, y) -> seq(
        element(x, List.of(-1, 0, 1)),
        element(y, List.of(2, 3, 4)),