The logic of the disequality constraint with multiple variables is incorrect

[alfredo08154711]

Let me preface this by saying that I am a complete beginner in logic programming, Python, Lisp and its variants, and especially Kanren, and I am impressed by miniKanren, microKanren, and this project.—Respect!

Actually, I was just looking for a very lean way to program in Prolog, implemented in pure Python. But with Prolog I lose my head as soon as a ! operator appears, so I was happy about relational programming. This was the way I became aware of Kanren and this project.—What I see and read now makes me very optimistic and makes me marvel at all the things you can do with it. So I just couldn't resist trying it out. And so I wanted to try out the second example in Logic programming, section Metalogic programming—and stumbled across the problem of negation.

As soon as negation is used in a context that is even slightly complex, e.g. multiple negation, nesting in logical conjunctions and disjunctions, etc., everyone gets confused very quickly.—I have an original sample of the PhD thesis by Martin F. Sohnius, one of the founders of supersymmetry (Haag-Łopuszański-Sohnius theorem), which deals with many Graßmann-valued objects that are multiplied anticommutatively. In his handwritten dedication, he wishes my doctoral supervisor: "Good luck with the minus signs!"

In short, no one should jump to conclusions about how to implement negation, especially not me.

Let's look at the example mentioned above:

attends(alice, tea_party).
attends(mad_hatter, tea_party).
attends(dormouse, tea_party).

approved_attends(alice, tea_party).

prohibited_attends(Person, Meeting) :-
    \+ approved_attends(Person, Meeting).

?- attends(Person, tea_party), prohibited_attends(Person, tea_party)
%   Person = mad_hatter
%   Person = dormouse

How can the negation \+ approved_attends(Person, Meeting) be expressed in miniKanren? Obviously there is no equivalent, in particular no general negation of a relation. But there is a limited way to express negation: that of the disequality constraint, implemented in this project by the neq goal. So I wondered if I could find a way to get at least a negation of the fact container Relation(). On the way there, maybe I should first build a container for negated facts to get a feel for the thing in the first place.

First, I translated the example:

>>> from kanren import run, var, Relation, fact, facts
>>> 
>>> attends = Relation('attends')
>>> facts(attends,
...   ('alice', 'tea_party'),
...   ('mad_hatter', 'tea_party'),
...   ('dormouse', 'tea_party'))
>>> 
>>> # Test
>>> Person = var('Person')
>>> run(0, Person, attends(Person, 'tea_party'))
('mad_hatter', 'dormouse', 'alice')
>>> 
>>> approved_attends = Relation('approved_attends')
>>> fact(approved_attends, 'alice', 'tea_party')
>>> 
>>> # Test
>>> run(0, Person, attends(Person, 'tea_party'), approved_attends(Person, 'tea_party'))
('alice',)

Cool.

To get something I can actually negate, namely an equality, I rephrased approved_attends:

>>> from kanren import eq
>>> 
>>> def approved_attends_alt(Person, Meeting):
...   return eq((Person, Meeting), ('alice', 'tea_party'))
... 
>>> # Test
>>> run(0, Person, attends(Person, 'tea_party'), approved_attends_alt(Person, 'tea_party'))
('alice',)

Okay, now the negation:

>>> from kanren.constraints import neq
>>> def not_approved_attends_alt(Person, Meeting):
...   return neq((Person, Meeting), ('alice', 'tea_party'))
... 
>>> # Test
>>> run(0, Person, attends(Person, 'tea_party'), not_approved_attends_alt(Person, 'tea_party'))
('mad_hatter', 'dormouse')

Looks good.

As we all know, the logical conjunction is commutative. Since what's going on under the hood actually depends heavily on the order of the goals, it's worth testing:

# Test with goals in the other order
>>> run(0, Person, not_approved_attends_alt(Person, 'tea_party'), attends(Person, 'tea_party'))
('mad_hatter', 'dormouse')

It still looks good.

So far we have kept the tea party constant as a literal. Now let's try it with a variable:

# Test with two logical variables
>>> Meeting = var('Meeting')
>>> run(0, [Person, Meeting], attends(Person, Meeting), not_approved_attends_alt(Person, Meeting))
(['mad_hatter', 'tea_party'], ['dormouse', 'tea_party'])

