Attribute Coinduction and Coherence
Recall that coinduction is a powerful technique for proving behavioral equalities of terms. Attribute coinduction is a special case of coinduction that has two major advantages: (1) it can be applied essentially automatically; and (2) it works for operations that have more than one hidden argument. On the other hand, this proof rule can only be applied in the very special case of attribute coherent theories. To help define that important property, we first give an auxiliary definition:

Given a hidden theory T=(,E) where is a hidden signature and E is a set of -equations, we say that two -terms t,t' of hidden sort h over a variable set X are attribute equal iff for all attributes a(Y,S) where S has sort h and Y is some variables, we have

   E  (X)(Y) a(Y,t) = a(Y,t') ,
where (as is usual) we call the hidden sort valued operations methods and the visible sort valued operations attributes. Let us write attribute equality as t =A= t'; this just means that t,t' have exactly the same attribute values. Although in general this is far short of behavioral equivalence, it can still be a useful relation on terms.

Now for the main definition: A theory T is attribute coherent iff for any method f: v1...vj -> h in with k > 0, if S1,...,Sk and S'1,...,S'k are new variables of sorts h1,...,hk, and if T' is T with the addition of the assertions Si =A= S'i for i=1,...,k, then we have

   T' implies f(Z,S1,...Sk) =A= f(Z,S'1,...,S'k) ,
where Z is a set of new variables of sorts v1,...,vj. Let's denote the assertion that T is attribute coherent by ACoh(T). The definition of coherence above can be considered a proof rule for establishing the goal ACoh(T).

Now we are in position to state the attribute coinduction proof rule. To prove

   T  (X)t = t' ,
it is sufficient to prove that T is attribute coherent and that
   T implies  t =A= t' . 
The connection of this to the full coinduction proof rule is that =A= is just a particularly simple candidate relation on terms, and showing a theory attribute coherent shows that attribute equality is behavioral equivalence.
[Prev] [Home] [BHome]
12 March 1998