racket - 我什么时候应该使用 Rosette 的浅嵌入与深层嵌入进行程序合成？

Question

Rosette 的一些教程使用 shallow embedding 介绍程序合成和其他人使用 deep embedding .

阅读 Torlak et Bodik 的 "Growing Solver-Aided Languages with ROSETTE" 后，似乎浅嵌入有利于快速原型(prototype)设计(因为它不需要定义 DSL 和解释器)，而深层嵌入有利于进行具有更强正确性保证的查询。这是决定使用哪个嵌入的好经验法则吗？

使用 Rosette 的浅嵌入与深层嵌入进行程序合成的充分理由是什么？

Answer 1

作为一般经验法则，浅嵌入最适合使用求解器来搜索程序处理的值的应用程序，这对于程序验证和天使执行是典型的。

如果您正在进行程序合成和搜索(表示的值)代码，那么深度嵌入是最佳选择。

如果您的应用程序将只搜索常量，那么浅嵌入可能是程序合成的不错选择。但是，如果您正在搜索更复杂的东西(例如，表达式或语句)，那么深度嵌入是您的最佳选择。

使用浅嵌入，您对 Rosette 将搜索的程序空间的控制有限。基本上，您仅限于可以使用 Rosette 基于宏的草图构造进行编码的任何内容。这些允许您定义基本搜索空间并编写快速原型(prototype)，但如果您想构建一个可扩展的工具，您将需要严格控制搜索空间。

通过深度嵌入，您可以完全控制要搜索的程序空间。本质上，您可以编写任意 Rosette/Racket 函数来生成表示要搜索的所有具体程序的符号程序。然后，您还可以完全控制最后一步，即代码生成。一旦 Rosette 返回一个代表深度嵌入中的程序的值(例如 AST)，您就可以处理它，但要生成代码。使用浅嵌入，您只能使用 Rosette 的内置代码生成器。

因此，总而言之，如果您正在或计划进行合成，请使用深度嵌入。对于其他一切(验证和天使执行)，浅嵌入将更容易和更快。