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
Ewhere (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.(
X)(
Y) a(Y,t) = a(Y,t') ,
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
Tit is sufficient to prove that T is attribute coherent and that(
X)t = t' ,
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.