Type Introduction for Runtime Complexity Analysis

ABSTRACT. In this note we show that the runtime complexity function of a sorted rewrite system R coincides with the runtime complexity function of the unsorted rewrite system obtained by forgetting sort information. Hence our result states that sort-introduction, a process that is easily carried out via unification, is sound for runtime complexity analysis. Our result thus provides the foundation for exploiting sort information in analysis of TRSs.