Type 2 functions
Call a function type 2, if and only if it satisfies all of the following conditions:
- Not amenable to lexicographic ordering
- Exactly one termination path, of infinite length
- Call graph is permutation on the natural numbers
Here's an example of a type 2 function
$$f(x) = \begin{cases} 0 & \text{if }x = 0 \\ f(x - 3) & \text{if }x\text{ is even} \\ f(x + 1) & \text{if }x\text{ is odd} \end{cases}$$Here's the call graph for \(f:\)
Notice that the call graph is one infinitely long path. Further, this path is a sort of permutation of the sequence of natural numbers. Because it's a permutation, we can use another permutation as the measure function.
$$g(x) = \begin{cases} x - 1 & \text{if }x\text{ is even} \\ x + 1 & \text{if }x\text{ is odd} \end{cases}$$This measure function essentially takes the argument \(x\) and returns its position in the call graph as a natural number. In other words, it undoes the permutation displayed by the call graph.
Now let's generalize. A permutation is always a bijection, and a type 2 function has a permutation in its call graph, by definition. Thus, there will always be a measure function \(g,\) that undoes the permutation on the call graph of \(f.\) Thus, all type 2 functions must be total.
theory Scratch imports Main begin function f :: "nat ⇒ nat" where "f x = ( if x = 0 then 0 else if even x then f (x - 3) else f (x + 1) )" apply auto done fun g :: "nat ⇒ nat" where "g x = ( if x = 0 then 0 else if even x then x - 1 else x + 1 )" termination f apply (relation "measure (λx. g x)") apply simp apply (simp_all only: in_measure) apply auto done end