为什么在minikanren中引入numbero会导致有效统一的失败

Question

我使用的是Racket v8.5，需要minikanren和
minikanren/numbers的软件包。为什么引入numbero
约束会导致以前有效的统一失败？

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

Answer 1

因为numbero约束强制要求术语与主机语言中的数字一致(在本例中为Racket(。将numbero视为Racket的number?谓词的约束等价物：(numbero 5)成功。然而，您使用的是Kisleyov的关系算术系统，其中数字表示为二进制数字的小端序列表：(numbero '(1 0 1))失败，就像(number? '(1 0 1))在Racket中返回#f一样。