Type 1 functions

Call a function type 1, if and only if it satisfies all of the following conditions:

We characterize this type because noting specific properties allows us to consider functions which don't have all of these properties. After developing an argument for why type 1 functions always terminate, we can go looking for functions that aren't type 1.


Here's an example of a type 1 function which obviously terminates, but not by a lexicographic ordering argument.

$$f(x) = \begin{cases} 0 & \text{if }x\text{ is even} \\ f(x + 1) & \text{if }x\text{ is odd} \end{cases}$$

Informally, when \(f\) is given an even number, go straight to 0. If given an odd number, go to the next even number, then to 0. From this, it's obvious that there are no paths of length greater than 2. Thus, our measure function should spit out only 0 or 1.

When \(x\) is even, \(f(x)\) terminates immediately, and so our measure is 0. When \(x\) is odd, \(f(x)\) does not terminate immediately, it takes another step before terminating. Thus, our measure for odd \(x\) is \(1.\) Here is our measure function \(g.\)

$$g(x) = \begin{cases} 0 & \text{if }x\text{ is even} \\ 1 & \text{if }x\text{ is odd} \end{cases}$$
theory Scratch imports Main begin

function f :: "nat ⇒ nat" where
"f x = (
	if even x then 0
	else f (x + 1)
)"
apply auto
done

fun g :: "nat ⇒ nat" where
"g x = (
  if even x then 0 
	else 1
)"

termination f
apply (relation "measure (λx. g x)")
apply simp
apply (simp_all only: in_measure)
apply auto
done

end