[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 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
