精益编程语言中的循环

Question

我开始学习Lean编程语言https://leanprover.github.io

我发现有函数、结构体、if/else 和其他常见的编程命令。

但是，我还没有找到任何处理循环的方法。有没有办法在精益中迭代或重复代码块？类似于其他语言中的 for 或 while 。如果是这样，请添加语法或示例。

提前谢谢您。

Answer 1

与其他函数式编程语言一样，Lean 中的循环主要通过递归完成。例如:

-- lean 3
def numbers : ℕ → list ℕ
| 0 := []
| (n+1) := n :: numbers n

如果您不习惯的话，这会是一种心态上的改变。请参阅:Haskell from C: Where are the for Loops?

为了使事情复杂化，Lean 区分了一般递归和结构递归。上面的例子是在 ℕ 上使用结构递归，所以我们知道它总是会停止。非停机程序可能会导致像精益这样基于 DTT 的定理证明器出现不一致，因此必须严格控制。您可以使用 meta 关键字选择一般递归:

-- lean 3
meta def foo : ℕ → ℕ
| n := if n = 100 then 0 else foo (n + 1) + 1

---

在lean 4中，do block 语法包含一个for命令，该命令可用于以更命令式的方式编写for循环。请注意，它们在底层仍然表示为尾递归函数，并且有一些类型类支持脱糖。 (此外，您需要使用 partial 关键字而不是 meta 来在精益 4 中执行一般递归。)

-- lean 4
partial def foo (n : Nat) : Nat :=
  if n = 100 then 0 else foo (n + 1) + 1

def mySum (n : Nat) : Nat := Id.run do
  let mut acc := 0
  for i in [0:n] do
    acc := acc + i
  pure acc