Safe recursion revisited I: Categorical semantics for lower complexity

The objective of this paper is to prove that the initial Pola setting, with both inductive and coinductive data, is sound for polynomial size (PSIZE). Explicitly this means all programs written in Pola have their output size bounded by a polynomial in their input size. The paper describes the polarized categorical semantics for Pola and establishes the result by providing categorical models for various fragments of Pola which have explicit size bound information built into the maps.To obtain PSIZE soundness for Pola with just inductive data, the semantics in sized sets suffices. Sized sets are sets equipped with a “size map” which associates to each element a size. Size is usually just a natural number but, more generally, the size could be an element of a size rig. A polarized category consists of an opponent and a player category joined by a module. Sized sets can be used to create a polarized category by letting the opponent and module maps be bounded by polynomials while the player category consists of maps bounded by a constant. This gives a Pola setting with inductive data and immediately establishes the PSIZE soundness of the initial Pola setting.The main technical difficulty of the paper is to provide a semantics which correctly models coinductive data as well. For this “amortized” sets are introduced: these are set in which a higher-order size function is associated to each element, which given a size returns a size. This is amortized as one is concerned with the asymptotic behavior of these functions. While amortized sets have coinductive data they are not affine closed: a final step, using equivalence relations, is required to obtain a model which includes this aspect of Pola structure.While PSIZE by itself is a very weak bound it is a crucial step in establishing polynomial space (PSPACE) and polynomial time (PTIME) bounds for these settings.