Sound and Complete Axiomatization of Operational Equivalence between Programs with Memory

摘要

In this paper the authors present a formal system for deriving assertions about programs with memory. The assertions they consider are of the following three forms: (1) e diverges (i.e. fails to reduce to a value); (2) e(sub 0) and e(sub 1) reduce to the same value and have exactly the same effect on memory; and (3) e(sub 0) and e(sub 1) reduce to the same value and have the same effect on memory up to production of garbage (are strongly isomorphic). The e, e(sub 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.