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

Question

Rosette的一些教程介绍了使用浅嵌入和其他使用深度嵌入的 程序合成。

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

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

标签： racketrosette

Answer 1

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

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

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

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

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

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