1

问题

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

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

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

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

我不明白为什么需要取消嵌套。例如，对于上述目标，为什么 tp write 还不够(listo (cdr l))？

[1] 我在 Racket 中的迷你 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)))
4

3 回答 3

2

该术语un-nesting意味着修改结构的层次结构 - 或删除括号。

刚刚找到了The Reasoned Schemer这本书和相关的 GitHub页面，其中也定义了它：

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

于 2018-11-17T02:34:52.070 回答
1

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

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

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

“取消嵌套”用于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 中没有求值，也没有隐式返回的值，而是通过predicate、relation，通过“设置”作为该谓词的参数的逻辑变量来显式地存在它们。

于 2018-12-03T20:42:26.490 回答