Helmut Schwichtenberg

15. March 2016 (Departmental Seminar)

Linear two-sorted constructive arithmetic

We consider a term system in the style of Gödel’s system T together with a computation model that allows to faithfully represent polynomial-time algorithms. To this end we follow a tradition initiated by Simmons (1988) and developed by Bellantoni and Cook (1992), where two sorts of variables are admitted, here called output and input variables. The idea is that input variables are the general ones which may be recursed on and used many times, whereas output variables cannot be recursed on and can be used only once. These ideas have been extended to a higher type setting and hence – via the Curry Howard correspondence – to a linear two-sorted arithmetical system in the style of Heyting arithmetic in all finite types. Here we further extend this setup with the aim to also include certain nonlinear algorithms (like treesort), given by constants defined by equations involving multiple recursive calls.