精益编程语言中的循环

Question

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

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

然而，我还没有找到任何可以处理loops的东西。在精益中有迭代或重复代码块的方法吗？类似于其他语言中的for或while。如果是这样的话，请添加语法或一个例子。

提前谢谢你。

Answer 1

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

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

如果你不习惯的话，这是一种心态的改变。请参阅：C公司的Haskell : for Loops在哪里？

更复杂的是，精益区分了一般递归和结构递归。上面的例子是在ℕ上使用结构递归，所以我们知道它总是停止。不停止程序会导致基于DTT的定理验证器(如lean )的不一致性，因此必须严格控制。您可以使用meta关键字选择一般递归：

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

在精益4中，do块语法包括一个for命令，该命令可以用来以更命令式的方式为循环编写。请注意，它们仍然被表示为幕后的尾递归函数，并且有一些类型类型为去标记提供了动力。(在精益4中，您还需要使用partial关键字而不是meta来执行一般递归。)

-- 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