2

I am missing something in my reading of ISO/IEC 13211-1, subclauses 7.6.3 and 7.6.4:

7.6.3 Converting the head of a clause to a term

A head H with predicate indicator P/N can be converted to a term T:

a) If N is zero then T is the atom P.

b) If N is non-zero then T is a renamed copy (7.1.6.2) of TT where TT is the compound term whose principal functor is P/N and the arguments of H and TT are identical.

7.6.4 Converting the body of a clause to a term

A goal G which is a predication with predicate indicator P/N can be converted to a term T:

a) If N is zero then T is the atom P.

b) If N is non-zero then T is a renamed copy (7.1.6.2) of TT where TT is the compound term whose principal functor is P/N and the arguments of G and TT are identical.

c) If G is a control construct which appears in table 9 then T is a term with the corresponding principal functor. If the principal functor of T is call/1 or catch/3 or throw/1 then the arguments of G and T are identical, else if the principal functor of T is (',')/2 or (;)/2 or (->)/2 then each argument of G shall also be converted to a term.

Suppose we have a public (7.5.3) (e.g. dynamic) user-defined predicate a/1, defined by the following single clause:

a(X) :- b(X).

Clearly, the goal

?- clause(a(A), b(B)), A == B.

should succeed. Quoting part of the definition of clause/2 (8.8.1.1):

a) Searches sequentially through each public user-defined procedure in the database and creates a list L of all the terms clause(H, B) such that

1) the database contains a clause whose head can be converted to a term H (7.6.3), and whose body can be converted to a term B (7.6.4), and

2) H unifies with Head, and

3) B unifies with Body.

Converting the head of the above clause to a term, 7.6.3 b) applies, and we create a renamed copy a(A) of a(X). Similarly, converting the body of the clause, 7.6.4 b) applies, and we create a renamed copy b(B) of b(X).

The problem is that a(A) and b(B) are separate renamed copies. How is it required that A and B are identical variables, as we would expect?

The same question could be asked for a clause

p :- q(X), r(X).

When we convert the body of this clause to a term, 7.6.4 c) applies, and the principal functor of the term should be (',')/2, with the two arguments being the goals q(X) and r(X) converted to terms. But these are predications and 7.6.4 b) applies, so again the two resulting terms are separately renamed copies.

What am I missing?

5
  • 1
    Essentially, you are right. However, in 8.8.1.1 there is first a declarative description that explicitly mentions the term H :- B and the term Head :- Body that should unify. So here, the problem is avoided.
    – false
    Jun 5, 2016 at 18:39
  • @false: So is this a known issue? Is it likely to be fixed in a corrigendum? Jun 6, 2016 at 15:30
  • It is now known. In contrast to your previous find, this one is somewhat more serious. Yet, it most probably will be corrected after Cor.3.
    – false
    Jun 6, 2016 at 17:01
  • Thank you! I'm sorry I seem to keep finding such things. I hope this is the last one. Jun 6, 2016 at 17:17
  • That's fine! Who knows what you will find next!
    – false
    Jun 6, 2016 at 17:25

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.