Probabilistic Recursion Theory and Implicit Computational Complexity (Long Version)
我们表明，概率可计算的功能，即，输出分布并由概率图灵机计算的那些函数可以由Church和Kleene的部分递归函数的自然推广来表征。得到的代数，以下Leivant，可以限制，以捕捉多时间采样分布的概念，在平均情况下的复杂性和密码学的一个关键概念。
2014-06-25 cs.LO
The Power of Non-Determinism in Higher-Order Implicit Complexity
我们研究了高阶类型的纯函数式程序设计语言中的非确定性的力量。具体来说，我们考虑不同的数据顺序，配备明确的非确定性选择的无缺点的程序。Cons-freeness大致意味着数据构造函数不能出现在函数体中，因此所有对存储空间的操作都必须使用调用堆栈间接发生。虽然无缺点的程序以前已经被一些作者用来计算复杂性类，但非确定性程序的工作几乎只考虑数据阶为0的程序。以前的工作已经表明，添加明确的非确定性的无缺点的程序，以0的顺序数据不增加表达能力，我们证明，这是显着的情况下，更高的数据顺序：添加非确定性的程序，数据顺序至少为1允许整个类的特征的基本时间可判定集。最后，我们将展示如何，即使是非确定性的选择，原来的层次结构的特征恢复施加不同的限制。
2017-01-30 cs.CC cs.LO
Probabilistic Complexity Classes through Semantics
在最近的一篇论文中，作者展示了如何使用线性逻辑的交互图模型来获得非确定性复杂性类的隐式特征。在本文中，我们将展示如何使用这种语义方法来隐式复杂性理论（ICC），以确定性和概率模型的计算。在这样做的时候，我们得到组行动和确定性和概率层次结构的复杂性类之间的对应关系。作为一种特殊情况，我们给出了类PLogspace（无界误差概率对数空间）和PPtime（无界误差概率多项式时间）的第一个隐式特征
2020-01-31 cs.CC cs.LO math.DS
On Quasi-Interpretations, Blind Abstractions and Implicit Complexity
准解释是一种保证一阶函数程序复杂性界限的技术：通过终止排序，它们给出了一个程序在多项式时间内可执行的充分条件，这里称为P-准则。为了更好地理解程序的内涵表达能力，我们研究了满足P-准则的程序的性质。给定一个二进制列表上的程序，它的盲抽象是通过将列表替换为它们的长度（自然数）而获得的不确定性程序。如果一个程序的盲抽象在多项式时间内终止，则该程序是盲多项式的。我们表明，所有的程序满足的P-准则的变种，实际上是盲目的多项式。然后，我们给出了两个扩展的P-准则：一个通过放松的终止序条件，和其他一个（有界值属性）给出了一个必要和充分条件的程序是多项式时间可执行的，与memoisation。
2006-08-06 cs.CC cs.LO cs.PL
Proceedings 8th Workshop on Developments in Implicit Computational Complexity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis
DICE研讨会探讨了隐式计算复杂性（ICC）领域，该领域源于使用逻辑和形式化方法为复杂性有限计算（例如Ptime，Logspace计算）提供语言的几个建议。它旨在研究程序的计算复杂性，而不涉及外部测量条件或特定的机器模型，而只考虑语言限制或逻辑/计算原则带来的复杂性属性。FOPARA研讨会作为一个论坛，介绍与计算机程序的资源（如时间、空间、能源）消耗分析有关的原创研究成果。该研讨会旨在将研究基础问题的研究人员与更注重实际结果的研究人员聚集在一起。因此，鼓励在理论和实践方面作出贡献。我们还鼓励理论与实践相结合的论文。鉴于这两个社区之间的互补性和协同作用，以及在ETAPS 2015期间在伦敦共同举办DICE-FOPARA 2015的成功经验，我们将在瑞典乌普萨拉举行的ETAPS 2017上共同举办这两个研讨会。所提供的会议记录收集了研讨会上接受的论文。
2017-04-18 cs.CC cs.LO cs.PL
Cyclic Implicit Complexity
本文将循环证明与隐式计算复杂性结合，提出基于Bellantoni-Cook安全—正规函数代数的循环证明系统，并以证明论约束刻画多项式时间与初等可计算函数。
2025-08-29 cs.LO math.LO
Towards a Complexity-through-Realisability Theory
我们解释了如何在线性逻辑的可实现性模型领域的最新发展-或互动的几何-和隐式计算复杂性可以导致一个新的方法隐式计算复杂性。这种基于语义的方法应统一适用于各种计算范式，并使新的数学方法和工具的使用，以解决问题的计算复杂性。本文提供了背景，动机和前景的复杂性通过可实现性理论的发展，并说明了它与最近的结果。
2015-07-02 cs.CC cs.LO math.LO
A Novel Loop Fission Technique Inspired by Implicit Computational Complexity
本文探讨了隐式计算复杂性（ICC）在命令式程序中并行化循环的一个意想不到的应用。由于轻量级的依赖关系分析，我们的算法允许将一个循环分成多个可以并行运行的循环，从而在执行时间方面获得收益，这与最先进的自动并行化工具（当两者都适用时）相似。我们的基于图的算法是直观的，语言不可知的，被证明是正确的，并适用于所有类型的循环，即使他们的循环迭代空间是未知的静态或在编译时，如果他们不是在规范形式或如果他们包含循环进行依赖。作为贡献，我们提供的计算技术，证明其保留的语义正确性，和实验结果，以量化预期的性能收益。我们的基准测试也表明，该技术可以无缝集成到编译器通行证或其他自动并行套件。我们断言，这种原始的和自动化的循环变换方法是由于ICC提供的“正交”方法而发现的。
2022-05-18 cs.LO cs.PL
mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
隐式计算复杂性（ICC）推动了对复杂性类的更好理解，但它也指导了资源感知语言和静态源代码分析器的开发。在开发的方法中，mwp流分析证明多项式的界限上的大小操纵的值的一个命令式程序。这个结果是通过限制状态之间的转换而不是像大多数静态分析器那样孤立地关注状态来获得的，并且不关心值的终止或严格边界。这些差异，以及其内置的组合性，使mwp流分析一个很好的目标，以确定如何ICC启发的技术与更传统的静态分析方法相比，分歧。本文的贡献是三方面的：我们微调的内部机械的原始分析，使其易于处理的实践中，我们扩展的分析，函数调用，并利用其机械计算的分析结果有效地，我们实现了作为一个轻量级的工具，自动执行C程序的数据大小分析的结果。这种记录的努力准备和认证的复杂性分析的发展，通过将昂贵的分析转化为一个易于处理的程序，进一步解相关的问题，如果一个边界存在的问题，计算它。
2022-03-08 cs.FL cs.LO math.LO
Implicit definability of truth constants in Łukasiewicz logic
本文在命题逻辑的框架下，引入了一个合适的隐式可定义性概念，该概念适合于预定的实值语义，并涉及其域的元素。探讨了标准语义学中隐式定义每个理性元素的几种变体，并在此基础上得到了RationalPavelka逻辑中的理论在RationalPavelka逻辑中的忠实解释。其中一些结果已经在哈耶克的《模糊逻辑的元数学》中作为技术陈述提出。一个连接到缺乏（演绎）Beth属性在Eschukasiewicz逻辑。此外，虽然标准语义学的无理元素不能用有限的方法隐式地定义，但它们在无限的Rukasiewicz逻辑中的平行发展是可能的。作为一个应用程序的可定义性的理性，它显示了如何计算复杂性的结果，理性Pavelka逻辑可以得到类似的结果为Rankukasiewicz逻辑。可定义性概念本身的复杂性也进行了研究。最后，我们回顾了这些结果对于模糊逻辑的精确性/精确性讨论的重要性，以及对于真值常数在Eukasiewicz逻辑中的一般地位的重要性。
2018-02-23 cs.LO math.LO
Quantitative Coding and Complexity Theory of Continuous Data
解决计算问题需要固定输入和输出的编码：将图形编码为邻接矩阵，将字符编码为整数，将整数编码为位串，反之亦然。对于这样的离散数据，实际的编码通常是直接的和/或复杂的-理论上是不重要的（比如说，直到多项式时间）;但是对于连续数据，实数已经自然地提出了各种编码（所谓的代表）具有非常不同的属性，范围从可计算的“不合理的”二进制扩展，通过定性多项式，甚至线性复杂性-理论上“合理的”签署，数字扩展但是，如何区分微积分和数值中常见的其他空间（如Sobolev）的不合适的编码？关于定性的可计算性，Kreitz和Weihrauch（1985）已经将可容许性确定为无限二元序列在康托空间上的表示是“合理的”的关键标准。[doi：10.1007/11780342_48]。将拓扑空间上的可计算性细化为度量空间上的复杂性，发展了多项式/线性可容许性理论，作为定性可容许性的两个定量细化。我们还将数量容许性重新表述为表示及其集值逆的数量连续性，后者采用了[doi：10.4115/jla.2013.5.7]多函数的“序列”连续性的新概念。通过建立紧超度量空间之间的集值函数的定量连续选择定理，我们可以将上述定量主定理从函数推广到集值函数，也就是搜索问题。更高类型的复杂性是通过将Cantor（和Baire）的基空间编码推广到其他（紧凑）ULRA度量空间来捕获的。
2021-08-24 cs.IT cs.LO math.IT
A generic imperative language for polynomial time
隐式计算复杂性中的派生方法与函数式编程有关，但考虑到命令式编程的更广泛的算法适用性，将其适用于通用命令式编程是非常可取的。我们介绍了一种新的方法，衍生，除其他好处外，很容易适应完全通用的命令式编程。新颖之处在于分歧有限的二阶对象，即有限的结构，而不是分歧自由代数的元素。在此过程中，我们在隐式复杂性的可行性类型论特征和静态分析的数据流方法之间架起了桥梁。
2020-02-19 cs.CC cs.LO cs.PL
A characterization of functions over the integers computable in polynomial time using discrete differential equations
本文研究了离散常微分方程（ODEs）的表达能力和计算能力。（普通）差分方程。它提出了一个新的框架，使用这些方程作为计算和算法设计的中心工具。我们提出了一般理论的离散常微分方程的计算理论，我们说明了这与各种算法的例子，我们提供了几个隐式的复杂性和可计算性类的特征。该框架提出了一个原始的复杂性和计算类的观点。它统一了几个结构，已经提出了表征这些类，包括经典的方法在隐式复杂性使用限制递归计划，以及最近的可计算性和复杂性的连续常微分方程类的表征。它还有助于理解模拟计算与计算理论的经典离散模型之间的关系。从更技术的角度来看，本文指出了线性（离散）ODE和经典ODE工具的基本作用，如变量的变化，以捕获可计算性和复杂性的措施，或作为编程的工具，许多算法。
2022-09-25 cs.CC cs.DM cs.LO
Interaction Graphs: Nondeterministic Automata
本文给出了次线性非确定复杂性类的一系列语义刻画。这些结果属于复杂性理论和所谓的隐式计算复杂性（ICC）的基于逻辑的方法的一般域，即不参考特定的机器模型的复杂性类的描述。特别是，它与ICC的线性逻辑的基础上的结果，因为考虑的语义框架源于后者的工作。此外，所获得的特征具有几何性质：每个类都由群的特定作用通过保测度映射来表征。
2016-09-26 cs.CC cs.LO math.LO
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
本文研究定量可达性博弈中SPE的复杂性，证明约束存在性问题是PSPACE完全的，并提出一种通过迭代约束至不动点来刻画SPE结果集的新算法。
2020-11-04 cs.GT cs.LO
Typed lambda-calculi and superclasses of regular functions
我们建议在类型化的布尔代数演算中使用Church编码作为隐式计算复杂性的自动机理论对应物的基础，就像一元二阶逻辑提供了描述复杂性的对应物一样。具体来说，我们研究转换，即串到串（或树到树）函数-特别是那些具有超线性增长的函数，如多正则函数，HDT 0 L转换和Sénizergues的“k-可计算映射”。我们对这一目标的第一个结果包括显示列入一些转导类在某些类定义的Alzoda-calculi。特别是，这揭示了一个基本的开放式问题的表现力的简单类型的Alzida演算。我们还编码正规函数（并通过改变考虑的程序类型，我们得到一个更大的子类的多正则函数）在基本仿射代数演算，一个变量的线性逻辑最初设计的隐式计算复杂性。
2019-06-30 cs.FL cs.LO
Learning Implicitly with Noisy Data in Linear Arithmetic
Imperial College London（帝国理工学院）；University of Edinburgh（爱丁堡大学）；Washington University in St. Louis（圣路易斯华盛顿大学）
用真实世界的数据在表达性语言中进行鲁棒学习仍然是一项具有挑战性的任务。许多传统的方法呼吁化学家没有任何鲁棒性的保证。虽然可能近似正确（PAC）语义学提供了强有力的保证，但学习显式表示并不容易，即使在命题逻辑中也是如此。然而，最近的工作，所谓的“隐式”学习已经显示出巨大的承诺，在获得多项式时间的结果片段的一阶逻辑。在这项工作中，我们扩展了PAC语义学中的隐式学习，以处理线性算术语言中的区间和阈值不确定性形式的噪声数据。我们证明，我们的扩展框架保持现有的多项式时间复杂度的保证。此外，我们提供了迄今为止的纯理论框架的第一个实证调查。使用基准问题，我们表明我们学习最优线性规划目标约束的隐式方法在实践中显着优于显式方法。
2021-09-07 cs.AI cs.LO
