先决知识
- Dart 是一种编程语言。Dart 3 是 Dart 的第三个主要版本。
- Dart 3 引入了记录（records），它们基本上是带有可选标签的元组。
- Dart 是一种类 C 语言。
final声明了一个具有推断类型的变量。 - 最后一节需要一些关于命题演算和形式语言的知识。在此文章中介绍这些超出了范围。
Dart 中的括号
Dart 3 将记录引入了语言。() 是一个**空记录**。使用它可能会产生有趣的语法。
final a = (); // empty record
final b = ((),); // record holding a single empty record
final c = ((), ()); // record holding two empty records
请注意，示例 `b` 末尾有一个逗号。单元素记录需要此逗号来将其与稍后介绍的不同表达式区分开。
括号在 Dart 中还有其他几种用途，但我们将只关注另外两种。
首先，它们用于**分组表达式**以指示优先级。
final a = (1 + 2) * (3 - 4); // first add, then subtract, then multiply
final b = (123) + ((312)); // a no-op grouping of literals, equivalent to `123 + 321`
混合空记录和分组，我们得到一个新表达式。
final a = (()); // a no-op grouping of an empty record, equivalent to just `()`
final b = ((())); // same as above
所以 `((),)` 是一个包含单个空记录的记录，而 `(())` 只是 `()`，即一个空记录。
最后，括号的另一种用法是**函数调用表达式**。函数在 Dart 中是一等公民，因此您可以调用存储在变量中的函数。
final a = func(); // calls `func`
final b = returnFunc()(); // calls `returnFunc` and then calls the function that was returned
混合空记录和调用表达式，我们得到：
final a = func(()); // calls `func` with a single argument, the empty record
final b = func((),); // same as above
最后，将分组也加入其中，我们得到：
final a = func((())); // calls `func` with a single no-op grouped empty record, equivalent to `func(())`
final b = func(((),)); // calls `func` with a single record holding a single empty record
这介绍了我们解决当前问题（尚未介绍的问题）所需的所有括号用法。
调用重载
现在我们继续介绍将需要的另外三个 Dart 功能：可调用对象、扩展和可选参数。
类似于可以为类型重载 `+` 运算符，Dart 允许您**重载调用调用**。这是通过实现一个名为 `call` 的方法来完成的。这使得实例表现得像函数。
class StringLength {
StringLength(this.multiplier);
final int multiplier;
int call(String param) {
return param.length * multiplier;
}
}
final a = StringLength(3)('asd'); // constructs an instance of `StringLength` and calls this instance like a function
**扩展**允许您为现有类型添加新方法，这对在您的库之外定义的类型最有帮助。
extension on int {
int negate() => -this; // `=>` is a shorthand for immediately returning a value
}
final a = 123.negate(); // calls the attached method `negate` with `this = 123`
更重要的是，您可以使用扩展来重载调用调用。
extension on int {
int call() => this * 2;
}
final a = 123(); // calls `123` as if it were a function
完成拼图的最后一块是**可选参数**。这些参数是可以提供的，但不是必须的。
extension on int {
int call([int? multiplier]) {
if (multiplier != null) {
return this * multiplier;
} else {
return this;
}
}
}
final a = 123(); // calls `123` with `multiplier = null`
final b = 123(321); // calls `123` with `multiplier = 321`
将所有内容整合在一起
现在我们可以深入研究疯狂了。
extension on () {
() call([()? _]) => ();
}
final a = (())()(())()(()())()(((()()))())(((())));
这是使用**所有已介绍概念**的完全有效的 Dart 程序。让我们分解一下。
- 我们重载了空记录的调用调用。这使得 `final a = ()();` 有效，首先创建一个空记录，然后调用它。
- 我们接受一个类型为空记录的可选参数。这使得 `final a = ()(());` 有效，首先创建一个空记录，然后用一个空记录调用它。
- 我们返回一个空记录。这使得 `final a = ()()();` 有效，第一个 `()` 对是空记录，所有后续的对都是调用表达式。
- 我们添加了一些分组表达式。`final a = ((())())();` 等同于 `final a = ()()();`。
所以，尽管这些都只是括号，但它们代表了三种不同的功能。
平衡括号问题
我们终于可以使用引入的工具来解决一个实际问题：平衡括号。给定一个仅包含 `(` 和 `)` 字符的字符串，它是否具有以下属性：每个右括号都出现在其对应的左括号之后，反之亦然。一些例子：
- `()()` - 平衡
- `(())` - 平衡
- `(()(()))` - 平衡
- `())` - 不平衡，多余的右括号
- `(` - 不平衡，左括号从未闭合
- `(()())(()` - 不平衡，左括号从未闭合
请注意，平衡括号看起来像有效的 Dart 括号表达式，而不平衡括号看起来像无效的 Dart 括号表达式（我使用“Dart 括号表达式”来指代仅使用括号并对空记录重载 `call` 扩展的表达式）。这里，我们假设空字符串不平衡，因为它显然不是一个有效表达式。似乎存在一种等价关系，但在我们证明这一点之前，让我们编写一个将使用此（*暂时*）猜想的函数。
import 'dart:io';
void main() {
print(areParenthesesBalanced("()()(())()(()())()(((()()))())((((((()))))))"));
}
bool areParenthesesBalanced(String s) {
// sanity check if the input is up to assumptions
if (!RegExp(r'^[\(\)]*$').hasMatch(s)) return false;
final program = '''
extension on () {
() call([()? _]) => ();
}
void main() {
final _ = $s;
}
''';
final file = File(
Directory.systemTemp.createTempSync().path +
Platform.pathSeparator +
'main.dart',
)..writeAsStringSync(program);
final result = Process.runSync('dart', ['analyze', file.path]);
return result.exitCode == 0;
}
我们构建一个程序源代码，该程序将使用这些括号作为表达式。我们还定义了 `()` 上的 `call` 重载。我们将此代码写入操作系统临时文件夹中的某个文件，并对其运行 `dart analyze`。如果分析器报告没有错误（退出代码为零），则括号是平衡的。瞧。
引入一点严谨性
我推测所有平衡的括号字符串都代表一个有效的 Dart 括号表达式，而所有不平衡的括号字符串都代表一个无效的 Dart 括号表达式。
设 $b$ 为平衡字符串，$e$ 为有效的 Dart 括号表达式（则 $\neg b$ 为不平衡字符串，$\neg e$ 为无效的 Dart 括号表达式）。那么在命题演算中，我们的陈述是：$(b \implies e) \land (\neg b \implies \neg e)$，简化后我们发现这是一个非常强的陈述。
$$ \begin{align} (b \implies e) \land (\neg b \implies \neg e) &= (b \implies e) \land (\neg \neg b \lor \neg e) \\ &= (b \implies e) \land (b \lor \neg e) \\ &= (b \implies e) \land (\neg e \lor b) \\ &= (b \implies e) \land (e \implies b) \\ &= b \iff e \\ \end{align} $$
在 $(1)$ 我们使用规则 $(b \implies e) \equiv (\neg b \lor e)$。在 $(2)$ 我们消除了两个否定。在 $(3)$ 我们交换逻辑或的运算数（我们可以这样做，逻辑或具有交换性）。然后我们在 $(4)$ 中使用蕴涵规则，最后在 $(5)$ 中使用 iff 的定义，即 $(b \iff e) \equiv ((b \implies e) \land (e \implies b))$。
这意味着括号平衡当且仅当它们形成一个有效的 Dart 括号表达式。通常人们会通过证明两个蕴涵来证明这一点，但在这里我们将通过表明所有平衡括号的语言等于所有有效 Dart 括号表达式的语言来证明。等价地说，我们将表明用于生成两者的语法是相同的。
设 $B$ 为所有平衡括号的语言，$G_b$ 为其语法（即，由 $G_b$ 生成的语言为 $B$：$L(G_b) = B$）。类似地，设 $E$ 为所有有效 Dart 括号表达式的语言，$G_e$ 为其语法（即，由 $G_e$ 生成的语言为 $E$：$L(G_e) = E$）。
$G_b$ 语法
让我们开始展示 $G_b$ 的产生式。
$$ \begin{aligned} S &\to A \text{ ‘(‘ } A \text{ ‘)’} \\ A &\to A \text{ ‘(‘ } A \text{ ‘)’} \quad | \quad \varepsilon \\ \end{aligned} $$
$S$ 是语法的起始符号，我们可以用它来推导出所有可能的平衡字符串。括号总是成对出现的（产生式以成对引入括号），可以嵌套，也可以并列出现。
我们还可以通过内联使用 epsilon 产生式的情况来进一步简化它，从而消除 $A$ 产生式。
$$ \begin{aligned} S &\to A \text{ ‘(‘ } A \text{ ‘)’} \quad | \quad \text{‘(‘ } A \text{ ‘)’} \quad | \quad A \text{ ‘(‘ ‘)’} \quad | \quad \text{‘(‘ ‘)’} \\ A &\to A \text{ ‘(‘ } A \text{ ‘)’} \quad | \quad \text{‘(‘ } A \text{ ‘)’} \quad | \quad A \text{ ‘(‘ ‘)’} \quad | \quad \text{‘(‘ ‘)’} \\ \end{aligned} $$
这导致两个相同的产生式，所以我们可以只保留 $S$。
$$ S \to S \text{ ‘(‘ } S \text{ ‘)’} \quad | \quad \text{‘(‘ } S \text{ ‘)’} \quad | \quad S \text{ ‘(‘ ‘)’} \quad | \quad \text{‘(‘ ‘)’} $$
$G_e$ 语法
对于 $G_e$，我们将定义更多产生式，每个产生式都编码了 Dart 括号表达式的某种语义。
首先，我们可以生成空记录。
$$ \text{Record} \to \text{‘(‘ ‘)’} $$
但我们也可以分组任何表达式。
$$ \text{Group} \to \text{‘(‘ } \text{Expression} \text{ ‘)’} $$
但我们也可以调用任何表达式（因为每个表达式都计算为一个空记录），可能带有一个参数，该参数也是一个表达式。
$$ \text{Invoke} \to \text{Expression} \text{ ‘(‘ ‘)’} \quad | \quad \text{Expression} \text{ ‘(‘ } \text{Expression} \text{ ‘)’} $$
这结束了括号的三种不同用法。主要产生式是：
$$ \text{Expression} \to \text{Record} \quad | \quad \text{Group} \quad | \quad \text{Invoke} $$
$G_b \stackrel{?}{=} G_e$
我们有 $G_b$ 和 $G_e$。是时候证明它们实际上是等价的。让我们先内联整个 $\text{Expression}$ 产生式。
$$ \begin{aligned} \text{Expression} \to & \\ & \text{‘(‘ ‘)’} \\ &| \quad \text{‘(‘ } \text{Expression} \text{ ‘)’} \\ &| \quad \text{Expression} \text{ ‘(‘ ‘)’} \quad | \quad \text{Expression} \text{ ‘(‘ } \text{Expression} \text{ ‘)’} \\ \end{aligned} $$
然后……就这样。用 $S$ 替换 $\text{Expression}$，我们可以看到这两个产生式完全相同。因此，$G_b = G_e$，所以 $B = E$，所以 $b \iff e$ $\square$。
我在这里做了一个微妙的假设：为两种语言提供的语法是正确的。我从未证明过提供的语法实际上生成了相关的语言。
这些语言（或者在这个阶段，“这种语言”）不是正则的。一个有见地的推论是，您无法使用正则表达式确定括号字符串是否平衡。语言比正则语言高一个类别，它是上下文无关的（通过之前编写其上下文无关语法可以轻松证明）。证明它不是上下文无关的草图：使用泵引理的逆否命题，我们考虑单词 $(^N)^N$，它属于该语言，但泵送它只会移除/添加左括号，使字符串不平衡，从而使其不在该语言中。
- 关于 Hacker news 的讨论
- 在 Github 上贡献更正。
