Logic variables and accompanying unification are such salient features of popular logic programming languages that logic programming seems inconceivable without them. The story of programming in logic without logic variables is dramatic, filled with theoretically inspired hopes dashed in practice. We show that although theoretical advances and improvements in the Hansei implementation are welcome, Hansei as it is is already capable of expressing the standard Prolog idioms, retaining their spirit. We can indeed do proper logic programming in Hansei: declaring relations and asking the system to find their model. Logic programming without logic variables should be obvious. The minimal model semantics of Prolog needs no logic variables; after all, Herbrand basis is by definition a set of ground atoms. The fixpoint construction (iterating the immediate consequence operator) gives the algorithm of finding the minimal model with no use for variables or unification. The reality dims the hope: although the fixpoint construction is viable for definite Datalog programs, it is difficult to perform when the Herbrand basis is infinite and the logic program contains negation and committed choice.

Two recent theoretical results in functional logic programming, Antoy and Hanus (2006) and Dios Castro and Lopez-Fraguas (2006), point out that logic variables and non-determinism due to overlapping rules have the same computational power. The main idea is representing a logic variable by a generator of its domain, with sharing of the generator expressing repeated occurrences of the variable. The idea is intuitively clear: a logic variable indeed stands for some term, non-deterministically chosen from a suitable domain. The papers derive a systematic transformation of a program with logic variables into the one without, while preserving the set of derivations. Alas, preserving the set of derivations (reductions) is a rather weak notion of program equivalence. For example, it does not account for the multiplicity of results, considering a program that yields, say, a single 0 equivalent to a program yielding the infinite sequence of 0s. In logic programming practice, we usually do distinguish such programs, valuing programs that produce a finite set of answers in finite time. The other drawback of the theoretical frameworks used in both papers is the inability to reason about finite failure. A logic program that returns “NO” in finite time and the program that loops forever are regarded as equivalent in these frameworks. In practice we consider such programs as very different. Since the papers are written as theoretical, the details about sharing and fairness of generators are sketchy.

Aware of the theoretical hopes and practical shortcomings, we decided to press ahead and see just how far we can go expressing standard Prolog idioms in a language without logic variables. Pending adequate theoretical analysis, empirical case studies seem the only choice. The present web page documents our results. The somewhat unexpected conclusion is that we go quite far. Hansei as it is appears suitable for logic programming.

We have gone back to Herbrand: we build the Herbrand universe (the set of all ground terms) and explore it to find a model of a program (that is, tuples of terms that model all declared relations). We build the universe by modeling logic variables' as generators for their domains. It greatly helps that Hansei is typed; the type of alogic variable’ specifies its domain and, hence, the generator. Since the Herbrand universe for most logic programs is infinite, we need non-strict evaluation. Furthermore, since logic variables may occur several times, we must be able to correlate the generators. Although Hansei is embedded in OCaml, which is strict, Hansei supports on-demand evaluated non-deterministic computations with sharing: so-called letlazy computations. Finally, since the search space is generally infinite, we need a systematic way of exploring it, without getting stuck in one infinite sub-region. Again Hansei provides a number of search strategies, including sampling and iterative deepening. (We shall use the latter in all our examples.)

Logic variables and unification have been introduced by Robinson as a way to `lift’ ground resolution proofs of Herbrand, to avoid generating the vast number of ground terms. Logic variables effectively delay the generation of ground terms to the last possible moment and to the least extent. Doing computations only as far as needed is also the goal of lazy evaluation. It appears that lazy evaluation can make up for logic variables, rendering Herbrand’s original approach practical.