语言实现破坏语言保证时，人们会感到困惑

<p>以下面的 Python 程序为例：</p> <div class="codehilite"><pre><span></span><code><span class="c1"># x = 1, y = 2</span> <span class="n">x</span> <span class="o">=</span> <span class="mi">0</span> <span class="n">y</span> <span class="o">=</span> <span class="n">x</span> <span class="nb">print</span><span class="p">([</span><span class="n">x</span><span class="p">,</span> <span class="n">y</span><span class="p">])</span> </code></pre></div> <p>它会打印 <code>[0, 0]</code>。如果我们交换两个赋值语句，则会打印 <code>[0, 1]</code>。每个赋值发生在独立的时间步骤中。几乎所有的命令式语言都是这样工作的。</p> <p>现在来看下面的 TLA+ 片段：</p> <div class="codehilite"><pre><span></span><code>\* x = 1, y = 2 /\ x&#39; = 0 /\ y&#39; = x /\ PrintT(&lt;&lt;x&#39;, y&#39;&gt;&gt;) </code></pre></div> <p>这会打印 <code>&lt;&lt;0, 1&gt;&gt;</code>。与命令式语言不同，TLA+ 将更新和时间步骤的概念分开。我们将 <code>x' = 0</code> 理解为“在<em>下一个</em>状态中，<code>x</code> 将为 0，但在当前状态中它仍然具有相同的值”。因此，在每个状态中，<code>x</code> 和 <code>x'</code> 本质上是不同的变量。因此，在 TLA+ 语义中，语句的顺序无关紧要，交换两个赋值不会改变打印的输出。这门语言非常巧妙！这意味着，除其他外，基本上没有步骤内的竞争条件。一个函数可以更新一个变量，而不会影响其他函数如何使用它。</p> <p>好了，现在初学者不可避免地会遇到一个问题：</p> <div class="codehilite"><pre><span></span><code>\* x = 1, y = 2 /\ x&#39; = y&#39; /\ y&#39; = x /\ PrintT(&lt;&lt;x&#39;, y&#39;&gt;&gt;) </code></pre></div> <p>这会崩溃，因为 <code>y'</code> 尚未定义。但如果交换两个赋值，这就能正常工作了，并打印 <code>&lt;&lt;1, 1&gt;&gt;</code>。显然，关于无序的说法完全是胡扯。</p> <p>嗯，并非如此。TLA+ 语义仍然保证无序。问题在于验证器并没有完美地实现 TLA+ 语义。<code>y' > 0</code> 是一个完全合理的“赋值”，但有无穷多个可能的下一个状态！因此，主模型检查器 (TLC) 要求 <code>y' = some_value</code> 出现在任何其他使用 <code>y'</code> 之前，这意味着顺序现在很重要。</p> <p>更大的问题是 <code>PrintT</code>。TLA+ 语义保证无序，因为语义不允许副作用。模型检查器添加了有副作用的运算符，如 <code>PrintT</code>、<code>Assert</code> 和 <code>IOExec</code>。这可能会导致保护语句出现问题。从理论上讲，以下两个脚本块是等价的：</p> <div class="codehilite"><pre><span></span><code>/\ x = 0 \* guard statement /\ P() /\ x&#39; = x + 1 /\ x&#39; = x + 1 /\ P() /\ x = 0 \* guard statement </code></pre></div> <p>当 <code>x = 1</code> 时，由于保护子句，这些不会导致新状态。但模型检查器逐行评估，这意味着在块 2 中，它会在到达 <code>x = 0</code> 并丢弃状态之前执行 <code>x' = x + 1</code> 和 <code>P()</code>。如果 <code>P</code> 是一个正常的 TLA+ 运算符，这没问题，但如果是 <code>PrintT</code> 或 <code>Assert</code>，它会先产生效果，导致奇怪的幽灵打印，这些打印不对应任何下一个状态。</p> <p>“TLA+ 语义保证的内容”与“TLC 可能破坏这些保证的具体方式”之间的这种差异是人们感到困惑的主要来源！除此之外，许多这些运算符，如 <code>IOExec</code> 和 <code>TLCSet</code>，都被设计为逃生舱口。所以如果你需要它们，你已经是在做一些相当奇怪的事情了，这会让事情更加混乱。</p> <p>除此之外，破坏保证的 TLC 运算符和常规安全的 TLA+ 运算符之间没有语法或视觉上的区分。在编译型语言中，你有编译指示和预处理器，它们让编译器做语言本身不能做的事情。但这些通常有视觉上不同的语法，所以你一看就知道这里有危险。</p> <p>我想起了 Neel Krishnaswami 的精彩文章<a href="https://semantic-domain.blogspot.com/2013/07/what-declarative-languages-are.html" target="_blank">《什么是声明式语言》</a><sup id="fnref:laurie"><a class="footnote-ref" href="#fn:laurie">1</a></sup>：</p> <blockquote> <p>这也让我们可以预测，任何声明式语言中最不受欢迎的特性将是那些暴露操作模型并破坏声明式语义的特性。因此我们可以预测人们会不喜欢 (a) 正则表达式中的反向引用，(b) 文法中的有序选择，(c) 查询语言中的行 ID，(d) Prolog 中的 cut，(e) 约束语言中的约束优先级。</p> </blockquote> <p>Prolog 的 cut 具有视觉上不同的语法，但使用 cut 的谓词与<a href="https://www.metalevel.at/prolog/purity" target="_blank">逻辑纯</a>谓词在视觉上并不不同。但这比我们在 TLA+ 中遇到的情况稍微不那么棘手，因为 cut 仍然是语言语义的一部分。</p> <p>（话说回来，不同的 Prolog 方言有不同的<a href="https://eu.swi-prolog.org/pldoc/man?section=printmsg" target="_blank">打印字符串</a>方式，这给 Prolog 添加了副作用，并且它们在视觉上与其他谓词没有区别。所以同样的问题！）</p> <p>我实际上对此没有任何修复。我只是觉得这是一个引人入胜的<a href="https://en.wikipedia.org/wiki/Leaky_abstraction" target="_blank">泄漏抽象</a>的例子。也许我们可以写一个代码高亮器，高亮所有传递性地使用“奇怪”函数的函数之类的。</p> <div class="footnote"> <hr /> <ol> <li id="fn:laurie"> <p><a href="https://tratt.net/laurie/blog/2013/relative_and_absolute_levels.html" target="_blank">必读的回应文章</a>&#160;<a class="footnote-backref" href="#fnref:laurie" title="跳回正文中的脚注1">&#8617;</a></p> </li> </ol> </div>