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

[O'Hearn, Peter]

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