Reasoning about Explicit and Implicit Representations of State

Amr Sabry^{∗}  John Field
Rice University  IBM T.J. Watson Research Center

        sabry@cs.rice.edu            jfield@watson.ibm.com

Abstract

The semantics of imperative languages are often expressed in terms of a store-passing translation and an algebra for reasoning about stores. We axiomatize the semantics of several typical imperative languages via equational axioms by “inverting” the storepassing translation as well as the algebraic axioms for reasoning about the store. The inversion process is simple and systematic and results in theories that are similar to equational theories for imperative languages that have been derived in more complicated ways, and is likely to be applicable to languages other than those presented here.

1 A Semantic Toolkit for Imperative Languages

The mathematical semantics of imperative languages conventionally regards the store as a primitive concept [16:p. 203]. Using a “store-passing transformation”, imperative operations are translated to explicit operations on a concrete representation of the store in an augmented lambda-calculus. The resulting store constructs typically have a simple semantics that is easy to reason about. Furthermore, such a store and its related operations can yield a natural “store algebra” that can be used for optimization purposes [9].

Since it is often the case that one wishes to reason about languages directly rather than by translation, there have been many proposals for logics for imperative languages [2, 4, 6, 7, 8, 10, 11, 17]. Although each of these was designed independently, and differs from the others in subtle ways, the similarities between them suggest the existence of a systematic way to derive equational logics from the semantics of the languages.

We propose to construct logics for imperative languages by deriving an inverse to the store-passing transformation and applying it to the equational axioms of the enriched lambda-calculus. We explain the general strategy in detail in Section 2. In later sections, we demonstrate the feasibility of our technique by applying it to a variety of imperative languages that are extensions of the call-by-value λ-calculus. The first language includes an infinite set of locations, facilities to assign values to these locations, and the ability to pass them to procedures. The second language extends the first with facilities to perform dynamic allocation and de-allocation. The last language has a lazy store update operation in addition to the conventional strict operation. Although the axioms of the derived equational logics simulate the effect of “passing the store”, they represent local transformations on the original programs, and do not rely on the concept of a centralized global store.

∗Supported in part by NSF grants CCR 89-17022 and CCR 91-22518 and Texas ATP grant 91-003604014.

Our derived logics are more complex than the store-augmented lambda-calculus, reflecting the intricacies of modeling the sequencing of imperative operations. By using the original store-passing transformation as the basis for deriving these logics, they may be obtained more readily than attempting to construct them ab initio. We believe this approach is likely to be particularly beneficial for developing logics for languages not designed with equational reasoning in mind.

2 Manufacturing Equational Logics

In this section, we outline the general strategy we will use to axiomatize the semantics of our imperative languages. Let R be the source language whose semantics we wish to axiomatize. The first step is to define a target language G with explicit store manipulation constructs and to axiomatize its semantics using an equational theory ax(G). Fortunately, the derivation of the latter equational theory is usually much simpler than the derivation of a corresponding equational theory for the source language because of the explicit representation of the store.

The semantics of the source language is then defined using a (store-passing) translation f : R → G, which can be used to reason (indirectly) about R-terms using ax(G). Our goal is to derive a set of axioms ax(R) with the following property. For all r_{1}, r_{2} ∈ R,

ax(R) ⊢ r_{1} = r_{2}  if and only if  ax(G) ⊢ f(r_{1}) = f(r_{2}).

To derive the axioms ax(R), we develop an inverse translation: f^{−1} : G → R, and axioms A_{0}^{R} such that for all r ∈ R:

A_{0}^{R} ⊢ r = (f^{−1} ∘ f)(r).

The inverse translation f^{−1} must be compositional, i.e., for all contexts C and terms g in G,

f^{−1}(C[g]) = f^{−1}(C[x]) [x := f^{−1}(g)] ,

where x does not occur in C. The compositional nature of f^{−1} ensures that the equations resulting from the inversion process are valid in any context as required by equational logics in general. Naturally, the axioms A_{0}^{R} must be sound with respect to the translation f and ax(G):

A_{0}^{R} ⊢ r_{1} = r_{2} implies ax(G) ⊢ f(r_{1}) = f(r_{2}).

