Logic in Computer Science

• New submissions
• Cross-lists
• Replacements

See recent articles

Showing new listings for Friday, 26 September 2025

New submissions (showing 3 of 3 entries )

[1] arXiv:2509.20409 [cn-pdf, pdf, html, other]

Title: A Unified Formal Theory on the Logical Limits of Symbol Grounding Show Chinese title

Title: 一种关于符号根基逻辑极限的统一形式理论

Zhangchi Liu

Comments: 8 pages, 1 figure. A formal proof on the logical limits of symbol grounding

Subjects: Logic in Computer Science (cs.LO)

This paper synthesizes a series of formal proofs to construct a unified theory on the logical limits of the Symbol Grounding Problem. We demonstrate through a four-stage argument that meaning within a formal system must arise from a process that is external, dynamic, and non-algorithmic. First, we prove that any purely symbolic system, devoid of external connections, cannot internally establish a consistent foundation for meaning due to self-referential paradoxes. Second, we extend this limitation to systems with any finite, static set of pre-established meanings, proving they are inherently incomplete. Third, we demonstrate that the very "act" of connecting an internal symbol to an external meaning cannot be a product of logical inference within the system but must be an axiomatic, meta-level update. Finally, we prove that any attempt to automate this update process using a fixed, external "judgment" algorithm will inevitably construct a larger, yet equally incomplete, symbolic system. Together, these conclusions formally establish that the grounding of meaning is a necessarily open-ended, non-algorithmic process, revealing a fundamental, G\"odel-style limitation for any self-contained intelligent system. Show Chinese abstract

本文综合了一系列形式证明，以构建关于符号奠基问题逻辑极限的统一理论。 我们通过一个四阶段的论证表明，形式系统内的意义必须来自于一种外部的、动态的且非算法的过程。 首先，我们证明任何纯粹的符号系统，如果没有外部联系，由于自指悖论，无法在内部建立一致的意义基础。 其次，我们将这一限制扩展到具有任何有限、静态预设意义的系统，证明它们本质上是不完整的。 第三，我们证明将内部符号与外部意义连接的“行为”不可能是系统内部逻辑推理的结果，而必须是一个公理性的、元层次的更新。 最后，我们证明任何尝试使用固定的外部“判断”算法来自动化这一更新过程，都会不可避免地构建出一个更大但同样不完整的符号系统。 综上所述，这些结论形式化地确立了意义的奠基是一个必然开放、非算法的过程，揭示了任何自洽智能系统的一个根本性、哥德尔式的限制。

[2] arXiv:2509.20931 [cn-pdf, pdf, other]

Title: Reverse Faà di Bruno's Formula for Cartesian Reverse Differential Categories Show Chinese title

Title: 反向 Faà di Bruno 公式用于笛卡尔反向微分范畴

Aaron Biggin (Macquarie University), Jean-Simon Pacaud Lemay (Macquarie University)

Comments: In Proceedings ACT 2024, arXiv:2509.18357

Journal-ref: EPTCS 429, 2025, pp. 115-129

Subjects: Logic in Computer Science (cs.LO) ; Machine Learning (cs.LG)

Reverse differentiation is an essential operation for automatic differentiation. Cartesian reverse differential categories axiomatize reverse differentiation in a categorical framework, where one of the primary axioms is the reverse chain rule, which is the formula that expresses the reverse derivative of a composition. Here, we present the reverse differential analogue of Faa di Bruno's Formula, which gives a higher-order reverse chain rule in a Cartesian reverse differential category. To properly do so, we also define partial reverse derivatives and higher-order reverse derivatives in a Cartesian reverse differential category. Show Chinese abstract

反向微分是自动微分中的基本操作。 笛卡尔反向微分范畴在范畴框架中公理化了反向微分，其中一个主要公理是反向链式法则，该公式表达了复合函数的反向导数。 在这里，我们提出了法多布罗尼公式（Faa di Bruno's Formula）的反向微分类似形式，它在一个笛卡尔反向微分范畴中给出了高阶反向链式法则。 为了正确地做到这一点，我们还在一个笛卡尔反向微分范畴中定义了偏反向导数和高阶反向导数。

[3] arXiv:2509.20933 [cn-pdf, pdf, other]

Title: A Coalgebraic Model of Quantum Bisimulation Show Chinese title

