Makoto Takeyama and I sent the following to data-refinement@etl.go.jp on Jan 5, 1996:
Subject: what is a data refinement relation?
Dear all: anyone still interested in data refinement?
Recently Mak and I have been looking again at an idea we considered
many months ago. The motivation is to characterize
the logical relations relevant to showing data refinement.
This was stimulated by the realization that logical relations can
be used to show "safety" of abstract interpretations
(see Section 2.8 of the chapter by Jones and Nielson in
volume 4 of the Handbook of Logic in CS), but such relations
are more general than those used to show data refinement.
My reasoning goes as follows. If a relation R is establishing a data
refinement between (among) sets, then it must be inducing
(partial) equivalence relations on each of the sets, with
these equivalence classes in one-to-one correspondence,
and every element of an equivalence class must be related
to all elements of the corresponding equivalence classes in
the other domains of interpretation. The idea is that each
equivalence class represents an "abstract" value; in a fully
abstract interpretation the equivalence classes are singletons.
We can give a simple condition to ensure that an n-ary relation R induces
this structure. Define v ~ v' in domain V iff there exists a value
x in some other domain X (and arbitrary values ... in the
other domains) such that R(...,v,...,x,...) and R(...,v',...,x,...).
This defines symmetric relations on each of the domains. Imposing
local transitivity would then give us pers on each domain, but
this would not suffice because we want to ensure transitivity
across interpretations. The following condition achieves this:
if v_i ~ v'_i for all i, then R(...,v_i,...) iff R(...,v'_i,...)
I call this "zig-zag completeness"; in the case n=2, it says
that if R(a,c) & R(a',c') then R(a,c') iff R(a',c).
Proposition. If R and S are zig-zag complete relations, so
are R x S and R -> S.
Proposition. Suppose t and t' are terms of type th in context pi,
and R is a zig-zag complete logical relation;
then, if the equivalence judgement t=t' is interpreted as follows:
for all u_i in V_i[[pi]],
R^{pi}(...,u_i,...) implies that, for all i, V_i[[t]]u_i ~ V_i[[t']]u_i
this interpretation satisfies the usual axioms and rules
for equational logic.
The intuition here is that the terms are to be "equivalent" both
within a single interpretation (V_i) and across interepretations;
i.e., the meanings of t and t' are in the same R-induced
equivalence class, no matter which interpretation is used.
Questions:
Has anyone seen this kind of structure before?
What are the natural generalizations of these ideas to
other propositions and "arbitrary" semantic categories?
Bob Tennent
rdt@cs.queensu.ca
