# 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.