理性策划者：不理解练习 57
The Reasoned Schemer : Not understanding Exercise 57
关于练习（或条目？）57，我只是不明白逻辑是如何流动的。问题是这样的：given
(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' 应该让其 conde 首先遍历其所有解决方案，并统一到其所有解决方案的列表。但似乎 teacupo 一次只放弃其中一种解决方案。这让我感到困惑，因为我对 conde 的解释是，使用它给出的规则，你应该遍历 conde 的行，并且在一行成功之后，假装失败，刷新变量并找到下一行成功。鉴于解决方案的工作方式，该代码中的 conde 似乎返回到成功行，然后迫使 teacupo conde 失败并放弃下一个可能的值。同样，我原以为 teacupo 解决方案会放弃列表中的所有 conde 解决方案，然后继续进行外部 conde 调用。任何人都可以指导我为什么它按照书中提供的方式而不是我推理的方式工作吗？
My reasoning being that the 'x' in (teacupo x) should have its conde
go through all of its solutions first, and unify to the list of all of
its solutions.
变量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)))
(teacupo x)表示"succeed twice: once with x unified with tea, and the second time with x unified with 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并成功；还有
- 不再生成解
因此 (tea cup) 中的每个 x 都与 (#t) 中的 y 配对，并且 (#f) 中的 x 也配对y 在 (#t) 中，组成 r；然后报告r，即收集到解决方案的最终结果列表中，给出( (tea #t) (cup #t) (#f #t) )。
"it appears that teacupo only gives up one of its solutions at a time."
是的，这在概念上是完全正确的。
"after a line succeeds, pretend that it failed, refresh the variables and find the next line that succeeds."
是的，但是如果条件（或后续目标）成功多次，则每一行都可以成功多次。
"it seems like the conde in that code goes back to a successful line, then forcing the teacupo conde to fail and give up the next possible value."
它实际上准备提前生成它们（但作为一个流，而不是一个列表），然后分别处理每个，通过整个后续步骤链，直到成功到达最后一步，或者链条被打破，被 #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)
至于 为什么 是这样工作的，我可以向您指出 another answer of mine，这可能会有帮助（尽管它不使用 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> run
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])], [("r", L [B False,B True])]]
如果我们将翻译后的 conde 表达式的第二行更改为
||: unify "x" (B False) &&: unify "x" (B True) -- ((= #f x) (= #t x))
我们确实只有两个结果，
*Main> run
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])]]
关于练习（或条目？）57，我只是不明白逻辑是如何流动的。问题是这样的：given
(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' 应该让其 conde 首先遍历其所有解决方案，并统一到其所有解决方案的列表。但似乎 teacupo 一次只放弃其中一种解决方案。这让我感到困惑，因为我对 conde 的解释是，使用它给出的规则，你应该遍历 conde 的行，并且在一行成功之后，假装失败，刷新变量并找到下一行成功。鉴于解决方案的工作方式，该代码中的 conde 似乎返回到成功行，然后迫使 teacupo conde 失败并放弃下一个可能的值。同样，我原以为 teacupo 解决方案会放弃列表中的所有 conde 解决方案，然后继续进行外部 conde 调用。任何人都可以指导我为什么它按照书中提供的方式而不是我推理的方式工作吗？
My reasoning being that the 'x' in (teacupo x) should have its conde go through all of its solutions first, and unify to the list of all of its solutions.
变量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)))
(teacupo x)表示"succeed twice: once with x unified with tea, and the second time with x unified with 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并成功；还有 - 不再生成解
因此 (tea cup) 中的每个 x 都与 (#t) 中的 y 配对，并且 (#f) 中的 x 也配对y 在 (#t) 中，组成 r；然后报告r，即收集到解决方案的最终结果列表中，给出( (tea #t) (cup #t) (#f #t) )。
"it appears that teacupo only gives up one of its solutions at a time."
是的，这在概念上是完全正确的。
"after a line succeeds, pretend that it failed, refresh the variables and find the next line that succeeds."
是的，但是如果条件（或后续目标）成功多次，则每一行都可以成功多次。
"it seems like the conde in that code goes back to a successful line, then forcing the teacupo conde to fail and give up the next possible value."
它实际上准备提前生成它们（但作为一个流，而不是一个列表），然后分别处理每个，通过整个后续步骤链，直到成功到达最后一步，或者链条被打破，被 #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)
至于 为什么 是这样工作的，我可以向您指出 another answer of mine，这可能会有帮助（尽管它不使用 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> run
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])], [("r", L [B False,B True])]]
如果我们将翻译后的 conde 表达式的第二行更改为
||: unify "x" (B False) &&: unify "x" (B True) -- ((= #f x) (= #t x))
我们确实只有两个结果，
*Main> run
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])]]