Conservativity of Equational Theories in Typed Lambda Calculi1

In programming languages that feature unrestricted recursion, the equational theory corresponding to evaluation of data type expressions must be distinguished from the classical theory of the data as given by, say, algebraic specifications. Aiming to preserve classical reasoning about the underlying data types, that is, for the equational theory of the programming language to be a conservative extension of the theory given by the data type specification, we investigate, alternative computational settings given by typed lambda calculi, specifically here by the Girard-Reynolds polymorphic lambda calculus ( λ ∀ ). We prove that the addition of just the λ ∀ -constructions to arbitrary specifications, as given by algebraic theories, and even simply typed lambda theories, is conservative. This suggests that polymorphic constructs and reasoning can be superimposed on familiar data-type definition features of programming languages without changing the behavior of these features. Using purely syntactic methods, we give transformational proofs of these results for certain systems of equational reasoning. A new technique for analyzing polymorphic equational proofs is developed to this purpose. Finally, we prove, with a semantics argument, that it is possible to combine arbitrary algebraic data type specifications and the λ ∀ -constructions into functional programming languages that both conserve algebraic reasoning about data. and ensure, over arbitrary algebraically specified observables, a computing power equivalent to that of the pure λ ∀ . The corresponding problem for simply typed specifications remains open.