Search code examples
isabelle

Could not find lexicographic termination order

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"
fun LTS_is_reachable :: "('q, 'a) LTS  \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool" where
   "LTS_is_reachable \<Delta> q [] q' = (q = q')"|
   "LTS_is_reachable \<Delta> q (a # w) q' = 
      (\<exists>q''. (if (q,{},q'') \<in> \<Delta> then LTS_is_reachable \<Delta> q'' (a # w) q' else (\<exists> \<sigma>. (a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q'))))"

Here, I just want to define a transition labeled system which take a triple set, a initial state, a list and a final state. The funtion LTS_is_reachable is to check whether there exists a path start from initial state to final state. The element in triple set can be (q,{a,b},p) which means that if we can get a or b, the state a will be transformed into state b. Also (q,{},p) means that we don't need any to do that, the state a will be transformed into state b automatically. My problem lies on how to define the later transformation. That sounds hard for me.

The difinition above in Isabelle warns that Could not find lexicographic termination order. Any help will be appreciated.

Solution

  • To define a recursive function, it must be terminating. And the error you get means that Isabelle is not able to prove automatically that your function is terminating.

    And indeed, LTS_is_reachable \<Delta> q (a # w) q' calls LTS_is_reachable \<Delta> q'' (a # w) q'. Actually it is not clear (both to Isabelle and to me) that this would be terminating.

    In general there are several solutions in such cases:

    • the function does terminate by Isabelle cannot find it automatically. See the function documentation.

    • it does not terminate, but you do not need the function to be executable. You can use inductive predicates.

    • it does not terminate, but you need the function to be executable. You can use the notion of fuel: You run up-to fuel steps. Then if you set your fuel high enough, everything will go through. This is rarely the best approach, but is sometimes required.

    In your case the inductive predicate sounds like a good approach.