Isabelle 终止对包含自身映射的数据类型的函数答案

【问题标题】：Isabelle termination of function on datatypes containing maps to themselvesIsabelle 终止对包含自身映射的数据类型的函数
【发布时间】：2021-04-02 17:12:15
【问题描述】：

Isabelle 中是否可以定义一个终止递归函数f where

f 有一个 t 类型的参数，因此 t 类型的值可能包含到 t 类型的值的映射，并且
f 对此类映射范围内的所有元素执行递归调用？

例如考虑trie理论上定义的数据类型Trie_Fun：

datatype 'a trie = Nd bool "'a ⇒ 'a trie option"

以及我对一个简单函数height 的尝试，该函数旨在计算尝试的高度（具有有限多个传出边）：

theory Scratch
  imports "HOL-Data_Structures.Trie_Fun"
begin

function height :: "'a trie ⇒ nat" where
  "height (Nd _ edges) = (if dom edges = Set.empty ∨ ¬ finite (dom edges)
    then 0
    else 1 + Max (height ` ran edges))"
  by pat_completeness auto
termination (* ??? *)

end

这里lexicographic_order 不足以证明函数要终止，但到目前为止，我还无法对trie（用于终止）制定任何本身不需要类似递归的度量。我必须在这里承认，我不确定我是否正确理解了 Isabelle/HOL 中的数据类型（即，上述定义的 trie 是否实际上总是有限高度）。

是否可以显示height 终止？

【问题讨论】：

您是否尝试过在声明中添加function (domintros) 选项，然后使用归纳法作为终止证明？
非常感谢，这确实足以证明终止。您想提交您的评论作为答案，还是我可以根据您的评论自己回答问题？
如果您可以自己添加答案，包括工作终止证明，那就太好了。

标签： isabelle

【解决方案1】：

根据 Peter Zeller 的评论，我能够通过将 (domintros) 添加到定义中，然后使用事实 height.domintros 对 trie 执行归纳来证明 height 的终止，结果如下终止证明：

function (domintros) height :: "'a trie ⇒ nat" where
  "height (Nd _ edges) = (if dom edges = Set.empty ∨ ¬ finite (dom edges)
    then 0
    else 1 + Max (height ` ran edges))"
  by pat_completeness auto
termination apply auto
proof -
  fix x :: "'a trie"
  show "height_dom x"
  proof (induction)
    case (Nd b edges)

    have "(⋀x. x ∈ ran edges ⟹ height_dom x)"
    proof -
      fix x assume "x ∈ ran edges" 
      then have "∃a. edges a = Some x"
        unfolding ran_def by blast
      then have "∃a. Some x = edges a"
        by (metis (no_types))
      then have "Some x ∈ range edges"
        by blast
      then show "height_dom x"
        using Nd by auto
    qed
    then show ?case
      using height.domintros by blast
  qed
qed

【讨论】：