A mixed modal/linear lambda calculus with applications to Bellatoni-Cook safe recursion

This paper introduces a simply-typed lambda calculus with both modal and linear function types. Through the use of subtyping extra term formers associated with modality and linearity are avoided. We study the basic metatheory of this system including existence and inference of principal types. The system serves as a platform for certain higher-order generalisations of Bellantoni-Cook's function algebra capturing polynomial time using a separation of the variables into "safe" and "normal" ones. The distinction between and the syntactic restrictions involved with the safe and normal variables in the Bellantoni-Cook framework are captured by the modal function space and the associated typing rules. The linear function spaces on the other hand are used to enable a certain form of primitive recursion with functional result type which is conservative over polynomial time. The proofs associated with these applications are based on an interpretation of the lambda calculus in a category-theoretic model in which all functions are polynomial time computable by construction The details of this interpretation are not the main subject of this paper and will appear elsewhere.