Coinduction
Coinduction is a powerful technique for proving behavioral properties of (systems of concurrent interacting) objects. It generalizes the notion of bisimulation introduced by David Park in late 70's for labeled transition systems, a proof technique for a semantic notion introduced earlier by Robin Milner. Here we formulate coinduction as a proof rule.

Technically, coinduction is used to show that an equation is behaviorally satisfied by (all models of) some hidden specification. Thus if E is a set of hidden -equations, our proof goal has the form 

   E (X) t1 = t2,
where X is some set of variables with their types, and t1, t2 are terms of (the same) hidden sort.

A coinductive proof of this goal must provide the following:

  1. A relation R defined on -terms with variables from X, called the candidate relation.
  2. A signature , whose elements are called generators.
  3. A signature , whose elements are called selectors.
To complete this coinduction proof, we must show the following:
  1. R is a hidden -congruence;
  2. R is a hidden -congruence; and
  3. t1 R t2;
where a hidden congruence is a relation that is the identity of the visible sorts and preserves the operations in its signatue. Of course, we will try to do these steps by reduction with OBJ. The following should be noted:
  1. + + must be a decomposition of .
  2. Any elements of and that are derived within their own signature can be omitted (this notion is defined, and the result is proved in "A Hidden Agenda").
  3. The candidate relation only needs to be defined on hidden sorts, because in any case it must be the identity on visible sorts (this is implied by 1.).
  4. There is a common default choice, where consists of the methods in , where contains the attributes in , and where two terms are R-related iff all their attributes are equal. If this default choice is taken, then condition above is automatically satisfied, and in fact R is behavioral -equivalence.
  5. If the equations satisfy a certain property (called "hidden completeness" -- see "A Hidden Agenda") then 2 property. is also automatically satisfied. It is sufficient for each equation to be of the form a(m(x)) = t(x), with m a method, a an attribute and t a term involving no methods.
As the name suggests, coinduction is dual to induction. Some category theory is needed to express the duality involved (between initial and final objects); see "A Hidden Agenda" for details.
[Next] [Prev] [Home] [BHome]
23 November 1996