[ 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. The Hoare rule for total correctness of while loops using variants is well explained in the wikipedia article: https://en.wikipedia.org/wiki/Hoare_logic#While_rule_for_total_correctness There, you make sure a quantity in a well-founded set decreases on each loop iteration. Here is Park induction: lfp(F) <= S iff Exists I. FI <= I & I <= S If you think of S as “spec” and I as “invariant”, then this can form the basis for reasoning about safety properties (as explained by Cousot here) http://web.mit.edu/16.399/www/lecture_11-b-fixpoints1/Cousot_MIT_2005_Course_11b_4-1.pdf I am a bit worried that my intuition "fixpoint induction is not good for termination” might have some holes in it. In particular, Park induction is used in a known complete proof theory for modal mu-calculus https://eprints.illc.uva.nl/569/1/PP-2016-33.text.pdf and that logic is notable for being able to express liveness properties. I asked a few experts who did not know a way to answer my question above, which is why I am posting it more widely here. In particular, if there is an explanation of how/why fixpoint induciton could be good for reasoning about (say) liveness or termination properties of while loops, I’f be glad to hear about it. Thanks! Peter O'Hearn
