Search code examples
logic-programmingunificationminikanren

Why does introducing numbero in minikanren cause the failure of valid unifications?


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)))                                                                                                                                                                                            
'()                                          

Solution

  • Because the numbero constraint enforces that a term is consistent with a number in the host language (Racket in this case). Think of numbero as the constraint equivalent of Racket's number? 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 #f in Racket.