| Equality Between Functionals in the Presence of Coproducts (1995) | |||||||||||||||
Abstract | |||||||||||||||
| We consider the lambda-calculus obtained from the simply-typed calculus by adding products, coproducts, and a terminal type. We prove the following theorem: The equations provable in this calculus are precisely those true in any set-theoretic model with an infinite base type. 1 Introduction The model theory of the simply-typed lambda calculus, ! , has been well developed in the last two decades. For the most part, techniques and results generalize readily to the calculus when product types are added. Indeed, a categorical treatment goes more smoothly in the presence of products. But very little is known about the model theory of the simplytyped lambda calculus with coproducts for two chief reasons. First, techniques in the model theory of ! often rely heavily on the strong syntactic properties of the calculus; many of these properties fail in the presence of coproducts. Second, the natural generalizations of several key theorems in the model theory of ! fail in the setting wi... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||