我们得到:
(defrel (alwayso)
(conde
(#s)
((alwayso))))
(run 1 q
(alwayso)
#u)这本书(第二版)说:
"__
alwayso成功了,接着是#u__,它导致(alwayso)被重试,而(alwayso)又成功了“。
我还是没拿到控制流程。为什么conde的两个分支在进入#u之前都没有尝试(继续递归)
发布于 2022-09-24 22:22:07
“为什么
conde的两个分支在进入#u之前都没有尝试(继续递归)?”
您的意思是,为什么在进入#u之前没有尝试第二个arm,结果来自于第一个。
简单的回答是,懒惰序列 (也就是懒惰评价)范式。
在热切的评价范式下,每个目标都会产生全部的解决方案。如果它们的数目是无界的(“无限”),这意味着无限循环,实际上正如您所预期的那样。
在懒惰的评估范式下,每个目标一个接一个地产生解决方案--意思是,它只产生它的第一个结果,并且随时准备在需要的时候产生下一个结果。
目标一个接一个地产生它们的替换结果,就好像是由Python中的yield来实现的。合并后的目标也是如此。conde组合以某种方式组合其子目标(见下文),并逐一生成组合目标的结果。因此
#| (defrel (alwayso)
(conde
(#s)
((alwayso)))) |#
(run 1 q
(alwayso)
#u)
=
(run 1 q
(conde
(#s) ; 1.1
((alwayso))) ; 1.2 -> ; 1
#u) ; 2run的第一个目标,即合并目标conde,一个接一个地产生其结果,每一个结果一产生就被反馈给第二个run目标#u。
如果run的第一个子目标的所有解决方案都是在将结果列表输入到下一个子目标之前生成的,那么对于任何能够产生无限列表(或更准确地说,无界流)的目标,评估永远不会结束。
因此,这些流是懒惰的流,列表是迫切的列表。差别是可以运作的。在急切方案下,第一个子目标的列表首先完整构建,然后由下一个目标进行处理。当结果的数量是无限的,建立一个无限渴望的列表将花费无限的时间。
因此,在急切的评估范式下,它确实会陷入conde内部的递归。
在这本书的实现所选择的懒惰评估范式下,它被困在一个更大的循环中,每次都会从#u上反弹回来。但是conde起作用,成功地一个一个地产生了它的替换结果。
阴谋本身就是一种热切的语言。延迟生产剩余的溪流是通过把它放在羊驼后面,粗略地说,
(cons 1 rest-of-list)(急切的名单)改为
(cons 1 (^() code-to-produce-the-rest-of-stream))(一条懒惰的小溪)
alwayso被定义为它会产生一个无限的输入替换的拷贝流,没有改变。但它是一个接一个地产生的。
然后,run将这个流从其第一个目标输入到第二个目标,#u,后者拒绝它。因为run 1要求它的子目标有一个解决方案,所以它会重新尝试它们,直到一个解决方案/替换通过为止。
这从来没有发生过。
因此,这将导致无限循环。
同样,这两种手臂都试过了--首先,第一种;然后,在其(一种)结果被随后的#u拒绝后,第二种手臂被尝试。由此产生的替代再次被拒绝。无限:
;; we have
(defrel (alwayso)
(conde
(#s)
((alwayso))))
;; running:
(run 1 q
(alwayso)
#u)
=
(run 1 q
(conde ; (a OR b) , c
(#s)
((alwayso)))
#u)
=
(run 1 q ; (a , c) OR (b , c)
(conde
(#s #u)
((alwayso) #u)))
=
(run 1 q
(alwayso)
#u)
=
.....卡住了。
遵循实现的定义,
(defrel (alwayso)
(conde
(#s)
((alwayso))))
= ; by def of defrel; with ^ for lambda
(define (alwayso)
(^s (^() ( (conde
(#s) ; first
((alwayso))) s)))) ; second
= ; by defs of conde, conj and disj
(define (alwayso)
(^s (^() ( (disj2
#s ; first
(alwayso) ) s)))) ; second
= ; by def of disj2
(define (alwayso) ; (-1-)
(^s (^() (append-inf
(#s s) ; first
((alwayso) s)) ))) ; second
= ; by defs of #s and alwayso (-1-)
(define (alwayso)
(^s (^() (append-inf
(list s) ; first
(^() (append-inf ; second
(#s s)
((alwayso) s)) )) )))
= ; by def of append-inf
(define (alwayso)
(^s (^() (cons s ; first
(^() (append-inf ; second
(#s s)
((alwayso) s)) )) )))
= ; by def of append-inf
(define (alwayso)
(^s (^() (cons s
(^() (cons s
((alwayso) s)) )) )))
=
....因此,我们在这里确实看到了一个定义,该定义产生了输入替换s的无限多个副本的流,当请求时,这是调用((alwayso) <s>)的结果。
或者,在伪码中,为append-inf编写append-inf,为(list s)编写[s],
((alwayso) s)
=
((#s OR (alwayso)) s)
=
(#s s) ++ ((alwayso) s)
=
[s] ++ ((#s OR (alwayso)) s)
=
[s] ++ [s] ++ ((#s OR (alwayso)) s)
=
[s] ++ [s] ++ [s] ++ ((#s OR (alwayso)) s)
=
[s s s .... ]最后,
(run 1 q (alwayso) #u)
= ; by def of run
(let ((q (var 'q)))
(map (reify q)
(run-goal 1 (conj (alwayso) #u))))
= ; by defs of run-goal and conj
(let ((q (var 'q)))
(map (reify q)
(take-inf 1 ((conj2 (alwayso) #u) empty-s))))
= ; by defs of conj2 and #u
(let ((q (var 'q)))
(map (reify q)
(take-inf 1
(append-map-inf (^s '())
((alwayso) empty-s)))))不管有多少empty-s应用了(^s '()),为了将结果附加到一起,所有的结果都是空列表,所以即使是包含的结果也不能take,因为没有任何结果。
(take-inf 1
(append-map-inf (^s '())
((alwayso) empty-s)))
= ; as established above
(take-inf 1 (append-map-inf (^s [])
[ s0 s0 s0 .... ]))
= ; by def of append-map-inf
(take-inf 1
(append-inf ((^s []) s0)
(append-map-inf (^s [])
[ s0 s0 .... ])))
= ; by beta-reduction
(take-inf 1
(append-inf []
(append-map-inf (^s [])
[ s0 s0 .... ])))
= ; be def of append-if
(take-inf 1
(append-map-inf (^s [])
[ s0 s0 .... ]))
= ; and we're back where we've started
<LOOPING> 或者,象征性地,
(take 1 (append-map-inf (^s [])
[ s0 s0 s0 .... ]))
=
(take 1 (append-inf [ [] [] [] .... ]))
=
(take 1 [ ; sic!所以它被卡住了。
https://stackoverflow.com/questions/73821032
复制相似问题