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