lambda 表达式中的递归答案

【问题标题】：Recursion in a lambda expressionlambda 表达式中的递归
【发布时间】：2021-04-24 22:36:28
【问题描述】：

是否可以在 Isabelle/HOL 中编写递归 lambda 表达式？如果有，怎么做？

例如（一个愚蠢的）：

fun thing :: "nat ⇒ nat" where
  "thing x = (λx. if x=0 then x else …) x"

所以不是……我想编写应用于 x-1 的 λ 函数。

我该怎么做？提前致谢。

【问题讨论】：

标签： lambda isabelle lambda-calculus hol

【解决方案1】：

只有一种情况是必要的：在证明中定义函数时。我已经这样做了，但这远非初学者友好，因为您必须手动推导出 simp 规则。

解决方案是模仿fun 在内部所做的事情，并用rec_nat 表达您的定义：

fun thing :: "nat ⇒ nat" where
  "thing x = rec_nat 0 (λ_ x. if x=0 then x else (x-1)) x"

(*simp rules*)
lemma thing_simps[simp]:
  ‹thing 0 = 0›
  ‹thing (Suc n) = thing n - Suc 0›
  unfolding thing_def
  by simp_all

除非不可避免，否则我不建议这样做......

【讨论】：

我的建议是不要这样做。有一个用于列表的原始递归运算符 (rec_list)，您可以使用它，但尤其是当事情变得更复杂时，我不建议这样做。只需使用fun/function/primrec 等定义一个显式辅助函数（特别是因为无论如何您可能都必须证明有关此辅助函数的辅助定理）
我同意曼努埃尔的观点。可以使用rec，但这不是一个好主意，尤其是当模式很复杂时。