Sound Bisimulations for Higher-Order Distributed Process Calculus
虽然分布式系统的进程转移已经变得普遍，推理他们的行为的方法是欠发达。在本文中，我们提出了一个互模拟技术证明行为等价的\emph{higher-order $π$-calculus with passivation}（和限制）中建模的系统。以前的研究，这种演算仅限于上下文互模拟和正常的互模拟，这是不切实际的或不健全的。相比之下，我们提供了一个健全的和有用的定义\emph{environmental bisimulations}，与几个非平凡的例子。从技术上讲，我们的互模拟中的一个中心点是并行组合的子句，它必须考虑在执行过程中产生的进程的钝化。
2011-05-06 cs.DC cs.LO cs.PL
History-Preserving Bisimulations on Reversible Calculus of Communicating Systems
历史互模拟和遗传互模拟（HPB和HHPB）是并发指称模型的等价关系。在进程代数中寻找它们的对应物是一个开放的问题，有一些部分的成功：在通信系统演算（CCS）中存在一个基于因果树的等价物，对应于HPB。在可逆CSS（RCCS）中，有一个对应于HHPB的互模拟，但它只考虑没有自动并发的进程。我们提出了等价的CCS与自动并发对应的HPB和HHPB，和他们所谓的“弱”的变种。等价性不仅利用了RCCS的可逆性，而且利用了RCCS的记忆机制。
2018-04-27 cs.DC cs.FL cs.LO
Tree algebras and bisimulation-invariant MSO on finite graphs
CNRS, IRIF, Université Paris Cité（法国国家科学研究中心，信息研究与交叉研究所，巴黎西岱大学）；CNRS, LIP, ENS Lyon（法国国家科学研究中心，高等师范学校里昂分校计算与语言实验室）
该研究解决了悬而未决数十年的问题，证明有限转换系统上互模拟不变的MSO片段与模态μ演算表达等价，完善了无限树正则语言的代数理论。
2026-09-02 cs.LO
On Probabilistic Applicative Bisimulation and Call-by-Value $λ$-Calculi (Long Version)
概率应用互模拟是一个最近推出的共归纳方法程序等价的概率，高阶，设置。在本文中，该技术被应用到一个类型化的，按值调用，演算。令人惊讶的是，所获得的关系符合上下文等价，相反，当调用的名字被认为是评估时会发生什么。更令人惊讶的是，完全抽象只适用于对称设置。
2014-01-29 cs.LO
Applicative Bisimulation and Quantum $λ$-Calculi (Long Version)
应用互模拟是一种在高阶函数式语言中检验程序等价性的共归纳技术。就上下文对等而言，它是合理的，有时是完整的。在本文中，我们表明，应用互模拟也工作时，底层语言的程序采取的形式的线性$λ$ -演算扩展的功能，如概率二进制选择，但也量子数据，后者是一个设置中的线性发挥作用。的主要结果是证明所获得的概念的双相似性的合理性。
2015-06-22 cs.LO
Bisimulations for Delimited-Control Operators
本文系统研究了带分隔控制算子 shift 和 reset 的无类型 λ-演算的行为理论，定义了上下文等价并提出了多种双相似关系来刻画它，并探讨了扩展方向。
2019-05-23 cs.LO
Generating Witness of Non-Bisimilarity for the pi-Calculus
在逻辑编程范式中，很难开发出一个优雅的解决方案来生成证明两个π演算过程之间的开放双相似性失败的区分公式;这是出乎意料的，因为π演算和开放互模拟的语义已经在高阶逻辑编程系统中被优雅地指定。我们使用Haskell的解决方案将公式生成定义为从所有不确定互模拟步骤的森林到一对区分公式的树变换。由于Haskell中的惰性，只生成树转换函数所需的必要路径。我们的工作表明，Haskell和它的库提供了一个有吸引力的平台，象征性地分析等价性标记的过渡系统在环境敏感的设置。
2017-05-31 cs.LO
Capturing Bisimulation-Invariant Exponential-Time Complexity Classes
奥托定理将图上的互模拟不变PTIME查询描述为可以在多元μ演算中制定的那些查询，它依赖于Immerman-Vardi定理，Immerman-Vardi定理通过具有最少不动点的一阶逻辑来描述PTIME（有序结构）。这种连接已经通过在谓词上使用函数的polyadic μ演算的扩展到了具有最小不动点的双模拟不变EXPTIME，利用Immerman的二阶逻辑对EXPTIME的表征。在本文中，我们表明，在指数时间层次中的所有类的互模拟不变的版本有逻辑对应的出现作为扩展的polyadic μ演算的高阶函数。这利用了高阶逻辑（k+1阶）对k-EXPTIME的特征化，具有最少的不动点，这是由Freire和Martins提出的。
2022-09-21 cs.CC cs.LO
Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
受最近基于线性逻辑技术的λ演算的图形化形式的启发，我们引入了一种无类型的结构λ演算，称为λ j，它将距离上的动作与指数规则相结合，通过弱化、收缩和消除来分解替换.首先，我们证明了一些基本性质的lambda j，如合流和保存的β-强规范化。第二，我们添加了一个强大的互模拟λ j通过一个方程的理论，特别是捕获Regnier的西格玛等价。然后，我们完成了这两个以上的方程的互模拟（去）组成的替代品，我们证明，由此产生的演算仍然保持β-强规范化。最后，我们讨论了我们的结果的一些后果。
2012-03-23 cs.LO
A Fully Abstract Symbolic Semantics for Psi-Calculi
我们提出了一个符号转换系统和PSI演算的互模拟等价，并证明了它是完全抽象的非符号语义的互模拟同余。psi演算是pi演算的扩展，具有用于数据结构和用于表示关于数据的事实的逻辑断言的名义数据类型。这些可以在进程之间传输，并且它们的名称可以使用标准的pi演算机制进行静态作用域，以允许范围迁移。PSI演算可以比其他提出的pi演算的扩展更一般，例如应用pi演算，pi演算，融合演算或并发约束pi演算。符号语义对于在探索状态空间的自动化工具中有效地实现微积分是必要的，并且完全抽象属性意味着过程的语义不会从原始的改变。
2010-02-15 cs.LO
A synchronous pi-calculus
SL同步编程模型是Esterel同步模型的松弛，其中对瞬时内没有信号的反应只能在下一瞬时发生。在以前的工作中，我们已经重新审视了SL同步编程模型。特别是，我们讨论了一种替代设计的模型，包括线程产卵和递归定义，介绍了CPS翻译的尾部递归形式，并提出了互模拟等价的概念。在目前的工作中，我们扩展了尾递归模型与一阶数据类型获得一个非确定性同步模型的复杂性是一个的pi演算。我们表明，我们的互模拟等价的方法可以应付这种扩展，特别是标记的互模拟可以表征为上下文互模拟。
2007-02-09 cs.LO cs.PL
Strong Bisimulation for Control Operators
本文的目的是确定程序的控制运营商的减少语义是在确切的对应关系。这是通过引入一个关系$\simeq$来实现的，该关系定义在Parigot的$λμ$的修正表示上-我们称之为$ΛM$的演算。我们的结果建立在两个基本成分上：（1）通过$ΛM$的显式项算子将$λμ$ -归约分解为乘法和指数步骤，以及（2）将$ΛM$ -项转换为Laurent的极化证明网（PPN），使得PPN中的割消模拟我们的演算。我们提出的关系$\simeq$的PPN结构等价的特点。最值得注意的是，$\simeq$被证明是一个强大的互模拟相对于减少$ΛM$，即两个$\simeq$ -等价的条款有完全相同的减少语义，一个结果，这失败的Regnier的$σ$ -等价的$λ$ -演算以及劳伦特的$σ$ -等价的$λμ$。
2019-10-16 cs.LO cs.PL
Proof-relevant pi-calculus
形式化π演算是对逻辑框架和机械化元理论系统的表达能力的启发性测试，因为存在名称绑定、带有名称挤出的标记转换、互模拟和结构一致性。形式化已经在各种系统中进行，主要集中在充分研究（和具有挑战性）的属性，如过程互模拟理论。我们提出了一个形式化的Agda，而不是探讨理论的并发转换，残留，因果等价的痕迹，这是以前没有正式的π演算。我们的形式化采用德Bruijn指数和依赖类型的语法，并对齐的“证明转换”提出的Boudol和Castellani在CCS的上下文中与自然存在的Agda的表示标记的过渡关系的证明条款。我们的主要贡献是证明了“钻石引理”的剩余的并发过渡和一个正式的定义等价的轨迹置换的过渡。
2015-07-29 cs.LO
Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus
本文展示了我们如何利用异步转换系统来定义所应用的$π$ -演算的非交织语义，该系统的转换用事件标记，并且配备了事件独立性的概念。我们定义的最重要的概念是：开始-终止或ST-双相似性，保留事件的持续时间;和历史保留或HP-双相似性，保留因果关系。我们指出，相应的相似前序暴露这些语义之间的区别。我们提请特别注意HP故障相似性的区分能力，并讨论它如何影响攻击者的威胁模型，我们验证的安全性和隐私属性。我们还比较现有的概念，位于双相似性的定义，我们介绍。
2022-09-06 cs.CR cs.DC cs.LO
Encoding call-by-push-value in the pi-calculus
本研究定义了CBPV到π演算的编码，针对pi-i-calculus优化以解决形式化难题，证明其可靠完备且满足优良编码标准，并启动了Coq形式化验证工作。
2025-06-12 cs.CL cs.LO
Core Higher-Order Session Processes: Tractable Equivalences and Relative Expressiveness
这项工作提出了易于处理的双向模拟高阶π演算会话原语（HOPI），并提供了一个完整的研究其最重要的子演算的表达能力。首先，我们开发了三种类型的互模拟，这是符合上下文对等。这些特征表明，仅观察高阶值的特定有限集合（其存在于会话类型中）作为输入就足以推理HOp过程。接下来，我们确定HO，一个最小的，二阶的HOPI子演算，其中高阶的应用程序/抽象，名称传递和递归是缺席的。我们表明，HO可以编码HOPI扩展高阶应用程序和抽象，一阶会话π演算可以编码HOPI。这两种编码都是完全抽象的。我们还证明了会话π演算与共享名称的传递不能被编码到HOPI没有共享名称。我们表明，HOPI，HO和PI是同样的表达; HO的表达能力，使有效的推理类型等价的高阶过程。
2015-02-10 cs.LO
How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation
可逆计算开辟了克服硬件当前物理限制的可能性。它还提供了理论上的见解，因为它丰富了多种计算范式和模型，有时回顾性地启发它们。例如，并发可逆计算为通信系统微积分提供了有趣的扩展，但仍然缺乏自然和相关的互模拟来研究过程等价性。我们的论文制定了一个等价利用可逆性的两个方面：向后移动和记忆机制。这种互模拟捕获了并发性的指称模型（历史和遗传的历史保留互模拟，（H）HPB）的经典等价关系，到目前为止，进程代数只部分表征了这些模型。这一结果提供了一个洞察可逆性的表现力，因为向后移动和记忆机制，提供“向后确定性”-需要捕捉HHPB。
2020-05-14 cs.DC cs.FL cs.LO
Proving Soundness of Extensional Normal-Form Bisimilarities
本文提出一种系统方法，证明外延范式互模拟及其上下文上至技术的可靠性，并应用于三个按值调用λ-演算，结果已在Coq中形式化。
2019-03-28 cs.LO cs.PL
Enabling Preserving Bisimulation Equivalence
大多数用于验证活性属性的公平性假设都被批评为过于强大或不切实际。另一方面，公正性，可以说是验证活性属性所需的最小公平性假设，并不被经典的语义等价所保留，例如强双相似性。为了克服这一缺陷，我们引入了一个更好的替代强双相似性，使保持双相似性。我们证明了这个等价是正义的保持和所有的标准运营商，包括并行组合的一个同余。
2021-07-31 cs.LO
Split-2 Bisimilarity has a Finite Axiomatization over CCS with<br> Hennessy's Merge
本文指出，分裂-2互模拟等价（也称为定时等价）提供了一个有限的方程公理化的进程代数，通过增加一个辅助操作Hennessy在1981年提出的递归，重新标记和限制自由片段米尔纳的演算通信系统。因此，除了一个单一的二元运算，即轩尼诗的合并，是足够的有限的方程公理化的并行组合模这个非交错等价。这一结果与同一作者以前得到的一个定理形成鲜明对比，该定理认为同一语言不是基于模互模拟的等价语言。
2005-06-21 cs.LO
Normal Form Bisimulations By Value
本文提出一种新的按值调用范式互模拟net互模拟，以弥补现有enf互模拟在验证无意义项识别和letexp交换律上的不足，并分析其与Ehrhard关系模型的关系。
2023-09-05 cs.LO cs.PL
Compositional equivalences based on Open pNets
建立程序或系统之间的等价关系对于验证程序的正确性（通过建立两个实现是等价的）和证明优化和程序转换（通过建立修改后的程序与源程序等价）都是至关重要的。程序存在几种等价关系，互模拟是这些等价关系中最通用的。在互模拟关系中，我们可以区分强互模拟和弱互模拟，强互模拟要求程序的每个动作都由等价程序的单个动作模拟，弱互模拟是一种粗糙的关系，允许某些动作是不可见的或内部移动的，因此不被等价程序模拟。pNet是对开放系统进行建模的自动机的概括。它们以变量和层次结构为特征。开放式pNet是具有洞的pNet，即层次结构内的占位符，稍后可以由子系统填充。本文定义了互模拟关系，用于比较指定为pNet的系统。我们首先定义了一个强互模拟开放pNet。然后，我们定义了一个类似于经典的弱互模拟的等价关系，并研究了它的性质。在这些性质中，我们感兴趣的是组合性：如果两个系统被证明是等价的，那么它们将无法通过它们的上下文来区分，并且当它们的洞被等价系统填充时，它们也将无法区分。我们确定充分条件的自动机，以确保组合的强和弱互模拟。文章用一个传输协议运行的例子来说明，它显示了我们的形式主义和我们的互模拟关系的特点。
2021-10-22 cs.LO
Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods
我们引入多项式耦合，概率耦合的推广，开发一个算法的等价关系的计算，可以被解释为一个提升的概率互模拟多项式微分方程，一个无处不在的模型的动力系统在科学和工程。该算法具有多项式时间的复杂性，并补充了经典的分区细化方法，因为：（a）它实现了系统的本地探索，可能产生的等价，不一定涉及整个系统的检查微分方程;（b）它可以增强技术;（c）它允许规范的对不应该被包括在输出中。使用一个原型，这些优势被证明从系统生物学的应用程序模型简化和比较的案例研究。值得注意的是，我们报告四个数量级较小的运行时间比分区细化方法时反驳马尔可夫链之间的等价性。
2021-04-27 cs.LO
Context-Free Session Types for Applied Pi-Calculus
我们提出了一个二进制会话类型系统，使用上下文无关的会话类型的一个版本的应用π演算的阿巴迪等。al.，其中只能发送基本项、常量和通道。会话类型类似于BPA的过程术语，我们使用互模拟等价来表征类型等价。我们提出了一个定义在类型等价类上的约束类型系统，其中类型等价被构建到类型系统中。这两种类型的系统满足一般的健全性属性，这是建立一个呼吁通用会话类型系统的PSI演算。
2018-08-27 cs.LO cs.PL
Relating Apartness and Branching Bisimulation Games
本文建立分离关系与回合制双人博弈之间的联系，证明在图像有限和有限迁移系统中，Spoiler 玩家的获胜配置对应分离证明，为强互模拟和分支互模拟提供新的证明视角。
2024-11-05 cs.LO
Modelling MAC-Layer Communications in Wireless Systems
我们提出了一个定时过程演算建模无线网络中，各个站广播和接收消息，而且广播受到碰撞。基于简化语义的演算，我们定义了一个上下文等价比较这样的无线网络的外部行为。此外，我们构建了一个扩展的LTS（标记的过渡系统），它模拟了可以直接观察到的外部环境的站的活动。在这个LTS标准互模拟提供了一个健全的证明方法，证明系统的上下文等价。我们说明了一系列的例子证明方法的实用性。最后，我们表明，这种证明方法也是完整的，对于一大类系统。
2015-03-30 cs.LO
Modular coinduction up-to for higher-order languages via first-order transition systems
本文通过完全抽象翻译将一阶LTS上的up-to双模拟技术推广到高阶语言（π-演算、λ-演算及带引用的λ-演算），仅需手动验证新语言特有技术的相容性。
2021-09-16 cs.LO cs.PL
Bisimulation Equivalence of First-Order Grammars
本文给出了一阶文法（重写一阶项根的标号规则的有限集合）互模拟等价性的可判定性证明。该等价性推广了DPDA（deterministic pushdown automata）等价性，其结果与Senizergues（1998，2005）在方程图框架下的结果或在PDA框架下的结果一致.经典一阶项的框架似乎特别有用，可以为更广泛的受众提供可以理解的证明。我们还讨论了Fu和Yin（2014）宣布的分支双相似性的扩展。
2014-05-30 cs.FL cs.LO
Using Pi-Calculus Names as Locks
本文引入类型系统将异步pi-calculus名字用作锁，支持锁释放，保证无死锁和无泄漏，并研究类型化行为等价。
2023-09-13 cs.LO cs.PL
From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus
我们研究了Pi演算，丰富了配对和非阻塞输入，并定义了一个使用类型构造函数“箭头”的类型赋值概念。我们编码电路的演算X到这个变种的Pi，并表明，所有的减少（削减消除）和可分配的类型被保留。由于X享有根岑演算LK的Curry-Howard同构，这意味着LK中的所有证明都有Pi的表示。
2011-09-22 cs.LO
Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
给经典推理赋予计算意义的问题是逻辑的核心。这篇文章调查了这个问题的三个著名的解决方案-微积分，修改的可实现性和辩证法解释-并从现代的角度重新审视它们，特别强调与算法和编程的联系。
2018-12-14 cs.LO
An Introduction to the Clocked Lambda Calculus
我们简要介绍了时钟λ演算，一个扩展的经典λ演算与一元符号τ用于见证β步骤。与经典的λ演算相比，这种推广是无穷强正规化的和无穷汇合的。无限范式是丰富的Boehm树，我们称之为钟控Boehm树。
2014-05-29 cs.LO
Focalization and phase models for classical extensions of non-associative Lambek calculus
Lambek的非联想句法演算（NL）在其资源意识方面表现出色：通常的弱化，收缩，交换甚至结合性的结构规则都被丢弃。最近，有人提出了一些保守的扩展，以免除NL对具有单一结论的序列的直觉偏见：De Groote和Lamarche的经典非结合Lambek演算（CNL）和Moortgat及其同事的Lambek-Grishin演算（LG）。我们证明了Andreoli的聚焦属性所述的建议：一个规范化的结果，确定在很大程度上，那些不同的只是由平凡的规则排列的切免费的cirrhosis推导。在这样做的时候，我们从一个“统一的”CCN介绍，通过增加结构规则从LG派生CNL。规范化的证明收益的句法阶段模型的建设，其中每一个“真理”有一个集中的证明，类似于冈田和Herbelin和李的工作。
2011-06-02 cs.LO
Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory
经典（或布尔）类型论是允许类型推断$σ\to \bot) \to \bot => σ$（双重否定消除的类型对应物）的类型论，其中$σ$是任何类型，$\bot$是荒谬类型。本文首先提出了一个指称语义的简化版本的Parigot的Alzoda-mu演算，经典的类型论的一个重要例子。在这种语义中，每个类型的定义域被划分为无限多个等级，不仅包含等级为0的类型的通常成员，还包含它们在更高等级中的否定、合取和析取阴影，这形成了一个无限嵌套的布尔结构。荒谬类型$\bot$被识别为真值类型。然后，本文提出了一个新的演绎系统的经典类型论，一个演算称为经典类型系统（CTS），它涉及到标准的逻辑运算符，如否定，合取，和分离，从而反映了讨论的语义结构，在一个更直接的方式。
2016-06-21 cs.LO
A lambda calculus for density matrices with classical and probabilistic controls
在本文中，我们提出了两种口味的量子扩展的λ演算。第一个是$λ_ρ$，它遵循经典控制/量子数据的方法，其中量子数据由密度矩阵表示。我们提供了一个解释程序的密度矩阵和功能。第二种算法$λ_ρ^\circ$利用密度矩阵的表示方法，跟踪程序在一种广义密度矩阵中的混合轨迹。这种控制可以被看作是量子控制和数据方法的一种较弱形式。
2017-11-20 cs.LO
A sequent calculus with dependent types for classical arithmetic
在最近的一篇论文中，Herbelin开发了一种演算dPA $^ω$，其中可数和依赖选择公理的构造性证明可以通过将可数全称量化的证明编码为一个组件流来推导。然而，规范化的属性（因此也是健全性的属性）只是被证明了。规范化证明的困难在于依赖依赖类型的同时存在（对于选择的建设性部分），控制运算符（用于经典逻辑），共归纳对象（将$N\rightarrow A$类型的函数编码为流$(a_0,a_1,\ldots)$）和具有共享的惰性求值（对于这些共归纳对象）。建立在以前的作品，我们在本文中介绍了一个变种的dPA $^ω$提出的一个微积分。一方面，我们利用我们开发的Krivine经典可实现性的一个变体来证明经典按需调用的规范化。另一方面，我们受益于dL，一个经典的依赖类型的微积分，其中类型安全是确保使用定界的延续与语法限制。通过结合这些文件中开发的技术，我们设法定义一个可实现的解释我们的微积分，使我们能够证明规范化和健全的。
2018-12-20 cs.LO
Proof Analysis of A Foundational Classical Singlesuccedent Sequent Calculus
本文论证现有经典单后件矢列演算均不足以继承 Gentzen 的 LK 系统，并提出专为满足经典证明论期望而设计的 G-Calculus 经典部分 Gc。
2025-07-06 cs.LO
A lambda calculus for quantum computation with classical control
本文的目标是为量子计算机开发一种函数式程序设计语言。我们开发了一个λ演算的经典控制模型，以下第一作者的工作量子流程图。我们定义了一个按值调用的操作语义，并给出了一个使用仿射直觉线性逻辑的类型系统。本文的主要结果是语言的安全属性和类型推断算法的发展。
2004-11-12 cs.LO
The stack calculus
我们介绍了一个简单的语法和操作语义的功能演算，其中的演算介绍到目前为止，在Curry-Howard对应的经典逻辑可以忠实地编码。我们的演算没有任何限制地享有汇流。它的类型系统加强了表达式的规范性，是一个健全而完整的全蕴涵经典逻辑系统。我们给出了一个非常简单的指称语义，它可以很容易地计算表达式的解释。
2013-03-29 cs.LO
Countdown $μ$-calculus
我们介绍了倒计时$μ$ -演算，扩展的模态$μ$ -演算的顺序近似的不动点算子。除了经典微积分中可定义的性质外，它还可以表达（无）有界性，例如存在任意长的特定动作序列。与奇偶游戏和自动机的标准对应关系扩展到适当定义的倒计时游戏和自动机。然而，与经典的设置，标量片段是可证明的弱于完整的向量演算，并对应于自动机满足一个简单的语法条件。我们建立了一些事实，特别是可判定性的模型检验问题和严格的层次结构所引起的最大允许嵌套我们的新运营商。
2022-07-31 cs.LO
System $F^μ_ω$ with Context-free Session Types
我们研究越来越多的表达类型系统，从$F^μ$ --多态lambda演算的等递归类型的扩展--到$F^{μ;}_ω$ --高阶多态λ演算的等递归类型和上下文无关的会话类型。类型等价由定义在一个新的类型标记转换系统上的标准互模拟给出。我们的系统包含了文献中研究的$F^μ_ω$的收缩片段。各种类型语言的类型等价的可判定性结果是通过将类型转换为适当的计算模型的对象来获得的：有限状态自动机、简单语法和确定性下推自动机。我们表明，类型等价是可判定的类型语言的一个重要片段。我们进一步提出了一个消息传递，并发函数语言配备了表达类型语言，并表明它享有保存和不存在的运行时错误的类型化进程。
2023-01-20 cs.FL cs.LO cs.PL
XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus
长期以来，公式XCB = EpEEEpqErqr是否是经典等价演算的一个公理，以及替换和分离规则，一直是一个悬而未决的问题。本文肯定地回答了这个问题，从而完成了对70年前开始的所有这类11符号单公理的搜索。
2002-11-13 cs.AI cs.LO
Complexity of Nonassociative Lambek Calculus with classical logic
本文证明将经典逻辑与非结合兰贝克演算合并得到的BFNL，其后承关系仍可在指数时间内判定，解决了加入经典联结词后保持可判定性的复杂度问题。
2024-12-31 cs.CC cs.LO
The decohered ZX-calculus
本文通过退相干ZX演算的生成元，提出一个通用且完备的演算片段，用于仿射支撑概率分布，并给出范式，为处理混合经典-量子过程及更一般概率过程奠定基础。
2025-08-06 cs.LO quant-ph
Composing Codensity Bisimulations
本文利用代数与余代数层面的余密度提升，将分配律提升问题归结为余密度提升间的分配律构造，并给出简化充分条件，用于证明自动机等状态系统行为等价性及行为度量的组合性。
2024-05-22 cs.LO math.CT
Canonical Proof nets for Classical Logic
证明网为模规则排列的证明提供了抽象的对应物;其思想是，如果两个证明具有相同的底层证明网，则它们本质上是相同的证明。因此，提供一个令人信服的证明网络对应于经典的微积分证明是理解经典微积分证明的重要一步。通过令人信服，我们的意思是：（a）应该有一个典范函数从证明网络的证明，（b）应该有可能检查网络的正确性在多项式时间，（c）每个正确的网络应该是可获得的从一个微积分证明，（d）应该有一个削减消除程序，保持正确性。以前的尝试给证明网类对象的命题经典逻辑已经失败了至少一个上述条件。在[23]中，作者给出了满足（a）和（b）的证明网（扩展网）的演算;文章定义了与扩展网对应的证明演算，但没有给出（c）的显式证明。该演算称为LK \ast，是一种新的具有加法和乘法析取规则的单边演算.本文（[23]的一个自包含的扩展版本）给出了关于LK \ast的扩展网的（c）的一个充分证明，并且另外给出了扩展网内部的一个割消元过程--这使得扩展网成为满足所有四个准则的经典逻辑的第一个证明网概念。
2012-03-19 cs.LO math.LO
The ZX&-calculus: A complete graphical calculus for classical circuits using spiders
我们给出了由Z和X蜘蛛（对应于复制和加法）生成的ZX演算的片段ZX&以及“非”门和“与”门的完整介绍。为了证明完整性，我们自由地添加一个单位和计数器到由Toffoli门和辅助位生成的TOF类别中，表明这产生了有限序数和函数的完整子类别，对象幂为2;然后在此类别和ZX之间进行双向翻译。转换到TOF的某些扩展，而不是ZX演算的某些片段，是一个自然的选择，因为Toffoli门的乘法性质。为此，我们表明，自由添加计数到半Frobenius代数的离散逆范畴是相同的笛卡尔完成。特别地，对于一个离散逆范畴，经典通道范畴、笛卡尔完备化和加可数都产生同一个范畴。因此，将这些构造应用于TOF产生了有限序数的全子范畴和对象幂为2的部分映射。通过将自由单位完备化和自由单位完备化粘合在一起，这就产生了“量子比特多重关系”。"
2021-09-06 cs.LO math.CT quant-ph
Computational interpretation of classical logic with explicit structural rules
我们提出了一个演算提供了一个Curry-Howard对应的经典逻辑中所表示的显式的结构规则，即弱化和收缩演算。这些结构规则分别引入了明确的删除和重复的条款。我们提出了一个类型系统，我们证明了类型保持下减少。详细研究了它与经典微积分之间的一种相互关系，这种关系具有隐含的结构规则。从这个分析中，我们得到强归一化性质。
2012-03-21 cs.DC cs.LO math.LO
Higher-order semantics for quantum programming languages with classical control
本论文以类型论为理论框架，分三个层次研究量子计算的范畴形式化。我们研究的第一阶段涉及匕首λ演算的创建，匕首紧范畴的λ演算。我们的第二个贡献提升了表达能力的匕首λ演算，量子程序设计语言，通过添加经典控制的形式互补的经典结构和dualisers。最后，我们的第三个贡献演示了如何我们的λ演算可以应用到各种众所周知的量子计算问题。
2013-11-26 cs.LO cs.PL math.CT
A Lambda Calculus for Quantum Computation
经典的lambda演算既可以被看作是一种编程语言，也可以被看作是一种用于计算推理的形式代数系统。它提供了一个相当于图灵机的计算模型，并继续在经典计算理论中发挥巨大作用。我们建议，量子计算，像它的经典对应，可能会受益于一个版本的lambda演算适合表达和推理量子算法。在本文中，我们开发了一个量子lambda演算作为量子计算的替代模型，它结合了量子图灵机和量子线路模型的一些优点。演算原来是密切相关的线性lambda演算用于研究线性逻辑。我们建立了一个计算模型和一个方程证明系统，我们认为它是等价的量子图灵机。
2004-04-03 cs.LO hep-th quant-ph
