0

The tag logical purity mentions (=)/2 as pure. Is it "intrinsically" pure or "operational" pure? To the best of my knowledge it can be defined by this Horn clause:

∀x(=(x, x))

Which is this Prolog fact, if were not already a built-in:

X = X.

This means (=)/2 would be "intrinsically" pure, as SWI-Prolog already remarks. So what is then the difference to first order equality (FOL=), if there are any differences?

  • 1
    Since `(=)/2` differs *from itself* depending on the value of the `occurs_check` flag, I think it would be good to mention your preferred value of this flag. – Isabelle Newbie Dec 22 '20 at 11:45
  • Are they even in the same ballpark? `=` is an instruction to change computational state (and possibly trigger goals of attributed variables), whereas "=" is a statement about restricting oneself to certain worlds in which "the equality is true" (whatever [that even means](https://www.quantamagazine.org/with-category-theory-mathematics-escapes-from-equality-20191010/)) – David Tonhofer Dec 22 '20 at 11:45
  • An intrinsic definition of (=)/2 will be in sync with the occurs_check flag. Since the occurs_check flag not only affects the built-in (=)/2 but also the head unification when invoking a clause. See also: https://swi-prolog.discourse.group/t/what-does-sort-2-do/2418/50?u=j4n_bur53 –  Dec 22 '20 at 12:51
  • "The fact X = X will also trigger attributed variables". Not sure what this means exactly. Extensions to unification qua attributed variables do not affect syntactic equality of terms. That is, new behaviour is possible only for newly introduced symbols (which are called variable attributes, previously called meta-structures) and their relation to existing terms. – false Dec 23 '20 at 11:42
  • @false Did you follow the see also link? There you find the example: Fact eq(X, X). Query freeze(Y, (write(Y), nl)), eq(Y, foo). Result output foo. –  Dec 23 '20 at 12:10
  • `freeze/2` effectively introduces a new symbol. Thus `Y` refers to that. And the unification of that with an atom is just up to that extension. – false Dec 23 '20 at 12:17
  • Well I am not responsible for what people ask here. David Tonhofer asked. And I answer. Do you think my answer is incorrect? I didn't claim my answer concerning attributed variables has something to do with a Prolog that doesn't have attributed variables, and logical and non-logical ways to introduce attributed variables. You need to open a new question if you are interested in these matters. Its not in the scope of this question, it was only an answer to a comment. –  Dec 23 '20 at 12:22

1 Answers1

0

The "intrinsinc" definition of (=)/2 I guess does assure that the unify predicate is reflexive, symmetric and transitive. Requirements that are also satisfied by FOL=. But FOL= also requires congruence, which is this axiom schema:

/* Predicate Congruence in FOL= */

∀x1..∀xn∀yj(=(xj, yj) & p(x1, .., xn) -> p(x1, .., xj-1, yj, xj+1, .., xn))

Which is not represented by the only Horn clause for the unify predicate. And since the unify predicate is a built-in, the missing Horn clauses can also not be added. So what can go wrong? Can we make an example that would go wrong?

The classical example is this fact:

p(morning_star).

Obviously this query succeeds in Prolog:

?- p(morning_star).
true

But this query fails in Prolog, whereas in FOL= it would succeed:

?- morning_star = evening_star, p(evening_star).
false

The situation is different in so called unification modulo theories, where the unification and also the unify predicate might change their meaning.

  • https://en.wikipedia.org/wiki/Unique_name_assumption but the ramifications go beyond the behavior of `=`. – MWB Dec 22 '20 at 18:42
  • Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/226316/discussion-between-mostowski-collapse-and-maxb). –  Dec 22 '20 at 19:20