问题描述
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
应该适合代码生成。
最好的, 雷内