dsl - 构建规范语言表示的一般复杂性是多少？

Question

拥有语言的规范表示通常很方便（在我的情况下，它们通常是特定领域的语言）；但是，我相信所涉及的语言的表达能力有严格的限制，这些语言决定了是否可以为该语言的任意程序确定和/或创建规范形式。不幸的是，我一直找不到我（模糊地）记得在其中读过的参考资料。

一方面，创建语言的规范表示与许多硬图问题（例如：图同构）具有相当的复杂性似乎是合理的，但另一方面，iirc、gcc、yhc 和 ghc 等编译器使用中间表示生成各种格式的输出（程序集、javascript 等），所以这至少在某些形式下是一个已解决的问题。

何时可以确定/生成给定语言的规范形式？（该语言的表达能力如何，语言表达能力如何影响规范形式的效用？）如果可能，请提供参考或证明。

编辑：例如，正则语言（例如：正则表达式的“纯”形式）不能表达图灵完备语言所能表达的许多相同的东西。换句话说，您不能用常规语言编写 Web 服务器，但可以使用 lambda 演算）。我的问题是关于理论上的可能性，并且确实有与复杂性理论有关的具体答案。如果我有一个 DSL 需要传输到另一个系统，那么在传输它之前生成该代码的规范形式通常是有益的，因为这将解耦两个不同系统使用的独立表示。 然而，如果将图灵完备语言翻译成规范形式是 P-Space 完备或 NP-Complete，那么您不应该浪费时间尝试构建规范形式——要么找到另一种方法，要么减少可以在多项式时间内规范化的语言复杂性。

Answer 1

通过“规范表示”，我假设您的意思如下：如果程序P和Q 在相同的输入上“做同样的事情”，则它们是等效的。“做同样的事情”意味着程序具有相同的输出，并且两个程序在有限时间后停止或都进入无限循环。这种等价关系定义了所有程序集合中的等价类。程序P的“规范表示”是属于同一等价类的程序P' ，并且您要求同一等价类的所有成员具有相同的规范表示。

对于图灵完备的语言，图灵可计算的规范表示将使您能够解决停机问题，如下所示：首先编写一个由无限循环组成的程序并找到其规范表示Q。然后对于任何输入程序P，首先将它机械地转换成一个程序P ₀，除了它不产生输出之外，它做同样的事情，然后找到这个程序的规范表示P ₀ '。如果结果是Q，您知道P ₀不会停止，因此P也不会。否则，P ₀停止，P 也停止.

要获得更多乐趣，请阅读Gregory Chaitin关于他所谓的“优雅”程序的一些作品。

Answer 2

在我看来，编译成汇编语言可以归类为以实用的方式翻译成规范形式。