理解“定义符号”

Question

指南解释define-symbolic的用法：

The define-symbolic form binds the variable to the same (unique) [symbolic] constant every time it is evaluated.

(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 y)

Printed constant names, such as x or b, are just comments. Two [symbolic] constants created by evaluating two distinct define-symbolic (or, define-symbolic*) forms are distinct, even if they have the same printed name. They may still represent the same concrete value, but that is determined by the solver:

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

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

(<=> x x)

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

为什么 (eq? (static) (static)) returns #t，但是 (eq? (static) (yet-another-x)) returns (<=> x x)?

因为 define-symbolic 将变量绑定到 相同的（唯一的）常量，每次计算时 ，为什么 (eq? (static) (yet-another-x)) 不 return #t？ , 就像 (eq? (static) (static))?

是不是意味着两个符号变量出现在不同的作用域中同名，即使我们使用define-symbolic还是不同的？

<=> 和 = 有什么区别？例如(<=> x x) 对比 (= y y).

谢谢。

Answer 1

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

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

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

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

我们只有文档（当然没有源代码），所以我们也可以照着看。

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

所以看起来 (static) 变成了一种逻辑变量的生成器。它以某种方式知道它的内部绑定，知道它是否是第一次被调用，并据此采取行动。

总之，慢慢看，相信就好。没有别的事可做，除非你愿意研究资料来源。

关于(<=> x x)和(= y y)，这些看起来像是限制条件。该指南称它们为“符号表达式”。 <=> ~~最有可能的意思是“不等于”~~ 被描述为 here as "the logical bi-implication of two boolean values", and the = means equality。 x、x、y 和 y 是四种不同符号常量的打印表示。

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

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

Answer 2

以下是对文档内容的解释：

重要的是使用 define-symbolic 两个不同的符号常量来自哪个。因此 static 和 yet-another-x 中的两个用途是不同的用途，因此是不同的符号常量。
无论您对 define-symbolic 的相同用法求值多少次，它总是产生相同的符号常量。您可以将其视为被提升到程序的顶层。
对于 define-symbolic*，它 很重要 当你评估事物时，所以 (eq? (dynamic) (dynamic)) 产生一个约束，可能是也可能不是是的，这取决于求解器所说的内容以及您添加的其他约束条件。
= 仅适用于数字。 <=> 仅适用于布尔值。一般来说，eq? 可能不是您想要进行这些比较的结果。

理解“定义符号”

Understanding `define-symbolic`

racket

rosette