Georg Moser, Predicative Recursion and Register Machines
Predicative Recursion and Register Machines
In this talk I will propose a termination order, dedicated for complexity analysis, the small polynomial path order (sPOP* for short). This order provides a new characterisation of the class of polytime computable function via term rewrite systems. Based on sPOP*, we'll study a class of rewrite systems, dubbed systems of predicative recursion of degree d, such that for rewrite systems in this class we obtain that the runtime complexity lies in O(n^d). We show that predicative recursive rewrite systems of degree d define functions computable on a register machine in time O(n^d). This result emphasises the fact that (innermost) runtime complexity of a rewrite system is an invariant cost model.