We prove, in the context of simple type theory, that logical
relations are sound and complete for data abstraction
as given by equational specifications. Specifically, we show
that two implementations of an equationally specified
abstract type are equivalent if and only if they are linked
by a suitable logical relation. This allows us to introduce
new types and operations of any order on those types, and to
impose equations between terms of any order. Implementations
are required to respect these equations up to a general
form of contextual equivalence, and two implementations
are equivalent if they produce the same contextual equivalence
on terms of the enlarged language. Logical relations are
introduced abstractly, soundness is almost automatic, but
completeness is more difficult, achieved using a variant of
Jung and Tiuryn's logical relations of varying arity. This
also relates to lax, equivalently, pre-logical relations.
The results are expressed and proved categorically.
