The Safe Lambda Calculus

摘要

Safety is a syntactic condition of higher-order grammars that constrainsoccurrences of variables in the production rules according to theirtype-theoretic order. In this paper, we introduce the safe lambda calculus,which is obtained by transposing (and generalizing) the safety condition to thesetting of the simply-typed lambda calculus. In contrast to the originaldefinition of safety, our calculus does not constrain types (to behomogeneous). We show that in the safe lambda calculus, there is no need torename bound variables when performing substitution, as variable capture isguaranteed not to happen. We also propose an adequate notion of beta-reductionthat preserves safety. In the same vein as Schwichtenberg's 1976characterization of the simply-typed lambda calculus, we show that the numericfunctions representable in the safe lambda calculus are exactly themultivariate polynomials; thus conditional is not definable. We also give acharacterization of representable word functions. We then study the complexityof deciding beta-eta equality of two safe simply-typed terms and show that thisproblem is PSPACE-hard. Finally we give a game-semantic analysis of safety: Weshow that safe terms are denoted by `P-incrementally justified strategies'.Consequently pointers in the game semantics of safe lambda-terms are onlynecessary from order 4 onwards.