Is the structure of my Prolog expression isomorphic to the structure of the Liar Paradox?
We assume that Prolog does not evaluate the meanings of the term "not" and "true" and only evaluates the the structure of the expression.
Liar Paradox in English: "This sentence is not true."
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
After careful review by others it seems correct to say that the above expression is isomorphic to the (structure of the) Liar Paradox.
Experts seem to think that Prolog is taking "not" and "true" as meaningless and is only evaluating the structure of the expression.
?- LP = foo(bar(LP)).
LP = foo(bar(LP)).
?- unify_with_occurs_check(LP, foo(bar(LP))).
false.
The SWI-Prolog implementation of unify_with_occurs_check/2 is cycle-safe and only guards against creating cycles, not against cycles that may already be present in one of the arguments. https://www.swi-prolog.org/pldoc/man?predicate=unify_with_occurs_check/2
My understanding of this is that Prolog detects a cycle in the directed graph of the evaluation sequence of the expression.
The Clocksin & Mellish text in my answer explains the details of why unify_with_occurs_check rejects LP. ---
Prolog correctly rejects any expression having the same pathological self referential structure as the Liar Paradox with its unify_with_occurs_check/2.