在逻辑编程中，取消嵌套是为了什么？

Question

问题是

经过推理的计划者描述了如何使用miniKanren，它类似于Prolog，但它是类Lisp语言的库。这本书的“第一戒律”是：

若要将值为布尔值的函数转换为值为目标的函数，请用conde替换cond，并取消每个问题和答案的嵌套。将答案#t (或#f)替换为#s (或u)。

他们并没有真正定义取消嵌套，除非通过几个大致相同的例子。最清楚的是:取消嵌套将您从(list? (cdr l))带到

(fresh (d)
       (cdro l d)
       (listo d))

我不明白为什么需要取消嵌套。例如，对于上面的目标，为什么没有足够的tp写(listo (cdr l))

1我在球拍中的迷你kanren装置

正如所描述的这里，我运行了raco pkg install minikanren，然后定义了一些缺失的部分。

2.一些你可能不需要的函数定义

这里是listo的定义和它使用的一切，除了在minikanren库中定义的东西或在Racket的序曲中定义的东西。

(define listo
  (lambda (l)
    (conde
     ((nullo l) #s)
     ((pairo l)
      (fresh (d)
             (cdro l d)
             (listo d)))
     (else #u))))

(define nullo
  (lambda (x)
    (== x '())))

(define pairo
  (lambda (p)
    (fresh (a d)
           (conso a d p))))

(define cdro
  (lambda (p d)
    (fresh (a)
           (== (cons a d) p))))

(define conso
  (lambda (head tail result)
    (== (cons head tail) result)))

Answer 1

术语un-nesting意味着修改结构的层次结构--或者去掉括号。

刚刚找到了书推理的阴谋家和相关的GitHub 页面，后者也定义了它：

将(car (cdr l))转换为(cdro l v)和(caro v r)的过程称为取消嵌套…。。识别非嵌套和CPS之间的相似性。

Answer 2

免责声明，我不知道计划和我大约1/5进入这本书。

我认为这是必要的，因为您要替换的函数的输入奇偶性(使用的参数数)通常低于要替换它的函数。您在某种程度上重构一个函数，将输出放入您传递给它的变量中，而不是作为输出返回它。为什么需要用逻辑等效的方法替换每个函数？我不太确定，

(编辑:我更多地阅读了示例的上下文.)如果我们以您给出的例子为例，如果传递了一个我认为与返回失败不同的非列表，标准版本将引发一个错误。因此，如果您传递一些不是列表的内容，而不是从运行中获得()，则会引发一个不同的异常。我意识到另一个不同之处，更重要的是。您的例子来自listo的定义，listo并不只是检查某个东西是否可以是一个列表。如果给定一个未绑定变量，则可以使用它生成无限列表。它这样做是因为首先，conde中的第一个元素将成功，因此您将得到()。之后，pairo l将成功地创建第一个元素(reified_1)，第二个元素返回到listo，这个内部listo第一次返回()，就像外部listo做的第一个结果一样，因此得到(reified_1 )。()，这可以无限地继续下去。这是因为使用了(cdro L)的新d，允许d绑定到通过递归调用listo设置的变量。如果不通过取消嵌套来创建d变量，就无法做到这一点。

解释奇偶点：

cdr(x) # get the rest elements of x
cdro(a x) # you "pass in" the equivalent to the output element of the first function into this logical version. 

这意味着如果有b= cdr(cdr(x))，则需要创建一个变量来保存中间值，如下所示：

fresh(a)
cdro(a, x)
fresh(b)
cdro(b, a)

看到区别/理由了吗？你在传递你的输出。因此，不能“嵌套”嵌套表达式中的所有内容，您需要将其分解为行，以便有空间分配新变量。

为什么一定要这样？我在考虑是否可以通过重载基于奇偶的函数来避免大量的去嵌套。类似我在下面写的东西(在python中，假设caro已经定义了)。问题是，我认为它是无用的，因为绑定到列表的第一个元素的变量是新的，而不是其他任何地方，因此不可能对应用任何其他约束有用。目标的目的是返回满足它们的绑定集，但是这些绑定必须在已经定义的变量上，否则它们是无用的。

class UNDEF:
    pass

def cdronew(a, b=UNDEF):
    if b is UNDEF:
        # assume that we need to fresh a variable and use that for our output
        b = fresh('b')
        # not a typo in order, we're assuming we wanted the first val of the list
        # here is the problem, we'll bind b but noone outside this function knows about it so that binding is useless!
        return cdro(b, a)
    else:
        return cdro(a, b)

Answer 3

"Unnesting“用于SSA转换，因为Prolog就是这样的，因为它没有计算，所有状态的更改和传递都必须显式地完成。

SSA表单是您在执行有限形式的CPS转换之后得到的代码。简单地说，每个临时实体都是明确的，并被赋予一个名称。

(let* ((c (+ (sqr x) (sqr y)) )
       (z (sqrt c)))
  ....

转化成

(let*  ((a (sqr x))
        (b (sqr y))
        (c (+ a b))
        (z (sqrt c)))
  ....

类似地，在编写时，Lisp代码(list? (cdr l))被转换为谓词。

    ( L = [_ | D], 
      is_list( D ) )

在Prolog中，这是目标

    (fresh (d)
       (cdro l d)    ; a relation "cdro" holds between `l` and `d`
       (listo  d))   ; a predicate listo holds for `d`

在miniKanren中。为什么？因为(cdr l)是一个Lisp函数，它返回一个值。但是在Prolog中没有求值，没有隐式返回的值，而是通过“设置”一个逻辑变量(作为该谓词的参数)将它们显式地存在于谓词(关系)中。