Title: 一种量子对等性的代数模型

Lorenzo Ceragioli (IMT School for Advanced Studies, Lucca, Italy), Elena Di Lavore (University of Pisa, Italy), Giuseppe Lomurno (University of Pisa, Italy), Gabriele Tedeschi (University of Pisa, Italy)

Comments: In Proceedings ACT 2024, arXiv:2509.18357

Journal-ref: EPTCS 429, 2025, pp. 249-269

Subjects: Logic in Computer Science (cs.LO) ; Emerging Technologies (cs.ET)

Recent works have shown that defining a behavioural equivalence that matches the observational properties of a quantum-capable, concurrent, non-deterministic system is a surprisingly difficult task. We explore coalgebras over distributions taking weights from a generic effect algebra, which subsumes probabilities and quantum effects, a physical formalism that represents the probabilistic behaviour of an open quantum system. To abide by the properties of quantum theory, we introduce monads graded on a partial commutative monoid, intuitively allowing composition of two processes only if they use different quantum resources, as prescribed by the no-cloning theorem. We investigate the relation between an open quantum system and its probabilistic counterparts obtained when instantiating the input with a specific quantum state. We consider Aczel-Mendler and kernel bisimilarities, advocating for the latter as it characterizes quantum systems that exhibit the same probabilistic behaviour for all input states. Finally, we propose operators on quantum effect labelled transition systems, paving the way for a process calculi semantics that is parametric over the quantum input. Show Chinese abstract

最近的研究表明，定义一个行为等价性，使其匹配具有量子能力的并发非确定性系统的观察特性，是一个令人惊讶的困难任务。 我们探讨了在分布上使用来自通用效应代数的权重的余代数，这涵盖了概率和量子效应，这是一种表示开放量子系统概率行为的物理形式。 为了遵守量子理论的性质，我们引入了一个在部分交换独异点上分级的单子，直观上允许仅当两个过程使用不同的量子资源时才能进行组合，这由不可克隆定理规定。 我们研究了开放量子系统与其在将输入实例化为特定量子状态时获得的概率对应物之间的关系。 我们考虑了Aczel-Mendler和核双模拟性，主张后者，因为它可以表征对于所有输入状态都表现出相同概率行为的量子系统。 最后，我们提出了量子效应标记转移系统的运算符，为一种对量子输入参数化的进程演算语义铺平了道路。

Cross submissions (showing 2 of 2 entries )

[4] arXiv:2509.20539 (cross-list from math.CO) [cn-pdf, pdf, other]

Title: Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified Show Chinese title

Title: 塞缪尔定理在正则拟阵中的组合方向 -- 形式化验证

Martin Dvorak, Tristan Figueroa-Reid, Rida Hamadani, Byung-Hak Hwang, Evgenia Karunus, Vladimir Kolmogorov, Alexander Meiburg, Alexander Nelson, Peter Nelson, Mark Sandey, Ivan Sergeev

Subjects: Combinatorics (math.CO) ; Logic in Computer Science (cs.LO)

Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory faces many challenges, most importantly that only a limited number of notions and results have been implemented so far. In this work, we formalize the proof of the forward (composition) direction of Seymour's theorem for regular matroids. To this end, we develop a library in Lean 4 that implements definitions and results about totally unimodular matrices, vector matroids, their standard representations, regular matroids, and 1-, 2-, and 3-sums of matrices and binary matroids given by their standard representations. Using this framework, we formally state Seymour's decomposition theorem and implement a formally verified proof of the composition direction in the setting where the matroids have finite rank and may have infinite ground sets. Show Chinese abstract

塞缪尔的分解定理是拟阵理论中的一个标志性结果，提出了对正则拟阵类的结构特征描述。 拟阵理论的形式化面临许多挑战，尤其是目前只有有限数量的概念和结果已经被实现。 在本工作中，我们形式化了正则拟阵的塞缪尔定理的正向（组合）方向的证明。 为此，我们在Lean 4中开发了一个库，实现了关于全单模矩阵、向量拟阵及其标准表示、正则拟阵以及由其标准表示给出的矩阵和二元拟阵的1-、2-和3-和的定义和结果。 利用这个框架，我们形式化地陈述了塞缪尔的分解定理，并在拟阵具有有限秩且可能具有无限基集的情况下，实现了该方向的正式验证证明。

