首页/论文/1412.3271

arXiv 1412.32712014-12-10cs.LO

非终止性的二阶表述

A Second-Order Formulation of Non-Termination

Fred Mesnard, Etienne Payet

备注：: 8 pages

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们考虑一类循环的终止/非终止性质。这样的循环是真实程序片段的常用抽象。二阶逻辑是表达非终止性的一种方便的语言。当然，这种性质一般是不可判定的。然而，通过将语言限制在已知的可判定的情况下，我们展示了新的循环类，其非终止性是可判定的。我们举了很多例子。

英文摘要：

We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is generally undecidable. However, by restricting the language to known decidable cases, we exhibit new classes of loops, the non-termination of which is decidable. We present a bunch of examples.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

依赖选择作为终止原则

Dependent choice as a termination principle

我们引入了一个新的配方的公理依赖的选择，可以被看作是一个抽象的终止原则，概括的递归路径排序用于建立终止重写系统。我们认为我们的终止原理的几个变种，并将它们与文献中的一般终止定理。

2019-02-25cs.LOmath.LO

位向量程序的无限制终止性和非终止性变元

Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs

证明程序终止通常通过为程序状态找到有充分根据的排名函数来完成。现有的终止证明器通常使用线性代数或模板来找到排名函数。因此，他们经常被限制在寻找数学整数上的线性排名函数。这类函数不足以证明许多终止程序的终止性，此外，对于数学整数操作的程序的终止参数并不总是导致对于固定宽度机器整数操作的同一程序的终止参数。我们提出了一个终止分析能够产生非线性，字典排序功能和非线性递归集是正确的固定宽度的机器算术和浮点运算我们的技术是基于减少从程序\emph{termination}二阶\emph{satisfaction}。我们提供了配方的终止和非终止在一个片段的二阶逻辑有限域上可判定的限制量化。由此产生的技术是一个健全的和完整的分析有限状态程序的终止固定宽度的整数和IEEE浮点运算。

2014-10-19cs.LO

二阶计算规则的模块化终止性及其在代数效应处理器中的应用

Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers

提出一种基于语义标注翻译和Blanqui一般模式的模块化终止性证明方法，实现为工具SOL，并成功应用于证明带代数效应处理器的调用-按-值演算变体的终止性。

2022-06-13cs.LOcs.SC

多态高阶终止

Polymorphic Higher-order Termination

我们概括的终止方法的高阶多项式的解释与impredicative多态性的设置。而不是使用弱单调泛函，我们解释的条款在一个适当的扩展系统F-Ω。这使得重写规则的直接解释成为可能，而重写规则基本上使用了非谓词多态性。此外，我们的概括简化了非多态设置的方法的适用性，允许编码的归纳数据类型。作为我们的方法的潜力的一个例子，我们证明了一个完整的直觉二阶命题逻辑置换转换的实质性片段的终止。

2019-04-22cs.LO

一个几乎确定终止概率和恶魔程序的新规则

A new rule for almost-certain termination of probabilistic- and demonic programs

扩展我们自己和其他人的早期方法来推理概率程序的终止，我们提出并证明了一个新的规则终止概率为1，也被称为“几乎确定终止”。该规则同时使用（非严格）超鞅和进步保证，并且它似乎涵盖了早期方法没有的重要情况。特别是，它足以终止无界对称随机游走在一个和两个维度：对于第一个，我们给出了一个证明;对于第二个，我们使用福斯特定理来证明存在。支持非决定论（即恶魔选择）;但我们目前仅限于离散分布。

2017-01-06cs.LO

具有非线性约束的线性规划的终止性

Termination of Linear Programs with Nonlinear Constraints

Tiwari通过Jordan形式和特征向量计算证明了实数上线性规划（具有线性循环条件和更新的循环）的终止性是可判定的。布雷弗曼证明了它在整数上也是可判定的。本文研究了实数和整数上具有多项式循环条件和线性更新的循环的终止性。首先，我们证明了这种循环的终止整数是不可判定的。其次，在一个假设条件下，我们给出了一个完整的算法来判定一类实数上的此类规划的终止性。我们的方法在精神上类似于蒂瓦里，但使用不同的技术。最后，我们通过构造一个循环，将线性规划的终止性问题归结为另一个与数论和遍历理论有关的判定问题，并猜想其不可判定，从而推测了实数上具有多项式循环条件的线性规划的终止性一般是不可判定的.

2009-04-23cs.LO

更多相关论文收起更多论文

高阶重写系统的终止与合流

Termination and Confluence of Higher-Order Rewrite Systems

在过去的20年里，已经提出了几种高阶重写方法，其中包括Klop的组合重写系统（CRS），Nipkow的高阶重写系统（HRS）以及Jouannaud和Okada的高阶代数规约语言，其中只有最后一种考虑了类型化项。Jouannaud、Okada和本文作者将后一种方法推广到归纳数据类型系统（IDTS）。在本文中，我们扩展了IDTS与CRS高阶模式匹配机制，导致简单类型的CRS。然后，我们展示了如何终止标准开发的IDTS与一阶模式匹配，称为一般模式，可以扩展，以证明强规范化的IDTS与高阶模式匹配。接下来，我们将统一的方法与HRS进行比较。我们首先证明了扩展的一般模式也可以适用于人力资源系统。其次，我们展示了如何Nipkow的高阶临界对分析技术证明当地的融合可以应用于IDTS。

2006-10-11cs.LO

二阶命题可满足性

Second-Order Propositional Satisfiability