Next, for each equation E_{i}^{G} ∈ ax(G) such that: E_{i}^{G} =^{df} (g_{1} = g_{2}), find a set of equational axioms E_{i}^{R} such that:

E_{i}^{R} ⊢ f^{−1}(g_{1}) = f^{−1}(g_{2}).

If E_{i}^{G} is a simple first order equation, then we can define E_{i}^{R} as { f^{−1}(g_{1}) = f^{−1}(g_{2}) }.

The full equational theory for R then consists of the axioms ax(R) defined by:

ax(R) =^{df} A_{0}^{R} ∪ ⋃_{i} E_{i}^{R}.

It is straightforward to show that the set ax(R) proves all the equations that are provable in the target language. In other words, the development results in a complete equational correspondence between the theories for the source and target languages.

This technique is not specific to logics of imperative languages, and is similar to the method used to establish the correspondence between the λ-calculus and combinatory logic [1, 5], and the correspondence between the computational λ-calculus [13] for callby-value languages and the λ-calculus for continuation-passing terms [15].

3 Strict Assignments, Call-by-Reference

We begin by considering a pure functional language R_{1} extended with simple imperative facilities. The functional subset includes values V and applications (M N). The set of values includes the natural numbers , variables, procedures, and a “unit” constant ‘()’ denoting an unspecified value. The language also includes an infinite set of constants A representing locations. Locations may be passed as arguments and may be assigned to using setref!. The contents of a location is accessed using the operation deref. Although this language is quite simple, it is sufficient to represent, e.g., pointer manipulations and call-by-reference parameter passing, since addresses are computable “first-class” values. The syntax of R_{1} is as follows:

Definition 3.1. (R_{1})

M ::= V | (M N)  (Terms)
V ::=  | X | A | () | (λx.M) | deref | setref!  (Values)
X ∈ Variables = {x, y, z, …}
A ∈ Locations = {a_{1}, a_{2}, …}

In order to define the semantics of the language R_{1}, we introduce the language G_{1} that includes simple primitives for manipulating the store. All constructs in G_{1} manipulate the store explicitly; in particular, the evaluation of a G_{1}-program produces a pair that consists of a value and a store. The syntax of G_{1} is defined as follows:

Definition 3.2. (G_{1})

P ::= ⟨W, S⟩ | (W P) | S@W  (Terms)
W ::= | X | A | ? | (λ⟨x, s⟩.P) (Values)
S ::= s | (upd S W W)  (Stores)

The notation ⟨W, S⟩ denotes a pair whose first element is the value W and second element is the store S. The constant ‘?’ refers to an unspecified value. The variable s denotes an unknown store and the term (upd S W_{1} W_{2}) represents a store S whose most recent assignment associates expression W_{2} with address W_{1}. Such a store may contain more than one assignment for any given address. The lookup operation S@W_{1} returns a pair ⟨W_{2}, S⟩ where W_{2} is the rightmost, or most recent assignment, to location W_{1} in the store S. A G_{1}-program is a closed term ((λs.P) {}) where {} is the “initial” empty store.

Given the above informal explanation, we present three axioms that suffice for the evaluation of G_{1}-programs:

Definition 3.3. (ax(G_{1}))

((λ⟨x, s⟩.P) ⟨W, S⟩) = P [x := W, s := S]  (Q_{1} = β_{v}^{×})
(upd S A W)@A = ⟨W, (upd S A W)⟩  (Q_{2})
(upd S A_{1} W)@A = ((λ⟨x, s⟩.⟨x, (upd s A_{1} W)⟩) S@A) A_{1} ≠ A  (Q_{3})

Axioms Q_{1} and Q_{2} are straightforward and should be self-explanatory. Axiom Q_{3} ensures that store components not containing the looked-up address are preserved.

The semantics of the source language R_{1} is defined indirectly by the axioms ax(G_{1}), using the following store-passing translation:

Definition 3.4. (Store-Passing Transformation)

