How can Prolog derive nonsense results such as 3 < 2?

Question

A paper I'm reading says the following:

Plaisted [3] showed that it is possible to write formally correct PROLOG programs using first-order predicate-calculus semantics and yet derive nonsense results such as 3 < 2.

It is referring to the fact that Prologs didn't use the occurs check back then (the 1980s).

Unfortunately, the paper it cites is behind a paywall. I'd still like to see an example such as this. Intuitively, it feels like the omission of the occurs check just expands the universe of structures to include circular ones (but this intuition must be wrong, according to the author).

---

I hope this example isn't

smaller(3, 2) :- X = f(X).

That would be disappointing.

Yevette

I used this link from Google Scholar and I downloaded full text in PDF without any problems (and I don't have any paid subscription, I've never bought one): idp.springer.com/authorize/casa?redirect_uri=https://… – Frontality

They still don't use occurs check. You have to be specific: unify_with_occurs_check/2. This means head unification by default never does occurs check. To switch it on globally: occurs check flag – Purim

Here is another nonsense result: ?- sort([X1,X2,X3],[3,1,2]). yields X1 = 3, X2 = 1, X3 = 2.. I'm going to write a new sort, I swear! – Purim

@GrzegorzAdamKowalski You probably have institutional subscription (colege IP address or something) – Yevette

@DavidTonhofer sort([X1,X2,X3],[3,1,2]) Bug? It's unaffected by set_prolog_flag(occurs_check, true). in SWI – Yevette

@MaxB en.wikipedia.org/wiki/Sci-Hub (and, en.wikipedia.org/wiki/Library_Genesis) – Abran

@MaxB Not a bug, it's according to ISO spec. It has nothing to do with the occurs check, but it's a mixup between a logical reading of sort/2 ("arg2 should be at least a possible result of sorting arg1") and the actual operational semantics according to which it is specified and implemented ("sort arg1 according to the standard order and then unify with arg2"). – Purim

Answer 1

Here is the example from the paper in modern syntax:

three_less_than_two :-
    less_than(s(X), X).

less_than(X, s(X)).

Indeed we get:

?- three_less_than_two.
true.

Because:

?- less_than(s(X), X).
X = s(s(X)).

Specifically, this explains the choice of 3 and 2 in the query: Given X = s(s(X)) the value of s(X) is "three-ish" (it contains three occurrences of s if you don't unfold the inner X), while X itself is "two-ish".

Enabling the occurs check gets us back to logical behavior:

?- set_prolog_flag(occurs_check, true).
true.

?- three_less_than_two.
false.

?- less_than(s(X), X).
false.

So this is indeed along the lines of

arbitrary_statement :-
    arbitrary_unification_without_occurs_check.

Castilian

A treacherous example, indeed. How can anyone turn the occurs check off after seeing this? – Yevette

If you actually wanted to define less-than on Peano numbers, you would write sonething more like less_than(0, s(_)). less_than(s(X), s(Y)).. The example is contrived, this isn't a problem one runs into all the time. – Castilian

For whatever it's worth, I'd also argue that Prolog's no-occurs-check semantics is not "using first-order predicate-calculus semantics", so the original paper is incorrect in interpreting Plaisted in this way. – Castilian

less_than(s(X), s(Y)). did you mean less_than(s(X), s(s(X))). ? Either way, Prolog still proves three_less_than_two. – Yevette

Oh sorry I left off the recursion. The second clause was meant to be less_than(s(X), s(Y)) :- less_than(X, Y). This enforces some structure on the arguments. In general, you rarely write predicates like the original "a completely arbitrary term is in a relation with itself with an extra s stuck on". – Castilian

This last version of less_than/2 loops: #65439788 – Yevette

Answer 2

I believe this is the relevant part of the paper you can't see for yourself (no paywall restricted me from viewing it when using Google Scholar, you should try accessing this that way):

Frontality

That's pretty weak sauce, because what is a "logic programming language" in "if Prolog is to be considered seriously" isn't even made clear. The author seem to confuse Prolog with a theorem prover. One can always only prove small parts of Prolog programs "formally correct". Once actual programming takes place, I/O occurs, random numbers are generated, and var(X) come into the play, not so much. – Purim

could you please re-type the relevant code from the paper as a textual valid Prolog code snippet. I can't understand it as written in the paper. – Abran

Interestingly, the discussed Prolog has integrity constraints: :- 3 < 2: (i.e. s(s(s(z))) < s(s(z))" 3 is never smaller than 2". This exists in ASP, but not Prolog. – Purim

@WillNess Old-school syntax. The first line is the query. The rest are the "program". The syntax for variables and constants is swapped. No predefined <. – Yevette

@MaxB The first line is the query? – Purim

@DavidTonhofer I think so. 3 < 2 is what we are trying to prove. – Yevette

Answer 3

Ok, how does the given example work?

If I write it down:

sm(s(s(s(z))),s(s(z))) :- sm(s(X),X).  % 3 < 2 :- s(X) < X
sm(X,s(X)).                            % forall X: X < s(X)

Query:

?- sm(s(s(s(z))),s(s(z)))

That's an infinite loop!

Turn it around

sm(X,s(X)).                            % forall X: X < s(X)
sm(s(s(s(z))),s(s(z))) :- sm(s(X),X).  % 3 < 2 :- s(X) < X

?- sm(s(s(s(z))),s(s(z))).
true ;
true ;
true ;
true ;
true ;
true 

The deep problem is that X should be Peano number. Once it's cyclic, one is no longer in Peano arithmetic. One has to add some \+cyclic_term(X) term in there. (maybe later, my mind is full now)

Purim