理性的计划者:不理解练习57

Question

在练习(或输入？)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))

我的理由是(茶杯x)中的'x'应首先通过其所有解决方案,并统一到其所有解决方案的列表中.但似乎茶杯一次只放弃其中一种解决方案.这让我很困惑,因为我对conde的解释是,使用它给出的规则,你应该通过conde的行,并且在一行成功之后,假装它失败了,刷新变量并找到成功的下一行.考虑到解决方案的工作方式,似乎代码中的conde会回到成功的行,然后迫使teaupo conde失败并放弃下一个可能的值.再说一遍,我原以为茶杯解决方案会放弃列表中的所有conde解决方案,然后继续进行外部conde调用.任何人都可以向我提供指导,说明为什么它按照书中提供的方式工作而不是我推理的方式？

Answer 1

我的推理是 (teacupo x) 中的“x”应该让其 conde 首先遍历其所有解决方案，然后统一到其所有解决方案的列表。

该变量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)))

Answer 2

(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与in(tea cup)配对，并且in与in配对，形成; 然后进行报告，即收集到解决方案的最终结果列表中，给出。y(#t)x(#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 代码，我认为该代码实际上在功能上等同于本书的代码（当然，在这种特定情况下），

(conde
  ((teacupo x) (= #t y) #s)
  ((= #f x) (= #t y))        ; you had a typo here
  (else #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)

产生输出

*Main> run
[[("r", L [S "茶",B True])], [("r", L [S "cup",B True])], [("r", L [B 错误，B 正确])]]

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

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]]

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

*Main> run
[[("r", L [S "茶",B True])], [("r", L [S "cup",B True])]]