问题描述
Rosette 的一些教程介绍了使用浅层嵌入和其他使用深度嵌入.
Some tutorials for Rosette introduce program synthesis using shallow embedding and others using deep embedding.
在阅读了Torlak et Bodik的使用ROSETTE扩展求解器辅助语言"，似乎浅层嵌入对于快速原型设计是有好处的(因为它不需要定义DSL和解释器)，而深层嵌入对于进行具有更强正确性保证的查询是有好处的.这是决定使用哪种嵌入的良好经验法则吗?
After reading Torlak et Bodik's "Growing Solver-Aided Languages with ROSETTE", it seems the shallow embedding is good for fast prototyping (since it does not require defining DSL & interpreter) and the deep embedding is good for making queries with stronger correctness guarantees. Is this a good rule of thumb for deciding which embedding to use?
使用Rosette的浅层嵌入与深层嵌入进行程序综合的充分理由是什么?
What are good reasons for using Rosette's shallow vs deep embedding for program synthesis?
推荐答案
作为一般经验法则，浅嵌入最适合使用求解器搜索程序处理的值的应用程序，这对于程序验证是很典型的和天使处决.
As a general rule of thumb, shallow embedding is best suited for applications that use the solver to search for values processed by a program, as is typical for program verification and angelic execution.
如果要进行程序综合并搜索(表示值的)代码，则深层嵌入是最佳选择.
Deep embedding is the best choice if you are doing program synthesis and searching for (values that represent) code.
如果您的应用程序将仅搜索常量，则浅嵌入可能是程序综合的不错选择.但是，如果您要搜索更复杂的内容(例如表达式或语句)，则深层嵌入是解决之道.
Shallow embedding can be a good choice for program synthesis if your application will be searching just for constants. But if you are searching for anything more complex (e.g., expressions or statements), deep embedding is the way to go.
使用浅层嵌入，您对Rosette将搜索的程序空间的控制有限.基本上，您仅限于可以使用Rosette基于宏的素描构造进行编码的任何东西.这些允许您定义基本的搜索空间并编写快速的原型，但是如果您想构建一个可扩展的工具，则需要对搜索空间进行严格控制.
With a shallow embedding, you have limited control of the space of programs that Rosette will search. Basically, you're limited to whatever can be encoded with Rosette's macro-based sketching constructs. These allow you to define basic search spaces and write quick prototypes, but if you want to build a tool that scales, you'll want tight control of the search space.
通过深度嵌入，您可以完全控制要搜索的程序的空间.本质上，您可以编写任意的Rosette/Racket函数来生成表示所有要搜索的具体程序的符号程序.然后，您还可以完全控制最后一步，即代码生成.一旦Rosette返回表示您深层嵌入中的程序的值(例如AST)，您就可以对其进行处理，但要生成代码.通过浅层嵌入，您将只能使用Rosette的内置代码生成器.
With a deep embedding, you have total control of the space of programs that will be searched. Essentially, you can write arbitrary Rosette / Racket functions to generate the symbolic program that represents all concrete programs to be searched. You then also have total control over the final step, which is code generation. Once Rosette returns a value (e.g., an AST) that represents a program in your deep embedding, you can process it however you want to generate code. With a shallow embedding, you are limited to using Rosette's built-in code generator.
因此，总而言之，如果您正在或计划进行综合，请使用深层嵌入.对于其他所有内容(验证和天使执行)，浅层嵌入将更容易，更快.
So, to conclude, if you are doing or plan to do synthesis, use a deep embedding. For everything else (verification and angelic execution), shallow embedding will be easier and quicker.
这篇关于什么时候应该使用Rosette的浅层嵌入与深层嵌入进行程序综合?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！