[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I think, if I’m interpreting your question correctly, that your intuition is correct. Park’s upper fixpoint induction principle that you state allows you to prove upper bounds on lfp(F), which I interpret as safety properties, whereas I interpret liveness properties as lower bounds on lfp(F). Looking at the paper on the modal mu-calculus, I would think that the liveness properties arise not from the Park induction rule schema, but rather the pre-fixpoint axiom schema, which says (reinterpreting in your syntax the first equation on page 4): F(lfp(F)) <= lfp(F) It is this axiom schema that allows one to prove lower bounds on lfp(F), which I interpret as liveness properties. Very informally, I believe that a loop variant ought to correspond to the number of times the above axiom must be applied. (But I’m not entirely confident about this!) Ben > On Jun 14, 2019, at 11:23 AM, O'Hearn, Peter <[email protected]> wrote: > > [ 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 > > > > > > > > > > > >
