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

[Ben Sherman]

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 <p.ohearn at ucl.ac.uk> 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
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
>