当前位置：首页 > news >正文

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

news 来源：原创 2025/8/22 22:15:11

作为学习 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 手册

相关文章：