 # 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