[5] arXiv:2509.20932 (cross-list from cs.GT) [cn-pdf, pdf, other]

Title: A Category Theoretic Approach to Approximate Game Theory Show Chinese title

Title: 范畴论方法在近似博弈论中的应用

Neil Ghani (MSP Group, University of Strathclyde)

Comments: In Proceedings ACT 2024, arXiv:2509.18357

Journal-ref: EPTCS 429, 2025, pp. 190-202

Subjects: Computer Science and Game Theory (cs.GT) ; Logic in Computer Science (cs.LO) ; Multiagent Systems (cs.MA) ; Symbolic Computation (cs.SC)

This paper uses category theory to develop an entirely new approach to approximate game theory. Game theory is the study of how different agents within a multi-agent system take decisions. At its core, game theory asks what an optimal decision is in a given scenario. Thus approximate game theory asks what is an approximately optimal decision in a given scenario. This is important in practice as -- just like in much of computing -- exact answers maybe too difficult to compute or even impossible to compute given inherent uncertainty in input. We consider first "Selection Functions" which are functions and develop a simple yet robust model of approximate equilibria. We develop the algebraic properties of approximation wrt selection functions and also relate approximation to the compositional structure of selection functions. We then repeat this process successfully for Open Games -- a more advanced model of game theory. Show Chinese abstract

本文使用范畴论来开发一种全新的近似博弈论方法。 博弈论是研究多智能体系统中不同代理如何做出决策的学科。 其核心是询问在给定情况下什么是最佳决策。 因此，近似博弈论询问在给定情况下什么是近似最佳决策。 这在实践中很重要，因为——就像计算中的许多情况一样——精确答案可能难以计算甚至在输入固有的不确定性下无法计算。 我们首先考虑“选择函数”，这些函数发展了一个简单而稳健的近似均衡模型。 我们开发了相对于选择函数的近似代数性质，并将近似与选择函数的组合结构相关联。 然后我们成功地对开放博弈进行了同样的过程——这是一个更高级的博弈论模型。

Replacement submissions (showing 7 of 7 entries )

[6] arXiv:2412.20432 (replaced) [cn-pdf, pdf, html, other]

Title: Relative Constructibility via Generalised Sequential Algorithms Show Chinese title

Title: 通过广义顺序算法的相对可构造性

Desmond Lau

Comments: 47 pages, 3 tables. An error was found in the motivating example concerning abstract state machines. In light of this, the first section was reworked and our results reframed

Subjects: Logic in Computer Science (cs.LO)

We modify Gurevich's definition of sequential algorithms, so that it becomes amenable to computation with arbitrarily large sets on a sufficiently intuitive level. As a result, two classes of abstract algorithms are obtained, namely generalised sequential algorithms (GSeqAs) and generalised sequential algorithms with parameters (GSeqAPs). We derive from each class a relative computability relation on sets which is analogous to the Turing reducibility relation on reals. We then prove that the relative computability relation derived from GSeqAPs is equivalent to the relative constructibility relation in set theory. Show Chinese abstract

我们修改了Gurevich对顺序算法的定义，使其能够在足够直观的层面上与任意大的集合进行计算。 结果得到了两类抽象算法，即广义顺序算法（GSeqAs）和带参数的广义顺序算法（GSeqAPs）。 我们从每一类中推导出一个集合上的相对可计算关系，该关系类似于实数上的图灵可归约关系。 然后我们证明从GSeqAPs推导出的相对可计算关系等价于集合论中的相对构造关系。

[7] arXiv:2303.05623 (replaced) [cn-pdf, pdf, other]

Title: Relating homotopy equivalences to conservativity in dependent type theories with computation axioms Show Chinese title

Title: 将同伦等价与依赖类型理论中的保守性相关联，带有计算公理

Matteo Spadetto

Subjects: Logic (math.LO) ; Logic in Computer Science (cs.LO) ; Category Theory (math.CT)

We prove a conservativity result for extensional type theories over propositional ones, i.e. dependent type theories with propositional computation rules, or computation axioms, using insights from homotopy type theory. The argument exploits a notion of canonical homotopy equivalence between contexts, and uses the notion of a category with attributes to phrase the semantics of theories of dependent types. Informally, our main result asserts that, for judgements essentially concerning h-sets, reasoning with extensional or propositional type theories is equivalent. Show Chinese abstract