Super.—And, because we are thorough, we also make sure that commutativity also works with two variables:

# Test with two logical variables and goals in the other order
>>> run(0, [Person, Meeting], not_approved_attends_alt(Person, Meeting), attends(Person, Meeting))
()

Ooops…

Okay; while I have zero idea about logical programming, Python and miniKanren, I'm sure that logical conjunction is commutative, and as far as I understand the paradigm of relational programming (do I really?), the order of goals must have no effect on the result set, only on the order in which solutions are found—which is only relevant for very large result sets, especially infinitely large ones. What is also disturbing is that the result set shrinks when you remove a constraint (Meeting = 'tea_party').

Let's look at the state stream generated by the goal neq((Person, Meeting), ('alice', 'tea_party')), which is represented by not_approved_attends_alt:

>>> for s in not_approved_attends_alt(Person, Meeting)({}):
...   print(s)
... 
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Person: FlexibleSet([alice]), ~Meeting: FlexibleSet([tea_party])})})

As I understand this result (do I understand it correctly?), this is only one state, the one that is logically equivalent to the statement Person ≠ 'alice' ∧ Meeting ≠ 'tea_party'. And if I have understood this output correctly, then this is not correct. Rather, two states each with a ConstraintStore must be created, corresponding to the logical statement Person ≠ 'alice' ∨ Meeting ≠ 'tea_party'. Because this statement is logically equivalent to the negation of the statement Person = 'alice' ∧ Meeting = 'tea_party' (eq((Person, Meeting), ('alice', 'tea_party'))). —To check my understanding of the state stream, here is the state stream generated by Person ≠ 'alice' ∨ Meeting ≠ 'tea_party', formed with lany and neq:

>>> from kanren import lany
>>> 
>>> for s in lany(neq(Person, 'alice'), neq(Meeting, 'tea_party'))({}):
...   print(s)
... 
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Person: FlexibleSet([alice])})})
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Meeting: FlexibleSet([tea_party])})})

So this is what the state stream of not_approved_attends_alt should look like.

Also the logical conjunction of several of the versions of neq((Person, Meeting), (..., ...)) "corrected" in this way—i.e. conjunctions of several neq of each a different variable—is obviously implemented logically incorrectly:

>>> from kanren import lall
>>> 
>>> for s in lall(lany(neq(Person, 'alice'), neq(Meeting, 'tea_party')), lany(neq(Person, 'mad_hatter'), neq(Meeting, 'tea_party')))({}):
...   print(s)
... 
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Person: FlexibleSet([alice, mad_hatter])})})
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Meeting: FlexibleSet([tea_party]), ~Person: FlexibleSet([mad_hatter])})})
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Person: FlexibleSet([alice, mad_hatter]), ~Meeting: FlexibleSet([tea_party])})})
ConstrainedState({}, {<class 'kanren.constraints.DisequalityStore'>: ConstraintStore(neq: {~Meeting: FlexibleSet([tea_party]), ~Person: FlexibleSet([mad_hatter])})})

This result is also wrong, if I have misunderstood, because the second and fourth states are the same. In any case, this result does not correspond structurally to a conjunction of two disjunctions.

Thank you for your attention.

---

Python 3.12.3 (main, Jun  1 2024, 14:07:35) [GCC 7.5.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> __import__('unification').__version__
'0.4.6'
>>> __import__('etuples').__version__
'0.3.9'
>>> __import__('multipledispatch').__version__
'0.6.0'
>>> __import__('cons').__version__
'0.4.6'
>>> __import__('toolz').__version__
'0.12.1'
>>> __import__('kanren').__version__
'1.0.3'

[brandonwillard]

Thanks for the report! From a quick read, it does look like a genuine bug.

For reference, the constraint approach used here is based on the following fantastic paper by @jasonhemann: https://arxiv.org/abs/1701.00633. That explains how the constraints should be handled.

[jasonhemann]

What an awesome, well-written bug report! Thanks, that was fun to read.

BTW-there's a mistake in that paper---shouldn't have added boolean constraints. Described and remedied here:
https://scholarworks.iu.edu/iuswrrest/api/core/bitstreams/5b1793f6-f001-42e3-b83c-671ebe41d4e6/content#page=87.65

I don't believe that it's the source of this issue, but wanted to drop the breadcrumbs anyway.