涉及地图的数据类型函数的终止证明

Question

我有以下语言的记录：

datatype "term" = Rcd "string ⇀ term"

fun id_term :: "term ⇒ term" 
  where "id_term (Rcd vals) = Rcd (map_option id_term ∘ vals)"

这没有通过终止检查器，因为该类型的 size 函数始终为 0。我也不知道如何在不将映射约束到有限域的情况下提供可计算的度量。

那么：如何证明上述定义的终止？我怀疑我必须证明某些归纳谓词的有根据性，但我不确定该怎么做。

Answer 1

您可以使用 primrec:

定义此函数

primrec id_term :: "term ⇒ term"
  where "id_term (Rcd vals) = Rcd (map_option id_term ∘ vals)"

primrec 允许您使用相关类型构造函数的 map 函数。在你的例子中，那是 map_option 和 op ∘.

Answer 2

对于非原始递归函数，您也可以使用 function 命令，但由于没有 size 度量，事情会变得有点复杂。本质上，你必须定义一个子项关系并证明它是有根据的，然后你可以用它来证明你的函数终止：

datatype "term" = Rcd "string ⇀ term"

inductive subterm :: "term ⇒ term ⇒ bool" where
  "t ∈ ran f ⟹ subterm t (Rcd f)"

lemma accp_subterm: "Wellfounded.accp subterm t"
proof (induction t)
  case (Rcd f)
  have IH: "Wellfounded.accp subterm t" if "t ∈ ran f" for t
    using Rcd[of "Some t" t] and that by (auto simp: eq_commute ran_def)
  show ?case by (rule accpI) (auto intro: IH elim!: subterm.cases)
qed

definition subterm_rel where "subterm_rel = {(t, Rcd f) |f t. t ∈ ran f}"

lemma subterm_rel_altdef: "subterm_rel = {(s, t) |s t. subterm s t}"
  by (auto simp: subterm_rel_def subterm.simps)

lemma subterm_relI [intro]: "t ∈ ran f ⟹ (t, Rcd f) ∈ subterm_rel"
  by (simp add: subterm_rel_def)

lemma subterm_relI' [intro]: "Some t = f x ⟹ (t, Rcd f) ∈ subterm_rel"
  by (auto simp: subterm_rel_def ran_def)

lemma wf_subterm_rel [simp, intro]: "wf subterm_rel"
  using accp_subterm unfolding subterm_rel_altdef accp_eq_acc wf_acc_iff by simp

function id_term :: "term ⇒ term" 
  where "id_term (Rcd vals) = Rcd (map_option id_term ∘ vals)"
by pat_completeness simp_all
termination by (relation subterm_rel) auto

涉及地图的数据类型函数的终止证明

Termination proof for function on datatype involving a map

termination

isabelle