S : R_{1} × S → G_{1}
S[[V]]s = ⟨W[[V]], s⟩
S[[(M N)]]s = ((λ⟨x, s⟩.(x S[[N]]s)) S[[M]]s)
W[[n]] = n
W[[x]] = x
W[[()]] = ?
W[[(λx.M)]] = (λ⟨x, s⟩.S[[M]]s)
W[[A]] = A
W[[deref]] = (λ⟨x, s⟩.s@x)
W[[setref!]] = (λ⟨x, s⟩.⟨(λ⟨y, s′⟩.⟨?, (upd s′ x y)⟩), s⟩)

In the remainder of the section, we will systematically develop an equational theory ax(R_{1}) for R_{1}. The derived theory will have the property that any equivalence provable indirectly via ax(G_{1}) is also provable directly in ax(R_{1}). In this sense, ax(R_{1}) will be complete relative to ax(G_{1}).

3.1 Inverting the Store-Passing Transformation

The specification of an inverse to the store-passing translation relies on the representation of stores in the source language R_{1}. We choose the following common representation [2, 12, 14]. A store of the form:

(upd (upd … (upd (upd s W_{11} W_{12}) W_{21} W_{22}) …) W_{n1} W_{n2})

will be represented in the source language as the sequence of assignments:

() ; (setref! V_{11} V_{12}) ; (setref! V_{21} V_{22}) ; …; (setref! V_{n1} V_{n2}),

where V_{ij} corresponds to W_{ij} and the sequencing operation (M ; N) is an abbreviation for: ((λd.N) M), where d is not free in N.

The following inverse store-passing transformation defines inverses for arbitrary terms of G_{1}, and formalizes the store’s representation:

Definition 3.5. (Inverse Store-Passing)

S^{−1} : G_{1} → R_{1}
S^{−1}[[⟨W, S⟩]] = I[[S]] ; W^{−1}[[W]]
S^{−1}[[(W P)]] = (W^{−1}[[W]] S^{−1}[[P]])
S^{−1}[[S@W]] = I[[S]] ; (deref W^{−1}[[W]])
W^{−1}[[n]] = n
W^{−1}[[x]] = x
W^{−1}[[?]] = ()
W^{−1}[[(λ⟨x, s⟩.P)]] = (λx.S^{−1}[[P]])
W^{−1}[[A]] = A
I[[s]] = ()
I[[(upd S W_{1} W_{2})]] = I[[S]] ; (setref! W^{−1}[[W_{1}]] W^{−1}[[W_{2}]])

The relationship between the store-passing transformation and its inverse requires the following axioms:

Definition 3.6. (A_{0}^{R_{1}})

((λx.M) V) = M[x := V]  (I_{1} = β_{v})
deref = (λx.(deref x))  (I_{2} = η_{v}^{d})
setref! = (λx.λy.((setref! x y) ; ?))  (I_{3} = η_{v}^{s})
(V ((setref! V_{1} V_{2}) ; M)) = (setref! V_{1} V_{2}) ; (V M)  (I_{4})
(M N) = ((λx.(x N)) M)  (I_{5})

We now prove a tight relationship between the original store-passing transformation and its inverse, using the axioms A_{0}^{R_{1}}:

Lemma 3.7 Let M ∈ R_{1} and S be a store in G_{1}. Then

A_{0}^{R_{1}} ⊢ (I[[S]] ; M) = S^{−1}[[S[[M]]S]]

Proof. The proof is by induction on the structure of M and proceeds by cases:

• M = V, then S^{−1}[[S[[V]]S]] = S^{−1}[[⟨W[[V]], S⟩]] = (I[[S]] ; W^{−1}[[W[[V]]]]). It remains to

show that:

A_{0}^{R_{1}} ⊢ W^{−1}[[W[[V]]]] = V.

– V = n or V = x or V = A, then the result is immediate.

– V = λx.N, then:

W^{−1}[[W[[(λx.N)]]]] = W^{−1}[[(λ⟨x, s⟩.S[[N]]s)]]
= (λx.S^{−1}[[S[[N]]s]])
= (λx.(I[[s]] ; N))  (induction)
= (λx.(() ; N))
= (λx.N)  (β_{v})

– V = deref, then:

W^{−1}[[W[[deref]]]] = W^{−1}[[(λ⟨x, s⟩.s@x)]]
= (λx.S^{−1}[[s@x]])
= (λx.(I[[s]] ; (deref x)))

– V = setref!, then:

W^{−1}[[W[[setref!]]]] = W^{−1}[[(λ⟨x, s⟩.⟨(λ⟨y, s′⟩.⟨?, (upd s′ x y)⟩), s⟩)]]
= (λx.(I[[s]] ; λy.(I[[s′]] ; (setref! x y) ; ?)))

• M = (N_{1} N_{2}), then:

S^{−1}[[S[[(N_{1} N_{2})]]S]] = S^{−1}[[((λ⟨x, s⟩.(x S[[N_{2}]]s)) S[[N_{1}]]S)]]
= ((λx.(x (I[[s]] ; N_{2}))) (I[[S]] ; N_{1}))
= ((λx.(x N_{2})) (I[[S]] ; N_{1}))  (β_{v})
= I[[S]] ; ((λx.(x N_{2})) N_{1})

(Repeated application of (I_{4}))

= I[[S]] ; (N_{1} N_{2})  (I_{5})

3.2 Inverting the Store-Passing Axioms

To derive the complete equational theory that corresponds to the axioms ax(G_{1}), we apply the inverse store-passing transformation to these axioms. The result of inverting Q_{2} and Q_{3} yields the axioms I_{6} and I_{7}, respectively:

Definition 3.8. (I_{6} and I_{7})

(setref! A V) ; (deref A) = (setref! A V) ; V  (I_{6})
(setref! A_{1} V) ; (deref A) = ((λx.((setref! A_{1} V) ; x)) (deref A)) A_{1} ≠ A (I_{7})

The remaining axiom, Q_{1}, is not a simple first-order equation (it involves substitution). However, it turns out that the equivalence between the inversions of its right and left sides can be established using the set of axioms we have already developed. To show this, we require the following lemmas:

Lemma 3.9 (Substitution) Let P and W be terms of the appropriate sort in G_{1}, then S^{−1}[[P]][x := W^{−1}[[V]]] is identical to S^{−1}[[P [x := W]]].

Proof Idea. The proof is by induction on the structure of P and proceeds by cases.

Lemma 3.10 Let P, S and S_{1} be terms of the appropriate sort in G_{1}, then:

• ax(R_{1}) ⊢ (I[[S]] ; S^{−1}[[P]]) = S^{−1}[[P [s := S]]].

• ax(R_{1}) ⊢ (I[[S]] ; I[[S_{1}]]) = I[[S_{1}[s := S]]].

Proof. The proof is by induction on the structure of P or S_{1}. The proof relies on the fact that there is exactly one free store variable s in terms P and S and no free store variables in W:

• P = ⟨W_{1}, S_{1}⟩, then:

I[[S]] ; S^{−1}[[P]] = I[[S]] ; I[[S_{1}]] ; W^{−1}[[W_{1}]]
= I[[S_{1}[s := S]]] ; W^{−1}[[W_{1}]]
= S^{−1}[[⟨W_{1}, S_{1}[s := S]⟩]]

• P = (W_{1} P_{1}), then:

I[[S]] ; S^{−1}[[P]] = I[[S]] ; (W^{−1}[[W_{1}]] S^{−1}[[P_{1}]])
= (W^{−1}[[W_{1}]] (I[[S]] ; S^{−1}[[P_{1}]]))
= (W^{−1}[[W_{1}]] S^{−1}[[P_{1}[s := S_{1}]]])

• P = S_{1}@W_{1}, then:

I[[S]] ; S^{−1}[[P]] = I[[S]] ; I[[S_{1}]] ; (deref W^{−1}[[W_{1}]])
= I[[S_{1}[s := S]]] ; (deref W^{−1}[[W_{1}]])
= S^{−1}[[S_{1}[s := S]@W_{1}]]

• S_{1} = s, then:

I[[S]] ; I[[S_{1}]] = () ; I[[S_{1}]]
= I[[S_{1}]]
= I[[S_{1}[s := s]]]