从根本上说，每个静态程序分析器都是通过提供候选解决方案的算法和候选验证技术的组合来搜索证明。从本质上讲，启发式将二阶问题简化为一阶/命题问题，而验证通常只是对SAT/SMT求解器的调用。这导致了这种分析的整体设计，将问题的制定与解决过程混为一谈。因此，后者的任何变化都会导致整个分析的变化。这种设计是由求解器技术的最新发展水平决定的。虽然SAT/SMT求解器已经取得了巨大的进步，但几乎没有任何二阶求解器。本文采取了一个步骤来解决这种情况，提出了一个可判定的片段的二阶逻辑，仍然是足够的表达，以捕捉众多的程序分析问题（如安全证明，错误发现，终止和非终止证明，超优化）。我们把这个片段的可满足性问题称为二阶SAT，并证明它是NEXPTIME完全的。最后，我们建立了一个基于程序合成的二阶SAT的决策过程，并提出了实验证据表明，我们的方法是易于处理的程序分析问题。

2015-01-17cs.LO

用算术分析逻辑程序的非终止性

Non-termination Analysis of Logic Programs with Integer arithmetics

在过去的几年中，分析器已被引入到检测类的非终止查询的明确的逻辑程序。虽然这些非终止性分析器已经被证明是相当精确的，但它们在现实生活中的Prolog程序上的适用性是有限的，因为大多数Prolog程序使用非逻辑功能。作为分析Prolog程序的第一步，本文给出了含整数运算的逻辑程序的不可终止条件。该分析仪基于我们在ICLP 2009上展示的非终止分析仪。分析从一类查询开始，并推断出一个子类的非终止的。在第一阶段，我们忽略算术运算的结果（成功或失败），假设所有算术调用都成功。在第二阶段中，我们成功的算术调用的特点作为一个约束问题，其解决方案确定的非终止查询。

2011-09-15cs.LOcs.PL

非简化图重写终止

Non-simplifying Graph Rewriting Termination

LORIA（洛林信息学及其应用研究实验室）；Université de Lorraine（洛林大学）；Inria Nancy Grand-Est（法国国家信息与自动化研究所南锡大东部中心）

到目前为止，自然语言处理（NLP）中的大量工作依赖于树作为核心数学结构来表示语言信息（例如Chomsky的工作）。然而，有些语言现象并不能很好地处理树。在以前的论文中，我们展示了用图来编码语言结构和使用图重写规则来计算这些结构的好处。出于一些语言学上的考虑，图重写的特征在于两个特征：第一，沿着计算没有节点创建，第二，有非局部边修改。在这些假设下，我们证明了一致终止是不可判定的，非一致终止是可判定的。我们描述了两个终止技术的基础上的重量，我们给这些重写系统的推导长度的复杂性界。

2013-02-26cs.CCcs.CLcs.LO

二维约束循环问题是可判定的

The 2-Dimensional Constraint Loop Problem is Decidable

本文证明二维实数域上由线性约束合取定义的循环终止（等价于相应二元关系的良基性）问题可判定。

2024-04-26cs.LO

仿射概率规划定性和定量终止问题的数学分析

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

本文研究了实变量概率规划的终止性问题。有关问题是：1.定性问题，询问（i）程序是否以概率1终止（几乎肯定终止）和（ii）预期终止时间是否有限（有限终止）; 2.定量问题，要求（i）近似预期的终止时间（期望问题）和（ii）计算边界B，使得在B步后终止的概率呈指数下降（浓度问题）。为了解决这些问题，我们利用排序上鞅的概念，这是一个强大的方法来证明概率程序的终止性。详细地说，我们专注于算法合成的线性排名上鞅仿射概率程序（APP）与天使和恶魔的非决定性。APP的一个重要子类是LRAPP，它被定义为所有APP的类，其上存在线性秩上鞅。我们的主要贡献如下。首先，我们证明了LRAPP的成员问题（i）可以决定在多项式时间的APP的最恶魔的非确定性，和（ii）是NP-困难的，在PSPACE的APP的天使的非确定性;此外，NP-困难的结果已经成立APP的没有概率和恶魔的非确定性。其次，我们证明了LRAPP的浓度问题可以解决在相同的复杂性LRAPP的成员问题。最后，我们证明了LRAPP上的期望问题可以在2 EXPTIME中求解，并且即使对于没有概率和非确定性的APP也是PSPACE困难的（即，确定性程序）。我们的实验结果表明，我们的方法来回答定性和定量的问题在APP的最恶魔的非决定论的有效性。

2015-10-28cs.LOcs.PL

使用程序合成进行程序分析

Using Program Synthesis for Program Analysis

在本文中，我们确定了一个片段的二阶逻辑与限制量化，是表现力足以捕捉众多的静态分析问题（如安全证明，错误发现，终止和非终止证明，超优化）。我们将该片段称为{ \it合成片段}。合成片段中公式的可满足性在有限域上是可判定的;具体地说，判定问题是NEXPTIME完全的。如果这个片段中的公式是可满足的，则解由从二阶变量到\emph{functions over finite domains}的满足赋值组成。为了具体地找到这些解决方案，我们合成了计算函数的\emph{programs}。我们的程序合成算法对于有限状态程序是完全的，即有限域上的每个\emph{function}都是由我们可以合成的\emph{program}计算的。因此，我们可以使用我们的合成器作为二阶逻辑合成片段的决策过程，这反过来又允许我们使用它作为许多程序分析任务的强大后端。为了显示我们的方法的易处理性，我们评估了几个静态分析问题的程序合成器。

2015-08-31cs.LOcs.PL

近线性递推序列的正性

Positivity of Second-Order Nearly Linearly Recurrent Sequences

CNRS, IRIF, Université Paris Cité（法国国家科学研究中心，IRIF实验室，巴黎西岱大学）；Department of Computer Science, University of Oxford（牛津大学计算机科学系）

本文研究了近线性递推序列的正性问题，提出了一种二阶递推关系的决策方法，并利用新的超越结果证明了该方法的终止性。

2026-09-24cs.LOmath.DS