Isabelle 在包含自身映射的数据类型上终止函数
Isabelle termination of function on datatypes containing maps to themselves
是否可以在 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
终止?
根据 Peter Zeller 的评论,我能够通过在定义中添加 (domintros)
然后对 trie
执行归纳来证明 height
的终止,使用事实height.domintros
,导致以下终止证明:
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
是否可以在 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
终止?
根据 Peter Zeller 的评论,我能够通过在定义中添加 (domintros)
然后对 trie
执行归纳来证明 height
的终止,使用事实height.domintros
,导致以下终止证明:
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