我们证明了关于扩展类型理论相对于命题类型理论的保守性结果，即使用同伦类型理论的见解，依赖类型理论具有命题计算规则或计算公理。该论证利用了上下文之间规范同伦等价的概念，并使用带有属性的范畴来表述依赖类型理论的语义。非正式地，我们的主要结果断言，对于基本上涉及h-集的判断，使用扩展类型理论或命题类型理论进行推理是等价的。

[8] arXiv:2403.19884 (replaced) [cn-pdf, pdf, other]

Title: Representing Knowledge and Querying Data using Double-Functorial Semantics Show Chinese title

Title: 使用双函子语义表示知识和查询数据

Michael Lambert (University of Massachusetts-Boston), Evan Patterson (Topos Institute)

Comments: In Proceedings ACT 2024, arXiv:2509.18357

Journal-ref: EPTCS 429, 2025, pp. 174-189

Subjects: Category Theory (math.CT) ; Databases (cs.DB) ; Logic in Computer Science (cs.LO)

Category theory offers a mathematical foundation for knowledge representation and database systems. Popular existing approaches model a database instance as a functor into the category of sets and functions, or as a 2-functor into the 2-category of sets, relations, and implications. The functional and relational models are unified by double functors into the double category of sets, functions, relations, and implications. In an accessible, example-driven style, we show that the abstract structure of a 'double category of relations' is a flexible and expressive language in which to represent knowledge, and we show how queries on data in the spirit of Codd's relational algebra are captured by double-functorial semantics. Show Chinese abstract

范畴论为知识表示和数据库系统提供了数学基础。 现有的流行方法将数据库实例建模为到集合和函数范畴的函子，或者作为到集合、关系和蕴含的2-范畴的2-函子。 函数模型和关系模型通过到集合、函数、关系和蕴含的双范畴的双函子得到统一。 以一种易于理解、示例驱动的方式，我们表明“关系双范畴”的抽象结构是一种灵活且富有表现力的语言，可用于表示知识，并展示了如何通过双函子语义来捕捉类似Codd关系代数的数据查询。

[9] arXiv:2410.00675 (replaced) [cn-pdf, pdf, other]

Title: Fibrational Perspectives on Determinization of Finite-State Automata Show Chinese title

Title: 有限状态自动机确定化的纤维视角

Thea Li

Comments: In Proceedings ACT 2024, arXiv:2509.18357

Journal-ref: EPTCS 429, 2025, pp. 203-216

Subjects: Category Theory (math.CT) ; Formal Languages and Automata Theory (cs.FL) ; Logic in Computer Science (cs.LO)

Colcombet and Petri\c{s}an argued that automata may be usefully considered from a functorial perspective, introducing a general notion of "V-automaton" based on functors into V. This enables them to recover different standard notions of automata by choosing V appropriately, and they further analyzed the determinization for Rel-automata using the Kleisli adjunction between Set and Rel. In this paper, we revisit Colcombet and Petri\c{s}an's analysis from a fibrational perspective, building on Melli\`es and Zeilberger's recent alternative but related definition of categorical automata as functors satisfying the finitary fiber and unique lifting of factorizations property. In doing so, we improve the understanding of determinization in three regards: Firstly, we carefully describe the universal property of determinization in terms of forward-backward simulations. Secondly, we generalize the determinization procedure for Rel automata using a local adjunction between SpanSet and Rel, which provides us with a canonical forward simulation. Finally, we also propose an alternative determinization based on the multiset relative adjunction which retains paths, and we leverage this to provide a canonical forward-backward simulation. Show Chinese abstract

科姆博贝特和佩特里桑认为，从函子的角度来看，自动机可能被有益地考虑，他们引入了一个基于进入V的函子的“V-自动机”的一般概念。这使他们能够通过适当选择V来恢复不同的标准自动机概念，并且他们进一步利用Set和Rel之间的Kleisli伴随关系分析了Rel-自动机的确定化。 在本文中，我们从纤维化视角重新审视科姆布贝特和佩特里桑的分析，基于梅利埃和泽尔伯格最近提出的另一种但相关的范畴自动机定义，即满足有限纤维和因子分解唯一提升性质的函子。 在此过程中，我们在三个方面改进了对确定化的理解： 首先，我们仔细描述了确定化的普遍性质，涉及前向后向模拟。 其次，我们使用SpanSet和Rel之间的局部伴随关系，对Rel自动机的确定化过程进行了推广，这为我们提供了一个规范的前向模拟。 最后，我们还提出了一种基于多重集相对伴随关系的替代确定化方法，该方法保留路径，并利用这一点提供了一个规范的前向后向模拟。

