Pattern matching can be implemented using a point free style, and there are many articles on the internet about it. I'm wondering if the more generalized case also holds, i.e. is it possible to implement Prolog's unification in a point free language like J in a straight forward way.
Basically I want to know if there's any way to bridge the gap between point free languages and Prolog.
I’m not sure whether you’re more interested in the implementation of a unification procedure in J, or how unification could be expressed syntactically without logic variables, but I will touch on both, since they’re closely related.
MicroKanren in J: an Embedding of the Relational Paradigm in an Array Language with Rank-Polymorphic Unification(PDF) describes a basic implementation of a unification algorithm for an embedding of logic programming in J.
Unification is usually presented as the task of searching for a substitution under which the terms are equal, but the result isn’t really a general substitution, since the only terms we want to substitute are the metavariables. If we could replace any subterm, the problem would be a lot easier!
So we can also look at this as a proof-search task: our goal is to find a context, containing a set of bindings for the metavariables, which recursively equates the two input terms. We do this by contradiction: if we can prove no such context exists, then the terms don’t unify; if we can’t, the counterexample will be a context that unifies them.
In this J implementation, such a context is naturally represented as a boxed array, and a variable as an index into the same array, where an unbound variable points to its own index. This is a similar term representation to the Warren Abstract Machine, commonly used as the basis of Prolog implementations; you can find more examples in §2.1 of Warren’s Abstract Machine: A Tutorial Reconstruction(PDF).
Looking up a variable follows the chain of indices until reaching a fixed point, using the “do–while” construct with
^:_. It uses J’s preorder-traversal primitive “map”{::to flatten the input terms into a series of paths. A path that ends with a variable in one term is equated with the term at the corresponding path in the other term.This is an important insight: what it means to equate two terms structurally is that subterms are identified by their position. Named logic variables are only a concise way of specifying constraints among subterms.
So this also suggests a method of devising variable-free notations for unification, although I won’t go too deeply into this. Any term such as p(5, q(10), 15) can be described as a pair of its shape, with “gaps” for values, and a substitution that fills in those gaps: p(□, q(□), □)·[5, 10, 15]; the choice of traversal order is what allows assigning contents by position instead of by name.
For example, the Prolog-style unification f(X, f(X, g)) = f(h, Y) can be seen as a nested shape equation f(A, f(B, C)) = f(D, E), and a set of content equations {A = D, B = A, C = g, D = h, E = f(B, C)}. But again, it’s equally valid to view the shapes as unlabelled and flat, filled with content by index, and content equations separately as a vector of equivalence classes (indicated by the coloured shapes).
(Note that a substitution can also leave a gap unfilled, basically acting as the identity at that position.)