Isabelle 代码生成用于终止可能非终止函数的使用

如何解决Isabelle 代码生成用于终止可能非终止函数的使用

Isabelle 是否可以为使用递归函数 f 定义的函数 f_helper 生成代码，其中 f_helper 通常不会终止，但对于应用的输入总是终止在f？

例如，我目前正在尝试使用与以下函数 f_helper 非常相似的函数，该函数在有限自动机上执行幂集构造 - 在每个递归步骤中，从自动机 ({ {1}}) 和在此步骤中要考虑的幂集构造的一组状态 (transitions) 源于 todo 中的状态的幂集构造中的转换以及这些转换所达到的状态（ todo-参数携带中间结果）：

result_

这个函数当然不会因任意输入而终止（例如，如果 function f_helper :: "('a × 'b × 'a) set ⇒ 'a set set ⇒ 'a set set ⇒ ('a set × 'b × 'a set) set ⇒ 'a set set × ('a set × 'b × 'a set) set" where "f_helper transitions todo result_states result_transitions= (let new_transitions = ⋃ q ∈ todo . (let q_transitions = {t ∈ transitions . fst t ∈ q}; labels = (fst ∘ snd) ` q_transitions in (λ b . (q,b,(snd ∘ snd) ` {t ∈ q_transitions . (fst ∘ snd) t = b})) ` labels); result_transitions' = result_transitions ∪ new_transitions; result_states' = result_states ∪ todo; todo' = ((snd ∘ snd) ` new_transitions) - result_states' in if todo' = {} then (result_states',result_transitions') else f_helper transitions todo' result_states' result_transitions')" 是无限的并且允许不访问任何状态两次的无限路径），但是如果参数是有限的，它会终止并且应该很容易如果另外初始 transitions 是自动机状态集的幂集的子集并且初始 f_helper-sets 为空，则证明 todo 的任何使用是终止的，如在这种情况下，每个递归步骤都必须向 result_ 中插入一些新元素，而该集合也是自动机状态的（有限）幂集的子集。

然后考虑使用result_states的以下函数f，其中函数f_helper和transitions分别提取有限的转换集和自动机{{1}的初始状态}}：

initial

我希望能够为 a 生成代码，即使我无法证明在一般情况下 fun f :: "('a,'b) automaton ⇒ 'a set set × ('a set × 'b × 'a set) set" where "f a = f_helper (transitions a) {{initial a}} {} {}" 的终止，但仅针对参数的某些假设（在 {{1 }}）。 我知道我可能可以通过检查 f 来确保这些假设，但我相信这会导致代码效率非常低。

是否有一种方法可以仅在 f_helper 的上下文中定义递归函数 f 以避免必须证明 f_helper 的终止对于不相关的输入（无限集等） )？

解决方法

由于您的函数 f_helper 是尾递归的，您应该能够通过 f f_helper 定义 partial_function，如下所示：

partial_function (tailrec) f_helper :: ... where 
  [code]: "f_helper transitions todo result_states result_transitions = ..."  

然后 f_helper 应该适合代码生成。

最好的， 雷内