在涉及地图的数据类型上的功能终止证明

Question

我有以下记录语言：

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

这不会通过终止检查器，因为类型的size函数一直是0。我看不到如何在不将地图限制为有限域的情况下提供可计算的度量。

so：如何证明上述定义终止？我怀疑我必须证明一些归纳性的谓词，但我不确定如何做。

Answer 1

对于非初步恢复功能，您也可以使用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

Answer 2

您可以使用primrec：

来定义此功能

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

primrec允许您使用所涉及类型构造函数的map功能。就您而言，这是map_option和op ∘。