-- typeConsistencyOfStoreValues.tioga
-- Spreitze, May 9, 1991 1:55 pm PDT
We take a very simple model.
There is a set of variables, V. There is a configuration, G: V b U, where U is the set of values. V † U.
We have one operation: Store value u1 into variable v2. This is successful only if v2  V. When it is successful, it produces a new configuration G`, where G` is defined by:
if v ` v2 then G`(v) = G(v).
if v = v2 then G`(v) = u1.
We have a set of types, T. We have a typing, an assignment of types to the variables, : V b T. For the moment, we assume that the typing is fixed.
The types really belong to an algebra. This algebra has (for the moment) two unary operations: load and store. That is, for some types t in T, t.load and t.store are defined and also in T.
Given a typing, , and a type, t, we have a set of values: D(t) † U.
We say that a configuration G is consistent with a typing  if and only if
for all v in V, G(v)  D((v)).
Now, we restrict Store to also require:
Storing u1 into v2 is legal for typing  only if
u1  D((v2))
Now, we attempt to prove that: if G is consistent with a typing , Storing u1 into v2 is legal for typing , and Storing u1 into v2 succeeds for G, producing G`, then G` is consistent with .
We must prove that G`(v)  D((v)), for all v in V.
if v ` v2, then G`(v) = G(v), and the conclusion follows from the assumption that G is consistent with .
if v = v2, then G`(v) = u1  D((v2)) = D((v)).
Now go one step indirect (which a compiler must do, since it doesn't have runtime values in its hands), and introduce the operation: Store from v1 through v2, for v1 and v2 in V, which means to store the value G(v1) into the variable G(v2). This is successful only if G(v2)  V. When it is successful, it produces a new configuration G`, where G` is defined by:
if v ` G(v2) then G`(v) = G(v).
if v = G(v2) then G`(v) = G(v1).
Store from v1 through v2 is legal exactly when storing u1 into v3 is legal for every u1  D((v1)) and v3  D((v2)), and when it's legal it produces a G` that is consistent with .
What do we need to know in order to prove that storing u1 into v3 is legal for every u1  D((v1)) and v3  D((v2))? Let's try these hypotheses:
H1: for v  V, if v  D(t), then D(t.store) † D((v)) † D(t.load) .
H2: D((v1)) † D((v2).store) .
We must prove that u1  D((v3)).
(1): u1  D((v1))
given;
(2): D((v1)) † D((v2).store)
by H2;
(3): v3  D((v2))
given;
(4): D((v2).store) † D((v3))
by H1 and (3);
(5): u1  D((v3))
by (1), (2), and (4).
H2 must be checked when compiling as assignment expression. H1 is taken to be part of the language definition.
When might D(t.store) actually differ from D((v)) in H1? For example, when t is the union type (VAR t1) * (VAR t2). In this case, v will be a t1 variable or a t2 variable; D((v)) will either be D(t1) or D(t2). To guarantee that D(t.store) † D((v)) for every v  D(t), D(t.store) must be contained in D(t1) ) D(t2) --- which could be smaller than either or both of D(t1) or D(t2).
When might D(t.load) actually differ from D((v)) in H1? I don't know. Note that the relation between D(t.load) and D((v)) in H1 is never utilized in the above proof.