Conditions for the Completeness of Functional and Algebraic Equational Reasoning

We consider the following problem in proving equations in models of functional languages: given a call-by-name language based on the simplytyped -calculus with algebraic operations axiomatized by algebraic equations E, is the set of equations between terms exactly those provable from (fi), (j), and E? We find conditions for determining whether fijE- equational reasoning is complete for proving equations between such terms. We demonstrate the power and generality of the theorems by presenting a number of easy corollaries for particular algebras. 1 Introduction The two simple axioms of the -calculus, (fi) ((x: M) N) = M [x := N ] (j) (x: M x) = M; if x not free in M lie at the heart of reasoning about functional programs: (fi) explains function application syntactically, and (j) states that the meaning of functions can be based solely on their meaning under application. But the axioms have uses in reasoning about programs as well: the axioms (fi) and (j) yield sound program optimiz..