自然数游戏-乘法世界1~3关，一窥 Lean 的命名范式

在 Lean 的命名范式中，mul_succ 和 succ_mul 的命名规则体现了以下核心原则：

1. 动词优先的命名逻辑

Lean 的函数名通常以操作动词开头，后接操作对象或条件。例如：

• add （加法）、 mul （乘法）是基础运算动词；
• succ （后继函数，即 n + 1 ）是自然数中的核心操作。

因此：

• mul_succ 表示“乘法后应用后继操作”，即 mul a (succ b) ，对应数学中的 a * (b + 1) 。
• succ_mul 表示“先应用后继再相乘”，即 succ (mul a b) ，对应数学中的 (a + 1) * b 。

这种命名范式直接反映了运算的执行顺序和逻辑优先级。

2. 参数顺序的显式性

Lean 函数名的参数顺序通常与数学表达式中的左结合性一致。例如：

• mul a b 对应 a * b ；
• succ_mul a b 对应 (a + 1) * b ，即先对 a 应用 succ ，再与 b 相乘。

这与数学中的运算顺序一致，符合直觉。而 mul_succ a b 则对应 a * (b + 1)，即先对 b 应用 succ，再与 a 相乘。

3. 数学运算的分配律映射

在自然数乘法中，分配律是核心性质：

• 左分配律 ： succ a * b = a * b + b → 对应 succ_mul a b ；
• 右分配律 ： a * succ b = a * b + a → 对应 mul_succ a b 。

这种命名方式将数学性质直接编码到函数名中，便于开发者通过名称快速理解其数学含义。

4. 与标准库的命名一致性

Lean 的标准数学库（Mathlib）遵循类似的命名规则。例如：

• nat.add_succ ： a + (b + 1) = (a + b) + 1 ；
• nat.mul_succ ： a * (b + 1) = a * b + a 。

这种一致性降低了学习成本，使开发者能通过已有知识推测新函数的行为。

5. 函数式编程的柯里化特性

Lean 支持柯里化（Currying），即多参数函数可逐步应用。例如：

• mul_succ a 是一个函数，接受 b 后返回 a * (b + 1) ；
• succ_mul a 同理，返回 (a + 1) * b 。

这种设计使得函数组合和部分应用更加直观。

总结

在自然数游戏中，mul_succ 和 succ_mul 的命名体现了 Lean 的以下范式：

1. 动词优先 ：操作行为在前；
2. 参数顺序明确 ：左结合性对应数学表达式；
3. 数学性质编码 ：通过名称直接反映分配律等性质；
4. 与标准库一致 ：降低认知负担。

这种命名范式不仅符合函数式编程的惯例，也与数学的形式化表达高度契合，是 Lean 作为定理证明器和编程语言统一设计哲学的体现。

转载自久章智能（微信公众号，久章智能于 2025-06-04 转载），内容保持原貌，版权归原作者及原账号所有。阅读原文 ↗