Wrong result with absento

[AlexKnauth]

#lang racket
(require minikanren)

(run 1 (q)
  (== q 'A)
  (absento q '(A)))

;; should be '()
;; wrongly produces '(A)

P.S.
If I rewrite it to use my own "not-membero" relation instead of absento, it produces the correct '() result.

P.P.S
webyrd/miniKenren-with-symbolic-constraints seems to have the correct behavior on this example.

[AlexKnauth]

Is this intentional? The readme mentions something about absento needing a "ground atom." If it was intentional, why isn't this an error?

[webyrd]

The original implementation of absento supported arbitary terms, including fresh logic variables, as the first argument to absento. I think this general behavior should be supported. If not, at least allowing a fresh variable representing an atom should be supported. If not, signalling an error if the first argument is the wrong type, or isn't ground, is the correct behavior.

Michael, would it be difficult to support the full general behavior of absento? Is this a reification problem? An attributed variables problem? An efficiency problem?

Thanks!

[webyrd]

I just submitted my first ever pull request! :)

#3

This patch checks that the first argument to absento is a ground error--otherwise it signals an error.

Handling generalized absento constraints using faster-miniKanren's attributed variables architecture looks tricky to me. It may be necessary to handle absento constraints specially.

[michaelballantyne]

@webyrd Is there an example of a tricky case you're thinking about? I'm not sure it's too bad, except perhaps for reification concerns that would be handled by the old reifier this implementation inherits.

(absento a b) is equivalent to: for all subtrees s of b, (=/= a s).

Applying (absento a b) where a and b are fresh logic variables should apply (=/= a b) and add a to the absento part of the constraint record for b. If b is instantiated to a pair (c . d), we'll consult the constraint record and apply (absento a c) and (absento a d), which will create the disequalities and add the absento constraint record to c and d just as we did with b.

Generalized absento still doesn't allow a constraint to restrict the range of values for a variable to a finite range, so it shouldn't break any of the assumptions that make the attributed variable implementation safe.