Notes. Coinduction in what sense? In this paper,
in the thesis above, and in our RTSS '04 paper, we have categorized
our inductive proof method as coinductive and the induction
that we used to be coinduction. Our proof method is coinduction
in the sense that a path in the proof tree ends when we encounter a
cycle. When our proof method concludes a proof, it is because the
proof tree is regular, that is, there is no infinite path with
unique assertion at each node (such that it is rational, which
means that it has a finite representation). This is typical of
coinduction proof.
For the discussion below, a useful reference would be Park's 1969
paper Fixpoint induction and proof of program properties, which
appeared in Machine Intelligence 5, Edinburgh University Press, 1969.
Typically, a coinduction/greatest fixpoint-based proof is used to
prove that A is included in B by restricting B into B' (= T^-1(B) for
the given monotonic operator T --- since T is monotonic, necessarily
B' => B, and T^-1 is also monotonic), until a fixpoint is reached, and
demonstrate that A is undeniably in the fixpoint. That is,
(A => T(B')) => (A => B')
-------------------------
A => gfp(T)
This can be derived from the simpler form of greatest (maximal) fixpoint
induction which can be inferred from Park's article mentioned above,
as follows:
B => T^-1(B)
-------------
B => gfp(T)
On an assertion A (of the form G |= H), we apply any of our proof
rules resulting in a set of assertions. For example, using the left
unfold LU rule we obtain a set of assertions, each is the
result of unfold using a particular CLP clause. This set represents a
conjunction of these assertions. Using the right unfold RU
rule, we obtain a set containing a single new obligation that replaces
the original. Using all applicable rules other than AP we
obtain a disjunction of conjunctions of assertions. Each of the
disjunct implies the original assertion A, and hence the disjunction
implies the original assertion A.
Therefore the parallel application our proof rules represents a
monotonic operator c* (T^-1 in the above), and its inverse monotonic
operator c (T in the above).
Our proof method advocates a search strategy to find "inconsistency."
Formally, an assertion A is inconsistent, iff, given a program
P, lm(P) does not imply A. Our proof method establishes lm(P) => A by
coinduction. First, we transform A into a number of conjunctions
assertions S1 ... Sn. Now since our proof rules (without AP)
represent a monotonic operator, maximal fixpoint induction (a.k.a.
coinduction applies).
With the application of AP rule, we establish
(lm(P) => A) => (lm(P) => (S1 \/ ... \/ Sn))
That is, assuming G |= H "holds" (formally, lm(P) => (G |= H)),
we prove that its descendants also hold, and by maximal fixpoint
induction rule we can therefore establish that
lm(P) => gfp(c).
Note that this discussion by no means establishes the soundness of our
proof method. First, it simply says that concluding a proof using our
proof method is equivalent to an inability to find inconsistency.
Second, it also demonstrates the "coinductive" view of our proof
method. For the soundness proof, page visitors may refer to the thesis
above.
Look at the picture to the left, which illustrates a hypothetical
search tree. The search is done in depth-first manner left-to-right.
The horizontal arrows represent potential subsumption of nodes in
the search tree, where both the graph vertices are the same, and
the resource consumption of the potentially subsumed node implies
the resource consumption of the potentially subsuming node.