[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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: [email protected]
D-91058 Erlangen Web: http://www8.cs.fau.de/~sergey
