论文标题
逻辑上约束重写的运行时复杂性分析
Runtime Complexity Analysis of Logically Constrained Rewriting
论文作者
论文摘要
逻辑上受约束的重写系统（LCTRS）是一种多功能，有效的重写形式主义，可用于模拟各种编程范式中的程序，以及编译器和SMT求解器中的简化系统。在本文中，我们研究了分析LCTRS最严重的运行时复杂性的技术。为此，我们利用了先前开发的分解技术之间的协同作用，该技术由Avanzini等人的标准术语重写。结合Brockschmidt等人的整数程序的交替时间和大小结合近似值。并适当地适应LCTRS。此外，我们提供了新型的模块化技术来利用产生额定性界限的复发方程式的循环边界。我们已经在TCT中实现了测试方法可行性的方法。
Logically constrained rewrite systems (LCTRSs) are a versatile and efficient rewriting formalism that can be used to model programs from various programming paradigms, as well as simplification systems in compilers and SMT solvers. In this paper, we investigate techniques to analyse the worst-case runtime complexity of LCTRSs. For that, we exploit synergies between previously developed decomposition techniques for standard term rewriting by Avanzini et al. in conjunction with alternating time and size bound approximations for integer programs by Brockschmidt et al. and adapt these techniques suitably to LCTRSs. Furthermore, we provide novel modularization techniques to exploit loop bounds from recurrence equations which yield sublinear bounds. We have implemented the method in TCT to test the viability of our method.
