lambda - lambda 表达式中的递归

Question

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

例如（一个愚蠢的）：

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

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

我该怎么做？提前致谢。

Answer 1

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

解决方案是模仿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

我不建议这样做，除非它是不可避免的......