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.

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): https://idp.springer.com/authorize/casa?redirect_uri=https://link.springer.com/content/pdf/10.1007/BF03037324.pdf&casa_token=DwsqZYgeQgAAAAAA:UpyWfidKd0K9iwRXf2PQR6UlQVIeSTm6gCxg_e82RLZ00TLWeGks8bbYrSt0KRHEc0WWkOxG_W245mdt — Grzegorz Adam Kowalski, Dec 13 '20 at 12:01
They still don't use occurs check. You have to be specific: [`unify_with_occurs_check/2`](https://eu.swi-prolog.org/pldoc/doc_for?object=unify_with_occurs_check/2). This means head unification by default never does occurs check. To switch it on globally: [occurs check flag](https://eu.swi-prolog.org/pldoc/man?section=flags#flag:occurs_check) — David Tonhofer, Dec 13 '20 at 12:22
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! — David Tonhofer, Dec 13 '20 at 12:24
@GrzegorzAdamKowalski You probably have institutional subscription (colege IP address or something) — MWB, Dec 13 '20 at 12:38
@DavidTonhofer `sort([X1,X2,X3],[3,1,2])` Bug? It's unaffected by `set_prolog_flag(occurs_check, true).` in SWI — MWB, Dec 13 '20 at 12:49
@MaxB https://en.wikipedia.org/wiki/Sci-Hub (and, https://en.wikipedia.org/wiki/Library_Genesis) — Will Ness, Dec 13 '20 at 12:50
@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"). — David Tonhofer, Dec 13 '20 at 13:00

score 6 · Accepted Answer · answered Dec 13 '20 at 12:39

6

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.

answered Dec 13 '20 at 12:39

Isabelle Newbie

9,258
1
20
32

1

A treacherous example, indeed. How can anyone turn the occurs check off after seeing this? – MWB Dec 13 '20 at 13:05
1

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. – Isabelle Newbie Dec 13 '20 at 13:57
1

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. – Isabelle Newbie Dec 13 '20 at 13:59
`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`. – MWB Dec 13 '20 at 20:25
1

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". – Isabelle Newbie Dec 13 '20 at 22:28
This last version of `less_than/2` loops: https://stackoverflow.com/questions/65439288/less-2-relation-in-peano-arithmetic – MWB Dec 24 '20 at 14:11

score 3 · Answer 2 · answered Dec 13 '20 at 12:07

3

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):

answered Dec 13 '20 at 12:07

Grzegorz Adam Kowalski

5,243
3
29
40

1

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. – David Tonhofer Dec 13 '20 at 12:17
1

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. – Will Ness Dec 13 '20 at 12:18
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. – David Tonhofer Dec 13 '20 at 12:20
2

@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 `<`. – MWB Dec 13 '20 at 12:32
@MaxB The first line is the query? – David Tonhofer Dec 13 '20 at 12:36
1

@DavidTonhofer I think so. `3 < 2` is what we are trying to prove. – MWB Dec 13 '20 at 12:37

David Tonhofer · Answer 3 · 2020-12-13T13:01:41.157

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)

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

3 Answers3

Linked