| Algebraic Reasoning and Completeness in Typed Languages (1992) | |||||||||||||||
Abstract | |||||||||||||||
| : We consider the following problem in proving observational congruences in 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 observational congruences between terms exactly those provable from (fi), (j), and E? We find conditions for determining whether fijE-equational reasoning is complete for proving the observational congruences 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 (fi) and (j) axioms form the basis for proving equations in call-by-name functional languages. In these languages, (fi) and (j) yield sound program optimizations. For example, consider a version of the call-by-name language PCF [11, 15] which is described in Appendix A. Our version of PCF includes simplytyped -calculus, numerals 0; 1; 2; : : :, successor and predecessor, addition, ... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||