10

I am trying to write a toy logic programming query language, based on various sources of instruction including SICP and The Art of Prolog (AoP). I am just starting to work out my first sketch of the unification algorithm (the "heart of the computation model of logic programming" according to AoP), and AoP notes that

When implementing the unification algorithm for a particular logic programing language, the explicit substitution in both the equations on the stack and the unifier is avoided. Instead, logical variables and other terms are represented by memory cells with different values, and variable binding is implemented by assigning the memory cell representing a logical variable a reference to the cell containing the representation of the term the variable is bound to. (1st edition, p. 71)

Reading this made me realize that I only have a rough and practical grasp of how logical variables work, but I do not really understand how they are implemented. I'm not even sure what are the precise, formal characteristics that differentiate logical variable from the immutable variables that feature in other regions of the declarative programming paradigm. I will be grateful for all illuminating explanations and instructive references.

false
  • 10,264
  • 13
  • 101
  • 209
Shon
  • 3,989
  • 1
  • 22
  • 35
  • 1
    Maybe, cs.stackexchange.com is a better place to ask. – Roman Susi Nov 05 '15 at 07:39
  • 1
    @tobyodavies is right, SAT solvers are not central to Prolog-like, Turing complete programming languages. While there are different styles for logic programming, those are probably not what you are after. – Roman Susi Nov 05 '15 at 09:56
  • What will be your implementation language? – repeat Nov 05 '15 at 15:55
  • @repeat I'm working in SML, but I'm looking for general information about the nature of logical variables and strategies for implementation rather than language specific details. Maybe, for this reason, Roman Susi is right about this belonging in cs... – Shon Nov 05 '15 at 18:44

3 Answers3

5

Look up the Warren Abstract Machine if you want to understand how Prolog compilers and interpreters are implemented.

The basic idea for logic variables is that they are either bound to a term, free, or aliased to a different logic variable.

tobyodavies
  • 27,347
  • 5
  • 42
  • 57
  • I'm afraid my attempt to provide context might have caused some confusion (I'll edit to clear that up when I have a chance). I'm really only asking the question posed in the title. I'm not asking how to implement a Prolog compiler or interpreter. Do logic variables only make sense within the context of a Prolog-ish environment? I don't think so, but if so it would help to know why. In any case, I guess the WAM must have an implementation of logic variables I can study? – Shon Nov 06 '15 at 12:38
  • 1
    Logic variables only make sense in logic programming languages, where the WAM or something similar is the defacto-standard intermediate language. If you are doing anything with logic variables you will need a trail, the logic var itself (if you are using some functional language) is an algebraic data type with 3 states: bound (to some term of an appropriate term type), aliased (to another logic variable) and free. Unification changes this state and backtracting (popping the trail) reverts these state changes. – tobyodavies Nov 07 '15 at 07:09
  • This is *exactly* the kind of information I was looking for. Thanks! Given your remark on the necessity of an LP language for logic variables, do you have any thoughts on work such as this: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.1931 ? Would you see it as an FP language built on an LP language base? From what (little) I understand, a linear logic foundation seems to be decidedly different from the traditional LP paradigm... – Shon Nov 08 '15 at 01:28
2

Partial answer, concerning only the notion of logical variable.

A first approximation could be to say that logic variables act like math variables: once their value is learned, it will not change. That leads to the notion of assign-once variables. This contrasts with the notion of variables in imperative programming languages where they symbolically identify memory locations, allowing destructive (and thus) multiple assignment. But, going back to logic variables, it gets better. A logic variable can be unified with a term, but that term may itself contain variables. In turn, these variables can be further unified with other terms later. Consider the following example in Prolog:

?- V = a(Y).
V = a(Y).

?- V = a(Y), V = a(1).
V = a(1),
Y = 1.

In the second query, the variable V is further instantiated by unifying the variable it contains, Y, with the integer 1. The =/2 operator is Prolog unification operator. Unification is a logical operation that is true when you can take two terms and make them equal, possibly by binding variables in one term to a sub-term in the other term.

Paulo Moura
  • 18,373
  • 3
  • 23
  • 33
1

The main distinction in implementation are structure sharing vs structure copying. Googling for this brings many resources to attention...

In my Prolog interpreter, I've chosen structure sharing, so in unify it's apparent the kind of detailed handing required (well, it's a very simple mind approach): most of implementation is there, leaving to the service data structures BindStack and TrailStack just storing and little more... As consequence of my choices, an instantiated Term must be referenced together it's environment.

CapelliC
  • 59,646
  • 5
  • 47
  • 90
  • How do you do garbage collection in your Prolog interpreter? – repeat Nov 05 '15 at 15:56
  • @repeat: there is none, I mostly used findall, so terms were copied while 'produced' ... – CapelliC Nov 05 '15 at 16:07
  • 1
    @repeat: there are so many better Prolog out there... it's not worth to put any effort optimizing it, was just a case study. Nevertheless I actually used it to for some small job. – CapelliC Nov 05 '15 at 16:23