I am using Racket v8.5, with the packages for minikanren and
minikanren/numbers required. Why does introducing the numbero
constraint cause previously valid unifications to fail?
> (run 1 (q) (<lo '(1) q))
'((_.0 _.1 . _.2))
> (run 1 (q) (<lo '(1) q) (numbero q))
'()
> (run 1 (q) (numbero q) (<lo '(1) q))
'()
> (run 1 (q) (<lo q '(1)))
'(())
> (run 1 (q) (<lo q '(1)) (numbero q))
'()
> (run 1 (q) (numbero q) (<lo q '(1)))
'()
Because the
numberoconstraint enforces that a term is consistent with a number in the host language (Racket in this case). Think ofnumberoas the constraint equivalent of Racket'snumber?predicate:(numbero 5)succeeds. However, you are using Kisleyov's relational arithmetic system, in which numerals are represented as little-endian lists of binary digits:(numbero '(1 0 1))fails, just as(number? '(1 0 1))returns#fin Racket.