A sound and complete axiomatization of operational equivalence between programs with memory

ABSTRACT

In this paper we present a formal system for deriving assertions about programs with memory. The assertions we consider are of the following three forms: (i) e diverges (i.e. fails to reduce to a value), written $\arru e$; (ii) $e_O$ and $e_1$ reduce to the same value and have exactly the same effect on memory, written $e_O \bksimlr e_1$; and (iii) $e_O$ and $e_1$ reduce to the same value and have the same effect on memory up to production of garbage (are strongly isomorphic), written $_O \bksimeq e_1$. The e, $e_j$ are expressions of a first-order Scheme- or Lisp-like language with the data operations atom, eq, car, cdr, cons, setcar, setcdr, the control primitives let and if, and recursive definition of function symbols.