Predicative Copying and Polynomial Time

We use combinators to give a simple formulation of type-free applicative (i.e. functional programming) systems. The classical SK combinators allow all partial recursive functions to be represented, while the BCK combinators (corresponding to `affine' lambda calculus) normalize in linear time. To capture some intermediate classes of functions, we recall the notion of *Linear Combinatory Algebra* introduced by the present author, which gives a presentation of the computational ideas of Multiplicative Exponential Linear Logic in a combinatory format. Since standard combinatory logic can be interpreted into Linear Combinatory Logic, once again all recursive functions can be represented. However, in this refined setting we have more scope for capturing intermediate possibilities. If we remove the comultiplication combinator, and replace the contraction combinator by a `bounded' or `predicative' version, in which the number of copies made has to be decided a priori, then we obtain a system which characterizes polynomial time. This system is related to Lafont's `Soft Linear Logic'. It is a strikingly simple system, which admits a very simple and natural notion of model, by contrast to Girard's system of Light Linear Logic, which has to add a new modality to compensate for the loss of dereliction and monoidality. For this reason, it may prove useful in obtaining a semantic perspective on complexity classes.