2-or-more approximation for intuitionistic logic
Gabriel Scherer · HAL (Le Centre pour la Communication Scientifique Directe) · 2014
In the context of the simply-typed lambda-calculus (propositionalintuitionistic logic) with products and sums, we will answer the followingquestion. Given a fixed logic proof and typing environment, the number of possible programs that correspond to this proof depends on the number of free variables of each type in the type environment. If we are not interested in the precise number of programs but only "zero, one, or two-or-more", is it correct to approximate the number of variables at each type by "zero, one, or two-or-more"?