形式化数学——Lean求值表达式

作为学习 Lean 的程序员，最重要的是理解求值的工作原理。求值是求得表达式的值的过程，就 像算术那样。例如，15 - 6 的值为 9，2 × (3 + 1) 的值为 8。要得到后一个表达式的值，首先将 3 + 1 替换为 4，得到 2 × 4，它本身又可以归约为 8。有时，数学表达式包含变量:在知道 x 的 值之前，无法计算 x + 1 的值。在 Lean 中，程序首先是表达式，思考计算的主要方式是对表达 式求值。

大多数编程语言都是命令式的(Imperative)，其中程序由一系列语句组成，这些语句会按顺 序执行以得到程序的结果。程序可以访问可变内存，因此变量引用的值可以随时间而改变。除 了可变状态外，程序还可能产生其他副作用，例如删除文件、建立传出的网络连接、抛出或捕 获异常以及从数据库读取数据等等。「副作用(Side Effect)」本质上是一个统称，用于描述 程序运行过程中可能发生的事情，这些事情不遵循数学表达式求值的模型。

然而，在 Lean 中，程序的工作方式与数学表达式相同。变量一旦被赋予一个值，就不能再被重 新赋值。求值表达式不会产生副作用。如果两个表达式的值相同，那么用一个表达式替换另一 个表达式并不会导致程序计算出不同的结果。这并不意味着不能使用 Lean 向控制台写入

Hello, world!，而是执行I/O并不是以求值表达式的方式使用Lean的核心部分。因此，本 章重点介绍如何使用 Lean 交互式地求值表达式，而下一章将介绍如何编写、编译并运行

Hello, world! 程序。要让 Lean 对一个表达式求值，请在编辑器中的表达式前面加上 #eval ，然后它会返回结果。

通常可以将光标或鼠标指针放在 #eval 上查看结果。例如，

#eval 1 + 2

会产生值 3 。Lean 遵循一般的算术运算符优先级和结合性规则。也就是说，

#eval 1 + 2 * 5

会产生值 11 而非 15 。

虽然普通的数学符号和大多数编程语言都使用括号(例如 f(x) )将函数应用到其参数上，但 Lean 只是将参数写在函数后边(例如 f x )。函数应用是最常⻅的操作之一，因此保持简洁 很重要。与其编写

 #eval String.append("Hello, ", "Lean!")

其中函数的两个参数只是写在后面用空格隔开。

就像算术运算的顺序需要在表达式中使用括号(如 (1 + 2) * 5 )表示一样，当函数的参数需 要通过另一个函数调用来计算时，括号也是必需的。例如，在

 #eval String.append "great " (String.append "oak " "tree")

中需要括号，否则第二个 String.append 将被解释为第一个函数的参数，而非一个接受 "oak " 和 "tree" 作为参数的函数。必须先得到内部 String.append 调用的值，然后才能将其追 加到 "great " 后面，从而产生最终的值 "great oak tree" 。

命令式语言通常有两种条件:根据布尔值确定要执行哪些指令的条件语句(Statement)，以 及根据布尔值确定要计算两个表达式中哪一个的条件表达式(Expression)。例如，在 C 和 C++ 中，条件语句使用 if 和 else 编写，而条件表达式使用三元运算符 ? 和 : 编写。在 Python 中，条件语句以 if 开头，而条件表达式则将 if 放在中间。由于 Lean 是一种面向表 达式的函数式语言，因此没有条件语句，只有条件表达式。条件表达式使用 if 、 then 和

else 编写。例如，

String.append "it is " (if 1 > 2 then "yes" else "no")

会求值为

String.append "it is " (if false then "yes" else "no") 

进而求值为

String.append "it is " "no" 

最终求值为 "it is no" 。

为简洁起见，有时会用箭头表示一系列求值步骤:

 String.append "it is " (if 1 > 2 then "yes" else "no") ===> String.append "it is " (if false then "yes" else "no") ===> String.append "it is " "no" ===> "it is no"

可能会遇到的信息

让 Lean 对缺少参数的函数应用进行求值会产生错误信息。举例来说，

#eval String.append "it is "

会产生一个很长的错误信息:

 expression   String.append "it is " has type   String → String but instance   Lean.MetaEval (String → String) failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

表达式   String.append "it is "类型为   String → String但实例Lean.MetaEval (String → String)合成失败，此实例指示 Lean 如何显示结果值，回想一下任何实现了 `Repr` 类的类型也实现了 `Lean.MetaEval` 类。

会出现此信息是因为在 Lean 中，仅接受了部分参数的函数会返回一个等待其余参数的新函数。 Lean 无法向用户显示函数，因此在被要求这样做时会返回错误。

---

练习

以下表达式的值是什么?请手动计算，然后输入 Lean 来检查你的答案。

42 + 19     

String.append "A" (String.append "B" "C")      

String.append (String.append "A" "B") "C"     

if 3 == 3 then 5 else 7     

if 3 == 4 then "equal" else "not equal"

---

本文参考

David Thrane Christiansen, 《Lean on functional programming》

Lean-zh 项目组，译

Lean 手册