Algebraic Reasoning and Completeness in Typed Languages

Abstract

We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simply-typed λ-calculus with algebraic operations axiomatized by algebraic equations E, is the set of observational congruences between terms exactly those provable from (β), (η), and E? We find conditions for determining whether βηE-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.