精益编程语言中的循环

Question

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

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

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

先感谢您。

Answer 1

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

\n

-- lean 3\ndef numbers : \xe2\x84\x95 \xe2\x86\x92 list \xe2\x84\x95\n| 0 := []\n| (n+1) := n :: numbers n\n

\n

如果您不习惯的话，这会稍微改变一下心态。请参阅：来自 C 的 Haskell：for 循环在哪里？

\n

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

\n

-- lean 3\nmeta def foo : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\x95\n| n := if n = 100 then 0 else foo (n + 1) + 1\n

\n\n

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

\n

-- lean 4\npartial def foo (n : Nat) : Nat :=\n  if n = 100 then 0 else foo (n + 1) + 1\n\ndef mySum (n : Nat) : Nat := Id.run do\n  let mut acc := 0\n  for i in [0:n] do\n    acc := acc + i\n  pure acc\n

\n