[10] arXiv:2411.12840 (replaced) [cn-pdf, pdf, other]

Title: The Aldous$\unicode{x2013}$Hoover Theorem in Categorical Probability Show Chinese title

Title: Aldous$\unicode{x2013}$Hoover 定理在范畴概率中

Leihao Chen, Tobias Fritz, Tomáš Gonda, Andreas Klingler, Antonio Lorenzin

Comments: 39 pages, v2: minor changes per referees' suggestions

Subjects: Statistics Theory (math.ST) ; Logic in Computer Science (cs.LO) ; Category Theory (math.CT) ; Probability (math.PR)

The Aldous-Hoover Theorem concerns an infinite matrix of random variables whose distribution is invariant under finite permutations of rows and columns. It states that, up to equality in distribution, each random variable in the matrix can be expressed as a function only depending on four key variables: one common to the entire matrix, one that encodes information about its row, one that encodes information about its column, and a fourth one specific to the matrix entry. We state and prove the theorem within a category-theoretic approach to probability, namely the theory of Markov categories. This makes the proof more transparent and intuitive when compared to measure-theoretic ones. A key role is played by a newly identified categorical property, the Cauchy--Schwarz axiom, which also facilitates a new synthetic de Finetti Theorem. We further provide a variant of our proof using the ordered Markov property and the d-separation criterion, both generalized from Bayesian networks to Markov categories. We expect that this approach will facilitate a systematic development of more complex results in the future, such as categorical approaches to hierarchical exchangeability. Show Chinese abstract

阿洛斯-霍弗定理涉及一个随机变量的无限矩阵，其分布在行和列的有限排列下是不变的。 它指出，除了分布相等外，矩阵中的每个随机变量都可以表示为仅依赖于四个关键变量的函数：一个适用于整个矩阵的变量，一个编码其行信息的变量，一个编码其列信息的变量，以及一个特定于矩阵条目的变量。 我们在概率的范畴论方法中陈述并证明了该定理，即马尔可夫范畴理论。 与测度论方法相比，这使证明更加透明和直观。 一个关键作用是由新识别的范畴性质——柯西-施瓦茨公理所扮演，这也促进了新的合成德芬尼定理。 我们进一步提供了一种使用有序马尔可夫性质和d-分离准则的证明变体，这两者都从贝叶斯网络推广到了马尔可夫范畴。 我们预计这种方法将有助于未来更复杂结果的系统发展，例如分层可交换性的范畴方法。

[11] arXiv:2509.01728 (replaced) [cn-pdf, pdf, html, other]

Title: Constrained Decoding for Robotics Foundation Models Show Chinese title

Title: 约束解码用于机器人基础模型

Parv Kapoor, Akila Ganlath, Changliu Liu, Sebastian Scherer, Eunsuk Kang

Subjects: Robotics (cs.RO) ; Machine Learning (cs.LG) ; Logic in Computer Science (cs.LO)

Recent advances in the development of robotic foundation models have led to promising end-to-end and general-purpose capabilities in robotic systems. These models are pretrained on vast datasets of robot trajectories to process multi-modal inputs and directly output a sequence of action that the system then executes in the real world. Although this approach is attractive from the perspective of improved generalization across diverse tasks, these models are still data-driven and, therefore, lack explicit notions of behavioral correctness and safety constraints. We address these limitations by introducing a constrained decoding framework for robotics foundation models that enforces logical constraints on action trajectories in dynamical systems. Our method ensures that generated actions provably satisfy signal temporal logic (STL) specifications at runtime without retraining, while remaining agnostic of the underlying foundation model. We perform comprehensive evaluation of our approach across state-of-the-art navigation foundation models and we show that our decoding-time interventions are useful not only for filtering unsafe actions but also for conditional action-generation. Videos available on our website: https://constrained-robot-fms.github.io Show Chinese abstract

