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

Posted 2023-05-08

【中文标题】在逻辑编程中，取消嵌套是为了啥？

【英文标题】：In logic programming, what is unnesting for?在逻辑编程中，取消嵌套是为了什么？

【发布时间】：2019-04-20 04:35:29

【问题描述】：

问题

Reasoned Schemer 描述了如何使用 miniKanren，它类似于 Prolog，但它是类 Lisp 语言的库。这本书的“第一诫”是这样的：

转换一个布尔值的函数 变成一个以目标为值的函数，替换 cond 每个问题和答案都带有 conde 和 unnest。 将答案#t（或#f）替换为#s （或#u）。

它们并没有真正定义取消嵌套，除非通过一些大致等效的示例。最清楚的是：取消嵌套将您从(list? (cdr l)) 带到

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

我不明白为什么需要取消嵌套。比如上面的目标，为什么tp write (listo (cdr l))不够？

[1] 我在 Racket 中的迷你 kanren 设置

如here 所述，我运行了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)))

【参考方案1】：

术语un-nesting 表示修改结构的层次结构 - 或删除括号。

刚刚找到了The Reasoned Schemer这本书和相关的GitHubpage，里面也定义了它：

将(car (cdr l)) 转换为(cdro l v) 和(caro v r) 的过程称为取消嵌套...。认识到 unnesting 和 [CPS] 之间的相似性。

【讨论】：

这是一些有用的上下文......但我仍然不知道为什么需要它。此外，取消嵌套不仅仅是删除括号。它将普通值（如cdr）转换为目标（如cdro），并引入新变量（如您找到的引用中的v 和r）。

***.com/a/4114090/549372 可能更好地解释差异 - 其中条件 e 是每个，i 是交错的，a 是全部，u 可能是唯一的。

【参考方案2】：

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

我认为这是必需的，因为您要替换的函数的输入奇偶校验（采用的参数数量）通常低于您要替换的函数。您正在重构一个函数，将输出放入您传递给它的变量中，而不是将其作为输出返回。为什么需要用逻辑等价物替换每个函数？我不完全确定，

（编辑我阅读了您示例的上下文更多...） 如果我们以您给出的示例为例，如果通过我认为的非列表，标准版本会引发错误，这与返回失败不同。因此，如果您传递的不是列表，而不是从您的运行中获取 ()，您会引发一个不同的异常。 我意识到了另一个不同之处，也是一个更重要的区别。您的示例来自 listo 的定义，并且 listo 不只是检查某物是否可以是列表。如果给定一个未绑定的变量，它可以用来生成一个无限列表。这样做是因为 conde 中的第一个元素会成功，所以你会得到 ()。之后，pairo l 将通过使第一个元素 (reified_1) 和第二个元素返回 listo 来成功，这个内部 listo 首先返回 () 就像外部 listo 的第一个结果一样，所以你得到 (reified_1 . ()) 和这可以无限继续。这是有效的，因为你有一个新的 d (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)

【参考方案3】：

“取消嵌套”用于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`

在迷你看人中。为什么？因为(cdr l) 是一个返回值的Lisp 函数。但是在 Prolog 中没有求值，也没有隐式返回的值，而是通过 谓词、关系、通过“设置”一个逻辑作为该谓词的参数的变量。