[TYPES] Variants and [Park or Scott] fixpoint Induction

[Thomas Streicher]

> Two methods of reasoning about loops are provided by variants and by (Park or Scott) fixpoint induction. Is there a known relation or non-relation between them? My intuition is that fixpoint induction is not suitable for termination or liveness properties, but I am unsure whether this intuition is correct.

For fixpoint (i.e. Scott) induction you have to assume that the predicate
under consideration contains bottom and is closed under sups of increasing
chains. Since it contains bottom such a predicate can't express any
kind of termination property.

Termination properties of programs P = fix(Phi) are usually proved by
induction over data types from P = Phi(P), i.e. the defining equation
for P.

Park induction also only allows one to prove that mu(Phi) is contained
in some f \geq Phi(f), i.e. also can prove only downward closed
properties.

That explains why logic of programs which are not of domain-theoretic
kind, i.e. don't allow one to express infomation ordering, are
successful for proving total correctness properties.

But I think that proving negative properties like nontermination is
also very important and for this reason domain theory is very important.

Thomas