| Conditions for the Completeness of Functional and Algebraic Equational Reasoning (1998) | |||||||||||||||
Abstract | |||||||||||||||
| We consider the following question: in the simply-typed l-calculus with algebraic operations, is the set of equations valid in a particular model exactly those provable from (b), (h), and the set of algebraic equations, E, that are valid in the model? We find conditions for determining whether bhE-equational reasoning is complete. We demonstrate the utility of the results by presenting a number of simple corollaries for particular models. 1 Introduction The two axioms of the l-calculus, (b) ((lx: M) N) =M[x := N] (h) (lx: M x) =M; if x not free in M lie at the heart of reasoning about functional programs: (b) explains function application syntactically, and (h) states that the meaning of functions can be based solely on their meaning under application. The (b) and (h) axioms turn out to be fundamental: not only are they sound, they also are complete for proving equations that hold in all models of the simply-typed l-calculus [Friedman, 1975]. In other words, an equation between sim... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||