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

Question

Is it possible in Isabelle to generate code for a function f that is defined using some recursive function f_helper where f_helper does not terminate in general but does always terminate for the inputs applied to it in f?

For example, I am currently trying to use a function very similar to the following function f_helper that performs a powerset construction on a finite automaton - in each recursive step calculating from the set of transitions of the automaton (transitions) and a set of states of the powerset construction to consider in this step (todo) the transitions in the powerset construction originating from states in todo and the states reached by those transitions (the result_-parameters carry the intermediate results):

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')"

This function does of course not terminate for arbitrary inputs (e.g. if transitions is infinite and allows infinite paths that do not visit any state twice), but it does terminate if the arguments are finite and it should be easy to prove any use of f_helper to be terminating if additionally the initial todo is a subset of the powerset of the state set of the automaton and the initial result_-sets are empty, as in this case each recursive step must insert some new element into result_states while this set is also a subset of the (finite) powerset of states of the automaton.

Consider then the following function f that uses f_helper, where functions transitions and initial respectively extract the finite set of transitions and the initial state of automaton a:

fun f :: "('a,'b) automaton ⇒ 'a set set × ('a set × 'b × 'a set) set" where 
  "f a = f_helper (transitions a) {{initial a}} {} {}"

I would like to be able to generate code for f even though I cannot prove termination of f_helper in the general case but only for certain assumptions on the parameters (which are satisfied in f). I know that I could probably ensure the assumptions by checks in f_helper, but I believe that this would lead to very inefficient code.

Is there a way to define the recursive function f_helper only within the context of f to avoid having to prove termination of f_helper for inputs that are not relevant (infinite sets etc.)?

Answer 1

Since your function f_helper is tail-recursive, you should be able to define f f_helper via partial_function as follows:

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

Then afterwards f_helper should be amenable for code-generation.

Best, René