Elementary complexity and geometry of interaction (Q2708316)

The aim of the paper is to define a setting as large, and simple, as possible for elementarily bounded computations. An algebra of clauses is presented along the lines of \textit{J.-Y. Girard}'s paper [in: J.-Y. Girard et al. (eds.), Advances in linear logic. Lond. Math. Soc. Lect. Note Ser. 222, 329-389 (1995; Zbl 0828.03027)] with a kind of depth-preservation property analogous to that of Elementary Linear Logic (ELL). Execution is defined through resolution and the operators are certain sets of clauses. In addition to usual execution formulas weak execution is defined which amounts to giving up the computation of certain products of execution. Weak execution coincides with usual execution for operators coming from proof-nets. NEWLINENEWLINENEWLINESize and depth are defined for general operators. The main result being that weak execution always terminates and that when the depth is fixed, the number of steps of the computation is bounded by a function of the size of the program which is elementary, that is, a bound can be computed in advance, provided that size and depth are known. Therefore the intrinsic elementary bound obtained in ELL by logical means has been extended to a semantic setting.