List unification problem

Discussions related to Visual Prolog
Martin Meyer
VIP Member
Posts: 290
Joined: 14 Nov 2002 0:01

List unification problem

Unread post by Martin Meyer » 7 Oct 2019 17:52

Hello Thomas,

please have a look at this code. It outputs "not unfiable" (in build 902).

Code: Select all

class predicates     test : (unsigned*, unsigned*). clauses     test(As, Bs) :-         if [As, [X]] = [[X], Bs] then             stdIO::write("unifies")         else             stdIO::write("not unfiable")         end if.   clauses     run() :-         test([1], [1]).
P.S. Have you seen unsigned64 bit operations?
Regards Martin

User avatar
Thomas Linder Puls
VIP Member
Posts: 1624
Joined: 28 Feb 2000 0:01

Re: List unification problem

Unread post by Thomas Linder Puls » 7 Oct 2019 22:40

Thank you.

In the correct processing X is first bound and later compared

But unfortunately the operations has been exchanged, so that X is first compared and then bound.
Regards Thomas Linder Puls
PDC

Harrison Pratt
VIP Member
Posts: 285
Joined: 5 Nov 2000 0:01

Re: List unification problem

Unread post by Harrison Pratt » 8 Oct 2019 11:16

This behaves similarly in VP 8.02

User avatar
Thomas Linder Puls
VIP Member
Posts: 1624
Joined: 28 Feb 2000 0:01

Re: List unification problem

Unread post by Thomas Linder Puls » 10 Oct 2019 11:23

Just out of curiosity, how did you discover this?

I find it very unusual to use unification like that. After all

Code: Select all

[As, [X]] = [[X], Bs]
is just a more obscure way to write:

Code: Select all

As = [X], [X] = Bs
Regards Thomas Linder Puls
PDC

Martin Meyer
VIP Member
Posts: 290
Joined: 14 Nov 2002 0:01

Re: List unification problem

Unread post by Martin Meyer » 11 Oct 2019 23:02

I have tried variations of my prior post, thereby I discovered it. I have even copied the wrong spelling 'unfiable' from there. :oops:

Another example of notorious code, where unification has a problem (in build 902), is:

Code: Select all

    open core   clauses     run() :-         A = 1,         tuple(tuple(A, A), tuple(B, B)) = tuple(B, C),         stdIO::write(C).
It works however when exchanging the sides of the unification:

Code: Select all

    open core   clauses     run() :-         A = 1,         tuple(B, C) = tuple(tuple(A, A), tuple(B, B)),         stdIO::write(C).
Regards Martin

Martin Meyer
VIP Member
Posts: 290
Joined: 14 Nov 2002 0:01

Re: List unification problem

Unread post by Martin Meyer » 12 Oct 2019 23:15

An example, which is obscure too, but cannot be de-obscured in same way as you have done above, is:

Code: Select all

    open core   class predicates     test : (unsigned X). clauses     test(X) :-         tuple(A, X) = tuple(B, B), % throws errors: Variables "A", "B" are not completely bound         stdIO::write(A, ", ", B).   clauses     run() :-         test(1).
Both A and B are free initially, thus it cannot be re-written as:

Code: Select all

    open core   class predicates     test : (unsigned X). clauses     test(X) :-         A = B, % illegal         X = B,         stdIO::write(A, ", ", B).   clauses     run() :-         test(1).
Of course it is easy to see that it can be de-obscured in another way:

Code: Select all

    open core   class predicates     test : (unsigned X). clauses     test(X) :-         X = B,         A = B,         stdIO::write(A, ", ", B).   clauses     run() :-         test(1).
But that other way is obvious only because the example is very small. We could pump the code up by using many variables and algebraic expressions instead of only A and B, so that we obtain a complicated example, for which it is by no means easy to figure out, how to de-obscure it.

Hence de-obscuring an obscure unification means, that the programmer is performing a substantial part of the unification-computation in advance. However we have the expectation that the system does all the unification-computation by itself.
Regards Martin

User avatar
Thomas Linder Puls
VIP Member
Posts: 1624
Joined: 28 Feb 2000 0:01

Re: List unification problem

Unread post by Thomas Linder Puls » 14 Oct 2019 10:46

It is obviously a bug that the compiler doesn't treat this correctly. And we will fix it (later :-)).
Regards Thomas Linder Puls
PDC

Post Reply