An Optimization of Lambda Type assignments via Resource Control#

Abstract

The size of a lambda term’s type assignment is traditionally interpreted as the number of involved typing rules, but can be also assessed using some finer-grained measures such as the number of involved type declarations (TD). We propose a type assignment method that relies on the translation of a typeable lambda term to the corresponding term of a modified resource control lambda calculus. The translation output of a given lambda term is often syntactically more complex, therefore more rules need to be used for its type assignment in the target calculus. However, we show that TD measure decreases when types are assigned to terms satisfying a certain minimal level of complexity, thus our method represents an optimization of the lambda calculus’ type assignment.