AI 中文总结
研究将项重写系统扩展为量子项重写系统，通过适配技术获终止性证书及归约长度界限，划定一类可终止的QTRS，其可编译成特定量子电路族，且对量子电路通用，还给出量子多项式时间可计算函数类的特征。
AI 中文摘要
项重写系统（TRS）是一种计算模型，适用于静态分析，如终止性或复杂性分析。本文引入量子项重写系统（QTRS），它是TRS在量子计算方面的扩展，能在利用量子优势的同时认证复杂性。确保QTRS对应可物理实现的过程，并采用技术获得终止性证书或归约长度的通用界限。划定一类可终止的QTRS，能编译成大小受归约长度限制的量子电路统一族，反之该类对量子电路具有通用性。特别给出了量子多项式时间可计算函数类（即$\mathtt{FBQP}$）的特征描述。
英文摘要
Term Rewrite Systems (TRS) is a computational model offering a level of abstraction well-suited towards static analysis, e.g., termination or complexity analyses. In this paper, we introduce Quantum Term Rewrite Systems (QTRS), an extension of TRS to quantum computing, thus allowing to benefit from quantum advantage while being able to certify the complexity. We ensure that QTRS correspond to physically realizable processes and adapt techniques to obtain termination certificates or generic bounds on the reduction length. We delineate a class of terminating QTRS that can be compiled to uniform families of quantum circuits of size bounded by the reduction length. Conversely, this class is universal for quantum circuits. In particular, we show a characterization of the class of functions computable in quantum polynomial time, known as $\mathtt{FBQP}$.
