5

在练习（或条目？）57 中，我只是不明白逻辑是如何流动的。问题是：给定

(define teacupo
  (lambda (x)
    (conde
      ((= tea x ) #s)
      ((= cup x ) #s)
      (else #u))))

其中 '=' 实际上是三连杆统一 (?) 运算符。运行以下：

(run* (r)
  (fresh (x y)
    (conde
      ((teacupo x) (= #t y) #s)
      ((= #f x) (= #t y))
      (else #u)
    (= (cons x (cons y ())) r)))

书中给出了答案：

((tea #t) (cup #t) (#f #t))

我原以为答案是：

(((tea cup) #t) (#f #t))

我的理由是 (teacupo x) 中的“x”应该首先通过其所有解决方案，并统一到其所有解决方案的列表中。但似乎teacupo 一次只放弃了一种解决方案。它让我感到困惑，因为我对 conde 的解释是，使用它给出的规则，你应该遍历 conde 的行，在一行成功后，假装它失败，刷新变量并找到下一行成功。鉴于解决方案的工作方式，该代码中的 conde 似乎回到了成功的行，然后迫使 teacupo conde 失败并放弃下一个可能的值。再一次，我会认为 teacupo 解决方案会放弃列表中的所有 conde 解决方案，然后继续进行外部 conde 调用。

4

2 回答 2

4

我的理由是 (teacupo x) 中的“x”应该首先通过其所有解决方案，并统一到其所有解决方案的列表中。

变量x一次统一为一个值。该表单(run* (x) <goals>)收集x实现目标的值。

> (run* (x)
    (teacupo x))
'(tea cup)

在

(conde
  ((teacupo x) (== #t y))
  ((== #f x)   (== #t y)))

有两种成功的方法：要么实现目标(teacupo x)，并且x是其中之一，tea要么cup- 或者 - 实现目标(== #f x)，并且x是（统一到）#f。

简而言之，一次通过收集满足所有目标的那些值run*的可能值。x这意味着x一次统一为一个值。

一个更简单的例子：

> (run* (x)
  (fresh (y)
    (== y 10)
    (conde
     [(== x 1) (== y 10)]
     [(== x 2) (== y 20)]
     [(== x 3) (== y 10)])))
'(1 3)

想要尝试 DrRacket 中的片段的人的完整代码：

#lang racket
(require minikanren)
(define-syntax succeed (syntax-id-rules () [_ (fresh (t) (== t t))]))

(run* (x)
  (fresh (y)
    (== y 10)
    (conde
     [(== x 1) (== y 10)]
     [(== x 2) (== y 20)]
     [(== x 3) (== y 10)])))    

(define teacupo
  (lambda (x)
    (fresh (result)
      (conde
       ((== 'tea x ) succeed)
       ((== 'cup x ) succeed)))))

(run* (x)
  (teacupo x))

(run* (r)
  (fresh (x y)
    (conde
      ((teacupo x) (== #t y))
      ((== #f x)   (== #t y)))
    (== (cons x (cons y '())) r)))
于 2015-07-05T11:53:57.463 回答
3

(teacupo x)意思是“成功两次：一次与x统一tea，第二次与x统一cup”。然后，

(conde
  ((teacupo x) (= #t y) #s)
  ((= #f x) (= #t y))        ; you had a typo here
  (else #u)

方法，

  • 对于由 产生的每个解决方案(teacupo x)，也统一y并#t成功；并且
  • 对于由 产生的每个解决方案(= #f x)，也统一y并#t成功；并且
  • 不再产生解决方案

所以每个xin(tea cup)与yin配对(#t)，并且xin与in(#f)配对，形成；然后被报告，即收集到解决方案的最终结果列表中，给出.y(#t)rr( (tea #t) (cup #t) (#f #t) )

“看来，teacupo 一次只放弃了一种解决方案。”

是的，这在概念上是完全正确的。

“一行成功后，假装失败，刷新变量，找到下一行成功。”

是的，但是如果条件（或后续目标）成功多次，则每行都可以成功多次。

“似乎该代码中的 conde 回到了成功的行，然后迫使 teacupo conde 失败并放弃下一个可能的值。”

它实际上准备提前生成它们（但作为一个流，而不是作为一个列表），然后每个都被单独处理，通过整个后续步骤链进行馈送，直到成功到达最后一步，或者链中断，被一个#u或其他失败的目标打断。因此，当前一个的处理完成时，将尝试下一个。

在伪代码中：

for each x in (tea cup):
   for each y in (#t):    ; does _not_ introduce separate scope for `y`;
       collect (x y)      ;   `x` and `y` belong to the same logical scope
for each x in (#f):       ;   so if `x` is used in the nested `for` too,
   for each y in (#t):    ;   its new value must be compatible with the 
       collect (x y)      ;   one known in the outer `for`, or else 
for each _ in ():         ;   it will be rejected (x can't be two different
       collect (x y)      ;   things at the same time)

至于为什么它会这样工作，我可以指出我的另一个答案，这可能会有所帮助（尽管它不使用 Scheme 语法）。

使用它，作为说明，我们可以将您的测试编写为 Haskell 代码，它实际上在功能上等同于我认为的书的代码（当然，在这种特定情况下），

data Val = Fresh | B Bool | S String | L [Val] deriving Show 
type Store = [(String,Val)]

teacupo x =   unify x (S "tea") &&: true               -- ((= tea x ) #s)
          ||: unify x (S "cup") &&: true               -- ((= cup x ) #s)
          ||: false                                    -- (else #u)

run = [[("r", Fresh)]]                                 -- (run* (r) ......
  >>: (\s -> [ s ++: [("x", Fresh), ("y", Fresh)] ])   -- (fresh (x,y)
  >>:                                                  -- (conde  
    (    teacupo "x"          &&:  unify "y" (B True)  
                              &&:  true                -- ((teacupo x) (= #t y) #s)
     ||: unify "x" (B False)  &&:  unify "y" (B True)  -- ((= #f x) (= #t y))
     ||: false                                         -- (else #u)
    ) 
     &&: project ["x", "y"] (unify "r" . L)            -- (= r (list x y))
  >>:                                                  
     reporting ["r"]                                   --              ...... )

reporting names store = [[a | a@(n,_) <- store, elem n names]]

只需最低限度的实现，就足以使上述代码工作，

project vars kont store = 
     kont [val | var <- vars, (Just val) <- [lookup var store]] store

unify :: String -> Val -> Store -> [Store]
unify sym val store = 
   let 
      (Just v) = (lookup sym store)
   in 
      case (val_unify v val) of
        Just newval -> [replace_val sym newval store]  -- [updated store], if unifies
        Nothing     -> []                              -- couldn't unify - reject it

val_unify v     Fresh             = Just v             -- barely working,
val_unify Fresh  v                = Just v             --  initial
val_unify (B v) (B u) | v == u    = Just (B v)         --  implementation
                      | otherwise = Nothing
val_unify (S v) (S u) | v == u    = Just (S v)
                      | otherwise = Nothing
val_unify  _     _                = Nothing

replace_val s n ((a,b):c) | s == a    = (a,n) : c
                          | otherwise = (a,b) : replace_val s n c

产生输出

*Main> 运行
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])], [("r", L [B 假，B 真])]]

如果我们将翻译后的conde表达式中的第二行更改为

       ||: unify "x" (B False)  &&:  unify "x" (B True)  -- ((= #f x) (= #t x))

我们确实只得到了两个结果，

*Main> 运行
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])]]

于 2015-07-05T14:12:29.370 回答