1

我正在阅读Rosette Essentials。

该指南解释了使用define-symbolic：

define-symbolic每次计算时，该表单都会将变量绑定到相同的（唯一的）[符号]常量。

(define (static)
 (define-symbolic x boolean?)  ; Creates the same constant when evaluated.
 x)

(define (dynamic)
 (define-symbolic* y integer?) ; Creates a fresh constant when evaluated.
 y)
 
> (eq? (static) (static))
#t

> (eq? (dynamic) (dynamic))
(= y$1 y$2)

打印的常量名称，例如xor b，只是注释。通过评估两个不同的define-symbolic（或，define-symbolic*）形式创建的两个 [符号] 常量是不同的，即使它们具有相同的打印名称。它们可能仍然代表相同的具体值，但这由求解器确定：

(define (yet-another-x)
 (define-symbolic x boolean?)
 x)

> (eq? (static) (yet-another-x))

(<=> x x)

我真的不明白的解释define-symbolic：

为什么(eq? (static) (static))返回#t，但(eq? (static) (yet-another-x))返回(<=> x x)？

由于每次评估时都会define-symbolic将变量绑定到相同的（唯一）常量，为什么不返回？，就像？(eq? (static) (yet-another-x))#t(eq? (static) (static))

这是否意味着两个符号变量出现在不同的范围内并具有相同的名称仍然不同，即使我们使用define-symbolic?

<=>和有什么区别=？例如(<=> x x)与(= y$1 y$2)。

谢谢。

4

2 回答 2

2

这是试图解释文档所说的内容：

  1. 两个不同的符号常数的使用define-symbolic来自哪里很重要。所以里面的两个用途static是yet-another-x不同的用途，因此是不同的符号常数。

  2. 无论您评估 的相同用途多少次define-symbolic，它总是产生相同的符号常数。您可以将其视为被提升到程序的顶层。

  3. 对于define-symbolic*，当您评估事物时确实(eq? (dynamic) (dynamic))很重要，因此会产生一个可能为真或可能不是真的约束，具体取决于求解器所说的内容以及您添加的其他约束。

  4. =仅适用于数字。<=>仅适用于布尔值。一般来说eq?，这些比较可能不是您想要的。

于 2021-07-20T13:38:22.267 回答
1

正如您所注意到的，这里发生了一些关于范围的事情，这完全没有在文档中，未指定，根本没有提及。非常不幸；非常模糊。再多说几句就可能对澄清情况大有帮助；但我们被迫猜测。

我的猜测是表单 (define-symbolic x boolean?)知道它出现的位置，并在每次评估它（表单）时采取相应的行动。在

(define (static)
 (define-symbolic x boolean?)  ; Creates the same constant when evaluated.
 x)

范围是什么x？在我看来，唯一可能的解读是，调用 (define-symbolic x boolean?)在内部创建了一个本地绑定static，并将其设置为它（即调用）创建的“符号常量”。当然，在正常的方案中，在每次不同的调用时，这些仍然是不同的实体static。显然，Rosette 在这里做自己的事情。

我们所拥有的只是文档（当然没有来源），所以我们不妨看看它们。

至于什么是“符号常量”，它们似乎与 Prolog 的逻辑变量密切相关，但也知道它们自己的类型（可能还有更多的“约束”或你有什么）。

所以它看起来像是(static)一种逻辑变量的生成器。它不知何故知道它的内部绑定，知道它是否是第一次被调用，并采取相应的行动。

简而言之，只要慢慢阅读并相信它。没有别的事可做，除非你愿意研究来源。

关于(<=> x x)和(= y$1 y$2)，这些看起来像约束。指南称它们为“象征性表达”。最<=> 可能的意思是“不相等”在这里被描述为“两个布尔值的逻辑双蕴涵”，=意思是相等。x、x和是四个不同符号常量的打印表示y$1。y$2

与第二个约束一样，可以知道（要求）两个不同的符号常数（最终）相等；或不相等，如第一个。

虽然它们（常量）还没有任何与它们相关的具体值，但约束仍然是象征性的；但是一旦符号常量/逻辑变量获得其具体值（或者可能获得更多与之相关的约束，因此理论上可以检查这些约束的一致性），就可以对其进行实际检查。

于 2021-07-19T12:23:29.737 回答