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

[Sergey Goncharov]

Dear Peter,

my understanding of the discrepancy you mention is like this. The 
expressive power of mu-calculus comes from Park induction *plus* 
negation. Since negation is in the language, we can dualize all the 
properties we can specify, in particular, define greatest fixpoints 
dually to the least ones, for which the dual Park rule

      gfp(F) => S  iff    Exists I. FI => I & I => S

is derivable. This allows us to deal with safety since safety is dual to 
liveness (and liveness in mu-calculus is expressed via least fixpoints). 
Moreover, we can combine two kinds of fixpoints to express properties 
like fairness.

Now, when it comes to the comparison between Hoare logic and 
mu-calculus, one has to be careful, because Hoare logic is exogenous 
(programs are explicit) and mu-calculus is endogenous (the underlying 
model represents the program of interest). Connecting Hoare logic with 
mu-calculus can be done via a calculus of weakest preconditions. This 
involves some curious dualization, because if we compute the semantics 
of a while-loop as a least fixpoint then the corresponding precondition 
involves a greatest fixpoint.

So, connecting mu-calculus and Hoare logic introduces some confusion of 
fixpoints, but it does not change the fact that in mu-calculus we can 
freely use both kinds of fixpoints arbitrarily, while
in Hoare logic we essentially have a global choice between weakest 
preconditions for total correctness and weakest (liberal) preconditions 
for partial correctness. Computationally the former are completely 
different kind of properties (co-r.e.) in comparison to the latter 
(r.e.) in the arithmetical hierarchy.

I understand that the fact that mu-calculus is complete is essentially 
because it is complete wrt to a totality of over-abstracted programs, 
and so it is not affected by the above decidability issues. But in Hoare 
logic we deal with concrete programs for which the problem of checking 
partial correctness and the problem of checking total correctness are 
entirely asymmetric.

In summary, I think your slogan "fixpoint induction is not good for 
termination” is correct because termination is not an inductive property 
and there is no conflict with the completeness of mu-calculus.

Best,
Sergey


On 14/06/2019 16:23, O'Hearn, Peter 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
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 

-- 
PD Dr. Sergey Goncharov, Akademischer Oberrat

FAU Erlangen-Nürnberg         Phone: +49-91-3185-64031
Chair for TCS                 Fax:   +49-91-3185-64055
Martenstraße 3                Email: Sergey.Goncharov at cs.fau.de
D-91058 Erlangen              Web:   http://www8.cs.fau.de/~sergey