[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Reasoning about Functions with Effects
Talcott, C. L. - 1996

This paper presents a unified framework for reasoning about program equivalence in imperative functional languages such and Scheme, Lisp, ML A notion of uniform semantics for lambda-languages is defined, and general principles are developed for reasoning about program equivalence in any lambda language with uniform semantics. For such languages we have the combined benefits of reduction calculi (modular axiomatization), and operational equivalence (more equations). A lambda-language is a programming language obtained by augmenting the lambda calculus with primitive operations that include not only basic constants, branching, and algebraic operations such as arithmetic and pairing, but also operations that manipulate the computation state (store, continuation), and the environment (sending messages, creating processes). The operational semantics of a lambda-language is given by providing a reduction rule for each primitive operation. The semantics is said to be uniform if it satisfies two uniformity conditions spelled out in the paper. The key requirement is uniform computation which allows computation steps to be carried out on states with missing information. It has the property that computing commutes with filling in of missing information. A key result for lambda languages with uniform semantics is the CIU theorem (first presented by Mason and Talcott at ICALP89) which is a form of context lemma. Using CIU and other consequences of uniform semantics two general principles for proving program equivalence are established that capture computational intuitions: programs with equivalence reducts are equivalent; expressions placed in equivalent contexts yield equivalent programs. Simulation principles are also established for proving equivalence of imperative functions (aka lambdas) and objects (which have private store). The semantics of a Scheme-like language with algebraic, control, and memory primitives is deveoped as an illustration of the ideas.