2

A quick and simple question regarding what role anonymous variables play in the resolution of a Prolog query given a set of program rule. So, the way I understand how the simplest form of SLD resolution works, an SLD tree is constructed by taking some term from a set of goal terms (based on a selection rule, e.g. FIRST) and going through all the program rules to see which rule's left hand side (the consequent, so to say) can be unified with the term at hand. The way to unify two given terms is to take a difference set of two terms and see if variables can be substituted for terms such that the difference vanishes, you do this by successively taking the leftmost single difference and checking if, out of the two sets constituting the difference, one is a variable not appearing in the other and composing your current substitution with one mapping the variable onto the term (starting with the empty or identity substitution).

Now, when anonymous variables (_) come into play, I suspect the trick in doing it correctly and efficiently lies in changing the way you determine the leftmost difference between two terms to ignore a pair of terms whenever one of them is an anonymous variable. The obviously correct way to do it would be to rename every instance of _ in the goal and the program set to a new variable name and solve using those.

How is it actually done? Is my idea sufficient, or is there more to it than that? (Also, would appreciate it very much if something is missing in the way I understand SLD resolution works, barring negation, call, capsuling, arithmetic predicates and the more complicated stuff.)

Guy Coder
  • 24,501
  • 8
  • 71
  • 136
sanik98
  • 145
  • 6
  • In the reading the question you made me think. I don't believe that SLD resolution has the concept of an anonymous variable. If so then the task falls to the implementation such as Prolog and in there the choice of what binds to the anonymous variable is based on position in the term. Also anything can unify with an anonymous variable, but IIRC there is something of note when two of them unify. Take this with a grain of salt and I did not check all of this, but is what I recall off the top of my head, and thus the reason it is a comment. – Guy Coder Mar 05 '20 at 15:33
  • You might consider changing the title. It says `Prolog` but the question is more about `SLD resolution`. – Guy Coder Mar 05 '20 at 15:39
  • If terms bind to anonymous variables, then they need to be renamed so as to prevent a clash in case several are used in a Term, etc. But does the unifying substitution just leave them be when the only difference between two terms is that one has _ at some position and the other a whole term? But if SLD resolution has no concept of anonymous variables whatsoever, then the sensible thing to do would be to rename all anon. variables so as to eliminate them come SLD resoltion, is that correct? – sanik98 Mar 06 '20 at 08:01
  • My question relates specifically to how Prolog internally interprets _, though. Maybe I shouldn't have emphasized SLD resolution... – sanik98 Mar 06 '20 at 08:03
  • If you need a more technical explanation, then you can look at the instructions of the WAM. See: [Warren’s Abstract Machine - A Tutorial Reconstruction](http://wambook.sourceforge.net/wam-slides.pdf) Search for `anonymous variable`. – Guy Coder Mar 06 '20 at 09:10
  • In reading the ISO specification for Prolog, it states. `a) V is a set of variables such that for each form of variable token` then 3 specifics with `3) Every anonymous variable corresponds to a different member of V.` However since this is just a specification, I have no way of knowing how each Prolog implements an anonymous variable, but it in general one would think that a Prolog implementation would make each anonymous variable a different variable if they are adhering to the ISO Prolog specification. – Guy Coder Mar 06 '20 at 09:20
  • imagine that every `_` is renamed to an arbitrary unique name *before* Prolog starts working. that's all there is to it. – Will Ness Mar 06 '20 at 15:27
  • Thanks a lot, that answers my question outright. – sanik98 Mar 07 '20 at 10:47

2 Answers2

4

Prolog anonymous variables don't play a role in SLD resolution or in term unification but do play a practical role in Prolog code and Prolog queries. A fundamental aspect of anonymous variables is that each occurrence of an anonymous variable is a different variable. Consider the following query:

| ?- a(_, _) = a(1, 2).

yes

The unification would have failed if the two anonymous variables were the same variable. Now consider the query:

| ?- a(X, _) = a(1, 2).

X = 1
yes

Variable bindings are only reported for variables that are not anonymous variables. This allows using an anonymous variable everytime we are not interested in any bindings for a variable.

Anonymous variables also simplify writing predicate definitions where they similarly act as "don't care" variables. Consider as an example the usual definition of the member/2 predicate:

member(Element, [Element| _]).
member(Element, [_| List]) :-
    member(Element, List).

In the first clause, we don't care about the list tail. In the second clause, we don't care about the list head. By using anonymous variables, we can ignore those sub-terms and avoid the compiler complaining about variables that would be used once in a clause.

Update

Note that all different variables in a query get unique internal variable references, not to be confused with variable names as typed by the user. The variables names are only used by the top-level interpreter to report bindings for successful queries. The inference mechanism used to prove a query use the variable (internal) references. The following query, using the ISO Prolog standard read_term/2 predicate with standard options may help:

| ?- read_term(Term, [variable_names(Names), variables(Variables)]).
a(X, _, Y, _).

Names = ['X'=A,'Y'=B]
Term = a(A,C,B,D)
Variables = [A,C,B,D]

yes

In the term read, there are four distinct variables but only two of them have (user provided) names.

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

This is a comment in an answer because a comment can not format this as needed.

Using SWI-Prolog

?- trace,(_=_).
   Call: (11) _1834=_1836 ? creep
   Exit: (11) _1834=_1834 ? creep
true.

Each anonymous variable is created as a separate variable. When the unification takes place the one variable is unified with the other variable.

Guy Coder
  • 24,501
  • 8
  • 71
  • 136