No CrossRef data available.
Conditions for the completeness of functional and algebraic equational reasoning
Published online by Cambridge University Press: 01 December 1999
Abstract
We consider the following question: in the simply-typed λ-calculus with algebraic operations, is the set of equations valid in a particular model exactly those provable from (β), (η) and the set of algebraic equations, E, that are valid in the model? We find conditions for determining whether βηE-equational reasoning is complete. We demonstrate the utility of the results by presenting a number of simple corollaries for particular models.
- Type
- Research Article
- Information
- Copyright
- 1999 Cambridge University Press