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

83 Views Asked by At

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

There are 1 best solutions below

0
William E. Byrd On BEST ANSWER

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.