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

Now for the main definition: A theory T is
**attribute coherent** iff for any method f: v1...vj
h1...hk -> 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