• S_{1} = (upd S_{2} W_{1} W_{2}), then:

I[[S]] ; I[[S_{1}]] = I[[S]] ; I[[S_{2}]] ; (setref! W^{−1}[[W_{1}]] W^{−1}[[W_{2}]])
= I[[S_{2}[s := S]]] ; (setref! W^{−1}[[W_{1}]] W^{−1}[[W_{2}]])
= I[[(upd S_{2}[s := S] W_{1} W_{2})]]

Using Lemmas 3.9 and 3.10, we are now in a position to show that axiom Q_{1} is invertible:

Lemma 3.11 Let P, S, and W be terms of the appropriate sort in G_{1}. Then

(I_{1}–I_{7}) ⊢ S^{−1}[[((λ⟨x, s⟩.P) ⟨W, S⟩)]] = S^{−1}[[P [x := W, s := S]]]

Proof. The inverse of the left-hand side of the equation is:

((λx.S^{−1}[[P]]) (I[[S]] ; W^{−1}[[W]])) = I[[S]] ; ((λx.S^{−1}[[P]]) W^{−1}[[W]])

(Repeated application of (I_{4}))

= I[[S]] ; S^{−1}[[P]][x := W^{−1}[[W]]]  (β_{v})
= I[[S]] ; S^{−1}[[P [x := W]]]

(Substitution Lemma 3.9)

= S^{−1}[[P [x := W, s := S]]]

(Lemma 3.10)

The complete set of axioms ax(R_{1}) in Figure 1 consists of all the previously derived axioms. It proves the same equations that ax(G_{1}) proves on store-passing terms:

Theorem 3.12 ax(R_{1}) ⊢ M = N if and only if ax(G_{1}) ⊢ S[[M]]s = S[[N]]s (where s is a free variable).

Proof. Each direction is by induction on the length of proofs, using Lemmas 3.7 and 3.11, the derived axioms (I_{6}) and (I_{7}), and the fact that S^{−1}[[·]] is compositional.

4 Dynamic Allocation

We now extend the store-passing language with an operation that binds locations. The resulting language G_{2} is more realistic than G_{1}, since it can express various storage allocation (and de-allocation) protocols.

((λx.M) V) = M[x := V]  (I_{1} = β_{v})
deref = (λx.(deref x))  (I_{2})
setref! = (λx.λy.((setref! x y) ; ?))  (I_{3})
(V ((setref! V_{1} V_{2}) ; M)) = (setref! V_{1} V_{2}) ; (V M)  (I_{4})
(M N) = ((λx.(x N)) M)  (I_{5})
(setref! A V) ; (deref A) = (setref! A V) ; V  (I_{6})
(setref! A_{1} V) ; (deref A) = ((λx.((setref! A_{1} V) ; x)) (deref A))  A_{1} ≠ A  (I_{7})

Figure 1: Complete Set of Axioms ax(R_{1}).

Definition 4.1. (G_{2}) The language G_{2} extends G_{1} as follows:

P ::= … | (alloc A P)

In the term (alloc A P) the location A is bound in P. The usual notion of free variables in a term P is extended to include locations bound by alloc, and is notated F V (P). The formal semantics of the new construct is the following:

(W (alloc A P)) = (alloc A (W P))  A ∉ F V (W)  (Q_{4})
(alloc A P) = P  A ∉ F V (P)  (Q_{5})

The first axiom uses an idea of Felleisen et al. [8]; it “lifts” the binding of the location A to permit the evaluation of the application (W P). The condition A ∉ F V (W) ensures that alloc does not capture any free locations A in W and may require that the bound location A be renamed, e.g.,

((λ⟨d, s⟩.s@A) (alloc A ⟨A, S⟩)) = (alloc A_{1} ((λ⟨d, s⟩.s@A) ⟨A_{1}, S⟩)).

The second axiom is a garbage collection rule for de-allocating references. The theory ax(G_{2}) includes all the axioms in ax(G_{1}) as well as Q_{4} and Q_{5}.^{1}

Since the store-passing language G_{2} is more expressive than the previous language G_{1}, we can derive an equational theory for a correspondingly more expressive imperative language:

