语言句法演化及其语义保存

Posted 2023-02-24

【中文标题】语言句法演化及其语义保存

【英文标题】：Language syntax evolution and its semantics preservation

【发布时间】：2011-04-16 10:45:41

【问题描述】：

我正在研究语言的句法演变如何影响其语义。例如，java 的 for 循环语法在其版本 5 中演变为紧凑的语法。设计者是否必须证明即使使用这种语法仍保留语义！可能这是一个微不足道的例子。

那么，一般来说，如何证明一种语言的语义仍然保留，即使它的语法已经从非常冗长演变为紧凑？

非常感谢您提供任何见解/链接。

科坦

【问题讨论】：

所以你问的是如何证明语法糖是正确实现的？ o.O

好吧，我的例子是关于语法糖的，但是如果有一个重要的转换怎么办。让我再举一个例子；比如说从过程风格语法到数组编程风格，例如 C = A + B，其中 A、B 和 C 是数组，这里的语义是在数组 A 和 B 的相应索引处添加内容并加载它们到 C.

我还是不明白你想要证明什么：具体实现是正确的吗？语言规范中的定义与例如同步数学定义？初学者教程中的简化描述是否准确？ ...？

一些更具体的细节：我们有一个解释器以非常冗长的语法理解语言 A。现在，我们发明了一种新的语言 B，它的语法非常紧凑，与 A 完全不同。所以，用户现在可以用紧凑的语言 B 编写代码，使用我拥有的翻译程序翻译成冗长的语言 A书面。问题是如何证明/保证所有可能的此类翻译将保留口译员理解的原始语言A的语义。

IMO 你试图证明错误的事情。你实际上要证明的是，你的翻译结果按照B的规范、翻译规则和A的规范做了它所期望的事情。A的很多方面可能在B中是无法到达的。考虑将 C++ 翻译成汇编代码。这就是每个 C++ 编译器所做的（或多或少）。汇编代码可以完成 C++ 中无法安全完成的事情，例如计算跳转或自修改代码，因此您无法证明“汇编程序的语义保留在 C++ 中”。

【参考方案1】：

证明每个语法扩展在旧版本的语言中都是非法的。

出于显而易见的原因，新的句法元素应该以在旧版本的语言中在句法上非法的方式引入。因此，大多数语言都有一个保留字列表，超出了已使用的关键字。

例如，当 C# 在 3.0 版中引入 var 关键字时，它可能会出现问题，因为 var 在 C# 1.0 版中不是保留字（在 2.0 版中也可能不是）。因此，程序可以在 C# 1.0 中合法地创建一个名为 var 的类型，但在 C# 3.0 及更高版本中不再编译。

旧语言元素的不变语义更多地取决于编译器的构建方式，因为规范很少更改。如果它改变了，那么语义就不会被保留。例外情况是新规范修复了在规范的先前版本中构成未定义行为（但仍然合法）的事物。我想到了 C。

【讨论】：

不，这只是向后兼容/证明旧语法的语义没有改变。

德尔南是对的。如果 C# 引入了一种全新的方式来表达循环/条件，隐式运算符重载会怎样。是否有可能证明这两种语法是等价的？顺便说一句，对我来说，“句法等价”是一种解释器和两种语言语法的“语义保存”的同义词。

好的，看来我误解了你的问题。如何证明 foreach 循环与 for 循环一样？通过这样指定！

【参考方案2】：

好的，你最后的评论更容易回答。

一些更具体的细节：我们有一个解释器以非常冗长的语法理解语言 A。现在，我们发明了一种新的语言 B，它的语法非常紧凑，与 A 完全不同。所以，用户现在可以用紧凑的语言 B 编写代码，使用我拥有的翻译程序翻译成冗长的语言 A书面。问题是如何证明/保证所有可能的此类翻译都将保留口译员理解的原始语言 A 的语义。

简短的回答是：你不知道。一方面，当您添加语法糖时，您通常只是捕获一个众所周知的、广泛使用的模式并赋予它特殊、更好的语法——您不会替换语言的大部分语法。对于这样小的替换，可以用信息丰富的描述和示例来制定翻译 - 例如，PEP 343 defines the "with" statement 相对信息丰富。

现在，当语法变化如此激进时，新语言与后端语言几乎没有任何共同之处，我们不是在谈论语法变化 - 我们在谈论编译器。但是编译器也没有被证明是正确的。好吧，有些人实际上是try it。但是对于现实世界的编译器来说，这种情况很少发生。相反，测试检查了无数用户及其程序的正确性。 当然，所有严肃的语言实现都有广泛的测试用例（阅读：示例程序，从基本到荒谬），至少在官方版本中应该运行并通过（或在某些情况下产生错误）。当他们这样做时（并且测试套件物有所值），您仍然不知道没有错误，但至少有一些信心。正如 Dijkstra 所说：“测试表明存在错误，而不是没有错误。”

【讨论】：

delnan，非常感谢这篇精彩、内容丰富且有见地的帖子。这为整个问题提供了一个很好的论据。我从来没有意识到我所说的翻译器确实是一种编译器！