Could not find lexicographic termination order

user_13276122 0
Viewed 54
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.

isabelle
2 Answers

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.

user_128242070

This concept should definitely be formalised as an inductive predicate. Then you'd have tools for proving instances of LTS_is_reachable and conversely to prove facts by induction, given an assumption involving LTS_is_reachable.

And no need to prove termination.

user_31366860
Related