在Isabelle中是否有可能为使用递归函数f_helper定义的函数f生成代码，其中f_helper通常不终止，但在f中应用于它的输入总是终止?
例如,我目前试图使用一个函数非常类似于以下函数f_helper执行powerset建设有限自动机——在每个递归步骤计算组转换的自动机(transitions)和一组的powerset建设要考虑在这一步(todo)转换在todopowerset建设来自州和美国达成的那些转换(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的终止?
由于您的函数f_helper是尾递归的，您应该能够通过partial_function定义f f_helper，如下所示:
partial_function (tailrec) f_helper :: ... where
[code]: "f_helper transitions todo result_states result_transitions = ..."
然后f_helper应该适合代码生成。
最好的,Rene