Termination problem

How to proof a program will stop and give us an answer? This big question leads halting problem, but not the end. Even though we cannot get a result for arbitrary program, get this information for certain kind of program might still useful. However, even this simpler question is still hard. For example, the following program will stop(roughly speak).

for (int a=0; a<10; a++) {
}

What if we add a printf statement as loop body? The answer is subtle, it depends on how do we use printf, because printf in fact is a turing machine. In real life, as a creator of analysis tool, we might say let's ignore weird usage. Hence, the printf terminated, and we back to the loop structure. We know the above terminated, but how do we know? Because stop condition is bigger than initial value when a get increased. To inference on these condition, one must know how to extract information from program. There have many ways to represent a program, here I will assume just a proper abstract syntax tree and related tools existed. Then getting the information is simple:

for (int a = <init>; a < <stop>; a++)

Our checker can be like

(define (ok? init stop)
  (<= init stop))

What!? That simple? Yes, that simple, and useless. The code is useless because there has more form of loop. For example, control variable can get decreased.

for (int a = <init>; a > <stop>; a--)

To handle this also, the checker turns to

(define (ok? init stop step)
  (case step
   [(--) (>= init stop)]
   [(++) (<= init stop)]
   [else #f]))

1. Recursion

Even the step mode have infinite pattern, however. Which means this way has infinite thing to do. The point is recursion is isomorphic to iteration, hence, we rewrite program as the following.

let rec loop : int -> unit =
  fun a ->
  match a with
  | 0 -> ()
  | n -> loop (n - 1)

2. Inductive

To prove such program stop, is still hard, finding base case and induction case need manual work. We need something to restrict the possible input. For numberic, we can write:

type nat =
  | zero
  | suc nat

With type nat, the recursion be rewrote to:

let rec loop : nat -> unit =
  fun a ->
  match a with
  | zero -> ()
  | suc (n) -> loop n

The definition like type this kind, called inductive family. Turns out, we can see it's a lattice. Hence, termination problem is finding a process corresponding to a lattice, and inductive family is just a limited, full connected version. Anyway, now proving termination is finding every recursive point is an induction case, suc (n) to loop n so it's smaller on recursion then it's induction.