Definition 4.2. (R_{2}) The syntactic definition of the language R_{2} extends the one for R_{1} with the following clause:

V ::= … | (letref A M)

1Our approach to dynamic allocation has the advantage of simplicity and abstractness, but relies on the meta-operation of renaming to ensure uniqueness of addresses [8]. A more “concrete” allocation mechanism could be defined in any number of ways, but would require more complicated axioms to correctly reflect its internal behavior.

The semantics of the new construct is as expected:

S[[(letref A M)]]s = (alloc A S[[M]]s)

Informally, letref creates a reference cell and binds it to a new name.^{2} Using the inverse store-passing translation for alloc:

S^{−1}[[(alloc A P)]] = (letref A S^{−1}[[P]])

we can derive the equational theory for R_{2} that proves all the equations that G_{2} proves on store-passing terms. The development is similar to the one in the previous section. The resulting set of axioms includes all the axioms ax(R_{1}) and the following additional axioms:

(letref A (V M)) = (V (letref A M))  A ∉ F V (V)  (I_{8})
(setref! V_{1} V_{2}) ; (letref A M) = (letref A ((setref V_{1} V_{2}) ; M)) A ∉ F V (V_{1}, V_{2}) (I_{9})
(letref A M) = M  A ∉ F V (M)  (I_{10})

4.1 Related Calculi

When compared to other systems, the R_{2}-calculus has several distinguishing features. First, in contrast with calculi derived from abstract machines for the source imperative language [4, 8, 11], our equational theory never eliminates an expression of the form (setref! V_{1} V_{2}) (cf. Section 5). These expressions simply migrate from point to point within the program to allow lookup operations. In the other calculi [4, 8, 11], there is typically a distinguished position in the program text that contains the most recent value associated with a particular location: setref! expressions modify this current value and lookup operations copy this current value.

The R_{2}-calculus is closer in spirit to the theory λ_{var} [14] and the Imperative Lambda Calculus (ILC) [17] but differs in several technical respects. The theory λ_{var} uses a callby-name semantics for procedures and has an additional pure construct. It also uses a “monadic” operator to express the sequencing of assignments while the sequencing of assignments in R_{2} is implicit in the order of evaluation of applications. Finally, ILC does not include “first-class” reference cells as procedures cannot create reference cells and return them, e.g., the term (letref A A) is a valid program in our language but corresponds to a “dangling” pointer in ILC.

5 Extensions

Previous sections have concentrated on deriving calculi that are sufficiently powerful to evaluate programs. In this section, we turn our attention to extended target calculi and their effect on logics for source languages. We will concentrate on adding axioms for proving equivalences on open terms that are useful for optimization. In addition, we will consider certain functional extensions.

ref = λx.(letref A ((setref! A x) ; A)).

2The language can express ML-like reference cells as follows:

5.1 Lazy Store

We extend G_{2} with a lazy store update operation in addition to the conventional strict operation:

S ::= … | (upd_{ℓ} W P)

The lazy store semantics generalizes the strict semantics [3] and can be used to justify many optimizations in imperative languages that would be inconsistent with strict store semantics [3, 9]. Intuitively, the evaluation of a program may terminate in the lazy store semantics but diverge in the strict store semantics. However, if both evaluations terminate then the two semantics agree on the final answer. The formal semantics of the new lazy store update operation is defined in terms of the old update operation as follows:

(upd_{ℓ} A_{1} P)@A = ((λ⟨x, s⟩.(upd s A_{1} x)@A) P)

In other words, the evaluation of P does not happen until requested by a lookup operation.

By following a development similar to the previous sections, we extend the source language with a corresponding lazy assignment:

M ::= … | (setref!_{ℓ} M M)

The translations between the two languages are:

S[[(setref!_{ℓ} M_{1} M_{2})]]s = ((λ⟨x, s′⟩.⟨?, (upd_{ℓ} x S[[M_{2}]]s′)⟩) S[[M_{1}]]s)
I[[(upd_{ℓ} W P)]] = (setref!_{ℓ} W^{−1}[[W]] S^{−1}[[P]])