最近在机器人基础模型开发方面的进展，使得机器人系统在端到端和通用能力方面表现出良好的前景。 这些模型在大量机器人轨迹数据集上进行预训练，以处理多模态输入，并直接输出系统在现实世界中执行的动作序列。 尽管从跨不同任务的改进泛化角度来看，这种方法具有吸引力，但这些模型仍然是数据驱动的，因此缺乏行为正确性和安全约束的显式概念。 我们通过为机器人基础模型引入一个受约束的解码框架来解决这些限制，该框架在动态系统中对动作轨迹施加逻辑约束。 我们的方法确保生成的动作在运行时可证明满足信号时间逻辑（STL）规范，而无需重新训练，同时对底层基础模型保持无关性。 我们在最先进的导航基础模型上进行了全面评估，并表明我们的解码时干预不仅有助于过滤不安全动作，还有助于条件动作生成。 视频可在我们的网站上观看：https://constrained-robot-fms.github.io

[12] arXiv:2509.17774 (replaced) [cn-pdf, pdf, html, other]

Title: Efficient & Correct Predictive Equivalence for Decision Trees Show Chinese title

Title: 高效且正确的决策树预测等价性

Joao Marques-Silva, Alexey Ignatiev

Subjects: Artificial Intelligence (cs.AI) ; Machine Learning (cs.LG) ; Logic in Computer Science (cs.LO)

The Rashomon set of decision trees (DTs) finds importance uses. Recent work showed that DTs computing the same classification function, i.e. predictive equivalent DTs, can represent a significant fraction of the Rashomon set. Such redundancy is undesirable. For example, feature importance based on the Rashomon set becomes inaccurate due the existence of predictive equivalent DTs, i.e. DTs with the same prediction for every possible input. In recent work, McTavish et al. proposed solutions for several computational problems related with DTs, including that of deciding predictive equivalent DTs. This approach, which this paper refers to as MBDSR, consists of applying the well-known method of Quine-McCluskey (QM) for obtaining minimum-size DNF (disjunctive normal form) representations of DTs, which are then used for comparing DTs for predictive equivalence. Furthermore, the minimum-size DNF representation was also applied to computing explanations for the predictions made by DTs, and to finding predictions in the presence of missing data. However, the problem of formula minimization is hard for the second level of the polynomial hierarchy, and the QM method may exhibit worst-case exponential running time and space. This paper first demonstrates that there exist decision trees that trigger the worst-case exponential running time and space of the QM method. Second, the paper shows that, depending on the QM method implementation, the MBDSR approach can produce incorrect results for the problem of deciding predictive equivalence. Third, the paper shows that any of the problems to which the smallest DNF representation has been applied to can be solved in polynomial time, in the size of the DT. The experiments confirm that, for DTs for which the worst-case of the QM method is triggered, the algorithms proposed in this paper are orders of magnitude faster than the ones proposed by McTavish et al. Show Chinese abstract

决策树（DTs）的Rashomon集有重要的应用。最近的工作表明，计算相同分类函数的DTs，即预测等价的DTs，可以代表Rashomon集的一个显著部分。这种冗余是不希望的。例如，基于Rashomon集的特征重要性会因为预测等价DTs的存在而不准确，即DTs对于每个可能的输入都有相同的预测。在最近的工作中，McTavish等人提出了与DTs相关的几个计算问题的解决方案，包括判断预测等价DTs的问题。这种方法，本文称为MBDSR，包括应用著名的Quine-McCluskey（QM）方法来获得DTs的最小大小DNF（析取范式）表示，然后用于比较DTs的预测等价性。此外，最小大小的DNF表示还被用于计算DTs做出的预测的解释，并在存在缺失数据的情况下找到预测。然而，公式最小化问题对于多项式层次结构的第二层来说是困难的，QM方法可能会表现出最坏情况下的指数运行时间和空间。本文首先证明存在触发QM方法最坏情况指数运行时间和空间的决策树。其次，本文显示，根据QM方法的实现方式，MBDSR方法在判断预测等价性问题上可能会产生错误的结果。第三，本文显示，任何已应用最小DNF表示的问题都可以在DT大小的多项式时间内解决。实验确认，对于触发QM方法最坏情况的DTs，本文提出的算法比McTavish等人提出的算法快几个数量级。