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

Question

是否可以在 Isabelle 中为使用某个递归函数 f_helper 定义的函数 f 生成代码，其中 f_helper 通常不会终止，但总是会终止在 f?

中应用于它的输入

例如，我目前正在尝试使用与以下函数非常相似的函数 f_helper，该函数在有限自动机上执行幂集构造 - 在每个递归步骤中从自动机的转换集计算(transitions) 和一组在此步骤中要考虑的 powerset 构造状态 (todo) powerset 构造中的转换源自 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 是无限的并且允许不访问任何状态两次的无限路径），但是如果参数是有限的并且它应该如果初始 todo 是自动机状态集的幂集的子集并且初始 result_ 集为空，则很容易证明 f_helper 的任何使用都会终止，在这种情况下，每个递归步骤都必须在 result_states 中插入一些新元素，而该集合也是自动机状态的（有限）幂集的子集。

然后考虑以下使用 f_helper 的函数 f，其中函数 transitions 和 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}} {} {}"

我希望能够为 f 生成代码，尽管在一般情况下我无法证明 f_helper 的终止，但仅针对参数的某些假设（在 f). 我知道我可能可以通过检查 f_helper 来确保这些假设，但我相信这会导致代码效率非常低下。

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

Answer 1

因为你的函数 f_helper 是尾递归的，你应该能够通过 partial_function 定义 f f_helper 如下：

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

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

最好的，雷内

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

Isabelle code generation for terminating uses of possibly non-terminating functions

isabelle