This definition implies that the location into which a value is stored is computed strictly, but the expression associated with the location is not evaluated until it is needed by some dereference operation.

The resulting theory for the source language includes all the previously derived axioms and the following axioms:

(setref!_{ℓ} A_{1} M) ; (deref A) = ((λx.((setref! A_{1} x) ; (deref A))) M)  (I_{11})
(setref! V_{1} V_{2}) ; (setref!_{ℓ} V M) = (setref!_{ℓ} V ((setref! V_{1} V_{2}) ; M))  (I_{12})
(setref!_{ℓ} M_{1} M_{2}) = ((λx.(setref!_{ℓ} x M_{2}) ; ?) M_{1})  (I_{13})

5.2 Extensions to the Imperative Fragment

We can extend the axioms for the imperative fragments to include equations that axiomatize the store datatype. This is the approach taken in the logic Pim [9], and we consider a few similar extensions here. For example, we may include the following axioms:

(upd (upd S A_{1} W_{1}) A_{2} W_{2}) = (upd (upd S A_{2} W_{2}) A_{1} W_{1})

A_{1} ≠ A_{2} and A_{1} ∉ F V (W_{2})

(upd (upd S A W_{1}) A W_{2}) = (upd S A W_{2})

The corresponding axioms in the source language are immediately obtained by applying the inverse store-passing transformation:

(setref! A_{1} V_{1}) ; (setref! A_{2} V_{2}) = (setref! A_{2} V_{2}) ; (setref! A_{1} V_{1})
A_{1} ≠ A_{2} and A_{1} ∉ F V (V_{2})
(setref! A V_{1}) ; (setref! A V_{2}) = (setref! A V_{2})

5.3 Extensions to the Functional Fragment

We can also extend the axioms for the functional fragments to a more powerful call-by-value logic such as the computational λ-calculus [13]. Because the sequencing operation can be expressed using procedures, extensions to the functional fragment prove more equations between imperative terms. The following example shows the effect of adding the axiom β_{lift} [13, 15]:

(setref!_{ℓ} A M) ; (deref A) ; (deref A_{1})
= ((λx.(setref! A x) ; (deref A)) M) ; (deref A_{1}) (I_{11})
= ((λx.(setref! A x) ; x) M) ; (deref A_{1})  (I_{5})
= ((λx.(setref! A x) ; x ; (deref A_{1})) M)  (β_{lift})
= ((λx.(setref! A x) ; (deref A_{1})) M)  (β_{v})
= (setref!_{ℓ} A M) ; (deref A_{1})  (I_{12})

The equation is not provable without the additional axiom.

5.4 Extensions to the Store Representation

In addition to providing additional axioms to obtain more complete logics, it is also possible to provide functional extensions to our store algebras to model additional source language constructs. For example, arrays can be modeled in a straightforward manner by locations that are tuples of the form ⟨base, offset⟩, where base is one of the “atomic” locations we have defined previously, and offset is an integer offset. The location comparison implicitly required by the store lookup axioms must be correspondingly redefined to operate on such pairs. Implicit renaming performed by the alloc construct carries over without change to the extended representation for locations.

6 Assessment

We have shown here that equational logics for a family of representative programming languages can be defined in a particularly effective way by translation to simple, “orthogonal” target calculi. These calculi extend the untyped lambda-calculus with store constructs and simple store algebras.

Imperative programs typically have two aspects that complicate reasoning: the inherent behavior of the store, and the complications of sequencing operations on the store amidst other fundamental operations. When the store sequencing aspects of the language are encoded by translation to a target calculus, our approach allows source axioms to be developed that mirror the behavior of the translation, independently of the axioms that merely “implement the store.”

Although our derived source axioms are complete relative to the axioms of the store algebra, the latter theories do not provide a complete axiomatization of the observational equivalence relation for any of the presented imperative languages, and are therefore semantically incomplete. It is expected that we cannot achieve semantic completeness with untyped languages such as the ones we used in the previous sections. However, the incompleteness problem is much more fundamental. Even in a simply typed language, assignments can be used to define recursive or cyclic data structures, e.g., the evaluation of the following simply typed program diverges:^{3}

