[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 15 Jun 2019, at 11:46, Thomas Streicher <[email protected]<mailto:[email protected]>> 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
