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

[O'Hearn, Peter]

On 15 Jun 2019, at 11:46, Thomas Streicher <streicher at mathematik.tu-darmstadt.de<mailto:streicher at mathematik.tu-darmstadt.de>> wrote:

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.

Thomas, this was precisely what I meant. Termination is not “admissible for fixed-point induction”. And other techniques (e.g., based on ranking functions) are commonly used to prove termination.

The only thing that gives me pause is the existence of proof theories for temporal/modal formalisms (e.g., mu-calculus) that are based on Park induciton and which are complete, and yet
the formalisms can express liveness properties too. Possibly games are being played with greatest FP’s, or perhaps they cannot actually prove the kinds of properties one would want in order to show the termination argument in Hoare Logic for total correctness. I am not sure.

But thanks for your answer.

Peter