(setref! A^{ref (int→int)} (λx^{int}.x^{int})) ; (setref! A (λx.((deref A) x))) ; ((deref A) 0).

The technique of deriving equational logics by analyzing the translations between two languages is necessarily limited by the “expressive power” of the source language. In other words, for each term in one language, there should be a corresponding term in the other language that has the same behavior in all contexts. Cases of mismatch between the constructs in the languages require special consideration. Indeed, it need not be the case that any equational logic exists, however derived, which can prove all equations that are true in some semantic model—even when considering only closed terms.

However even when equational logics cannot be derived by our technique, we believe there is considerable benefit to adopting our approach to defining the semantics of imperative languages via translation, since this process may be used to obtain deeper understanding of the language’s semantics.

Acknowledgments

We thank Matthias Felleisen for suggesting several improvements in the presentation and for clarifying several historical facts. We also thank the reviewers for helpful comments.

References

[1] Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, revised edition (1984).

[2] Boehm, H.-J. Side effects and aliasing can have simple axiomatic descriptions. ACM Transactions on Programming Languages and Systems, 7, 4 (October 1985) 637–655.

[3] Cartwright, R. and Felleisen, M. The semantics of program dependence. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (1989) 13–27.

[4] Crank, E. and Felleisen, M. Parameter-passing and the lambda calculus. In Conference Record of the 18th ACM Symposium on Principles of Programming Languages (1991) 233–244.

3It is possible to use a type system that rejects the above program and that guarantees that the evaluation of “simply typed” programs terminates [17]. With such restrictions, it may be possible to axiomatize the observational equivalence relation.

[5] Curry, H. B. and Feys, R. Combinatory Logic, Volume I. North-Holland, Amsterdam (1958).

[6] Demers, A. and Donahue, J. Making variables abstract: An equational theory for Russell. In Conference Record of the 10th ACM Symposium on Principles of Programming Languages (1983) 59–72.

[7] Felleisen, M. and Friedman, D.P. A calculus for assignments in higher-order languages. In Conference Record of the 14th ACM Symposium on Principles of Programming Languages (1987) 314–325.

[8] Felleisen, M. and Hieb, R. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 102 (1992) 235–271. Technical Report 89-100, Rice University.

[9] Field, J. A simple rewriting semantics for realistic imperative programs and its application to program analysis (preliminary report). In ACM Sigplan Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Technical Report RR-909, Yale University (1992) 98–107.

[10] Hoare, C., Hayes, I., Jifeng, H., Morgan, C., Roscoe, A., Sanders, J., Sorensen, I., Spivey, J., and Sufrin, B. Laws of programming. Communications of the ACM, 30, 8 (1987) 672–686.

[11] Mason, I. and Talcott, C. Equivalence in functional languages with effects. Journal of Functional Programming, 1, 3 (July 1991) 287–327.

[12] Mason, I.A. and Talcott, C. Inferring the equivalence of functional programs that mutate data. Theoretical Computer Science, 105, 2 (1992) 167–215. Preliminary version in Proceedings of the 4th IEEE Symposium on Logic in Computer Science 1989.

[13] Moggi, E. Computational lambda-calculus and monads. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science (1989) 14–23. Also appeared as: LFCS Report ECS-LFCS-88-86, University of Edinburgh, 1988.

[14] Odersky, M., Rabin, D., and Hudak, P. Call by name, assignment, and the lambda calculus. In Conference Record of the 20th ACM Symposium on Principles of Programming Languages (January 1993) 43–56.

[15] Sabry, A. and Felleisen, M. Reasoning about programs in continuation-passing style. Lisp and Functional Programming (1993). To appear. Preliminary version in Proceedings of the ACM Conference on Lisp and Functional Programming, 1992. Also Technical Report 92-180, Rice University.

[16] Strachey, C. Towards a formal semantics. In Steel, T.B., editor, Formal Language Description Languages for Computer Programming, North-Holland (1966) 197–220.

[17] Swarup, V., Reddy, U., and Ireland, E. Assignments for applicative languages. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (1991) 192–214.