非终止归纳谓词

Question

在优秀的Programming and Proving in Isabelle/HOL里面写着

[...] in contrast to recursive functions, there is no termination requirement for inductive definitions. (pdf p. 40)

这是否意味着在归纳定义中可以有无限深的推导树？
这种非终止推导的例子是什么（最好是无限高的推导）？你如何'construct'这些？
关于这些的规则归纳原则如何仍然合理？

Answer 1

没有。为此，您需要合归纳谓词。
不存在。
如果你看一下归纳原理，你会发现他们还有一个额外的前提。例如，"even n"。这意味着，在您甚至可以应用归纳原理之前，您需要知道手头有一个有限推导。

Answer 2

Lars 已经回答了这个问题，但我想扩展他提到的余归谓词。这些确实允许你拥有“无限深的派生树”，对应于 codatatypes 本质上是“可能无限的数据类型”。

一个很好的例子是来自 ~~/src/HOL/Library/Stream 的 stream 类型：

codatatype 'a stream = SCons 'a "'a stream" (infixr "##" 65)

这是一个无限列表（请注意，与 Haskell 列表不同，此流类型必须无限长，就像您写 datatype Stream a = SCons a (Stream a)在 Haskell 中，虽然 Haskell 风格的“潜在无限”列表也可能是直接的，请参见 AFP 中的惰性列表）

然后您可以例如定义其值来自给定集合的所有流的集合。您可以将其定义为 streams A = {s. sset s ⊆ A}，但在 Isabelle 中，它是这样定义的：

coinductive_set streams :: "'a set ⇒ 'a stream set" for A :: "'a set"
  where "⟦a ∈ A; s ∈ streams A⟧ ⟹ a ## s ∈ streams A"

另一个可能更简单的例子是流上的“对所有元素”谓词的上推：

coinductive sall :: "('a ⇒ bool) ⇒ 'a stream ⇒ bool" for P :: "'a ⇒ bool" where
  "P x ⟹ sall P xs ⟹ sall P (x ## xs)"

至于如何构建这样一棵无限推导树，即证明一个余归纳谓词持有某个值的问题，你必须用余归纳来做。例如。我们可以证明如果 P x 成立，那么 sall P (sconst x) 成立，其中 sconst x 只是值 x 无限重复：

lemma sconst_reduce: "sconst x = x ## sconst x"
  by (subst siterate.code) simp_all

lemma sall_sconst: "P x ⟹ sall P (sconst x)"
proof (coinduction rule: sall.coinduct)
  assume "P x"
  thus "∃y ys. sconst x = y ## ys ∧ P y ∧ (ys = sconst x ∧ P x ∨ sall P ys)"
    by (subst sconst_reduce) auto
qed

非终止归纳谓词

Non-terminating inductive predicates

isabelle

induction

non-termination