Modular Construction of Fixed Point Combinators and Clocked Boehm Trees
不动点组合子（及其推广：循环组合子）是属于微积分和逻辑核心的经典概念。我们从探索不动点组合子（fpc）的结构开始，极大地推广了众所周知的事实，即如果Y是fpc，Y（SI）再次是fpc，生成Boehm序列的fpc。使用无穷大演算，我们设计无穷多个其他的生成方案的fpc的。通过这种方式，我们找到了以模块化方式构建新的柔性印刷电路板的方案和构建块。在创造了大量新的不动点组合子之后，我们的任务是证明它们确实是新的。也就是说，我们必须证明它们的β-不可转换性。通过Boehm树的已知技术不适用，因为所有fpc具有相同的Boehm树（BT）。因此，我们采用“时钟BT的”，与注释，传达信息的节奏，在BT中的数据产生。BT的，从而丰富了一个内在的时钟行为，从而导致一个精致的歧视方法，为DVDA条款。相应的等式严格地介于β-可转换性和BT-等式之间，BT-等式是经典微积分模型中的等式。类似的方法适用于Levy-Longo Berarducci树。最后，我们通过我们称之为“原子钟”的时钟概念的精度来增加辨别能力。
2010-02-12 cs.LO
A Braided Lambda Calculus
本文提出了一种带辫子的无类型线性λ演算，相应的组合逻辑，以及交叉G-集给出的语义模型。
2021-12-30 cs.LO cs.PL
Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
UCLA Department of Philosophy（加州大学洛杉矶分校哲学系）
本文提出结合模态逻辑与简单类型λ演算的参数化系统λ_θ，通过组合逻辑给出其模型刻画，并证明λ_θ与最大系统λ_ω之间的语义守恒与可表达性结果。
2026-07-14 cs.LO math.LO
Lecture notes on the lambda calculus
这是一组课堂讲稿，是我2001年在渥太华大学，2007年和2013年在达尔豪西大学教授的λ演算课程的基础上发展起来的。这些笔记涵盖的主题包括无类型λ演算、Church-Rosser定理、组合代数、简单类型λ演算、Curry-Howard同构、弱规范化和强规范化、多态性、类型推断、指称语义、完全偏序和PCF语言。
2013-12-26 cs.LO
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
对称交互作用组合子是拉丰交互作用组合子的一个同样有表现力的变体。它们是确定性计算的图重写模型。我们定义了两个观测等价的概念，类似于范式和头范式等价的微积分。然后，我们证明了一个完整的抽象结果的两个等价。这是通过将网解释为康托空间的某些子集（称为大厦）来获得的，这些子集在代数演算理论中扮演着与Boehm树相同的角色。
2009-12-22 cs.DM cs.LO
Models and theories of lambda calculus
本文对Manzonetto博士论文中关于纯无类型代数演算的指称语义和等式/序理论的内容作了简要的总结。主要的研究成果包括：（1）从自反对象构造了一个一般的自反模型，（可能非适点）范畴;（ii）组合代数的斯通式表示定理;（iii）证明没有有效的Eudda模型可以有Euda-beta或Euda-beta-eta作为其方程理论（这可以被看作是对Honsell-Ronchi Della Rocca在1984年提出的一个开放问题的部分回答）。
2009-04-30 cs.LO
Semantics of a Typed Algebraic Lambda-Calculus
代数代数演算已经以各种方式进行了研究，但它们的语义大多未被触及。本文给出了一个具有向量空间结构的一般单型λ演算的语义分析。我们用两个已建立的向量代数演算来描述这种关系。然后我们研究了不动点组合子的加法所引起的问题以及如何修正方程理论来解决这些问题。我们勾勒出一个代数矢量PCF和它可能的指称解释。
2010-06-08 cs.LO
Counting and Generating Terms in the Binary Lambda Calculus (Extended version)
在一篇名为Binary λ演算and combinatory logic的论文中，John Tromp提出了一种将λ演算项编码为二进制序列的简单方法。在下面的内容中，我们研究了表示lambda项的给定大小的二进制字符串的数量，并从它们的生成函数中得出结果，特别是大小为n的项的数量大致增长为1.963447954。.. n.在第二部分中，我们使用这种方法来生成随机lambda项使用玻尔兹曼采样器。
2015-11-17 cs.LO
Clones, closed categories, and combinatory logic
本文用多元结构阐释简单类型λ演算的语义，引入外延SK-克隆并证明其可靠完备，进而证明不含产品的简单类型λ演算是SK-范畴的内部语言。
2024-05-02 cs.LO math.CT
Counting Terms in the Binary Lambda Calculus
在一篇名为Binary λ演算and combinatory logic的论文中，John Tromp提出了一种将λ演算项编码为二进制序列的简单方法。接下来，我们将研究表示lambda项的给定大小的二进制字符串的数量，并从它们的生成函数中得出结果，特别是大小为n的项的数量大致增长为1.963447954^n。
2014-01-02 cs.DM cs.DS cs.LO
Partial combinatory algebra and generalized numberings
广义数是Ershov数概念的扩展，基于部分组合代数（PCA）而不是自然数。我们研究了广义数的各种代数性质，将数的性质与主元分析的性质联系起来。和lambda演算一样，可拓性是这里的关键概念。
2020-04-29 cs.LO math.LO
Lambda Calculus Synopsis
本文给出了一个粗略的，但线性的总结，涵盖了一些关键的定义，符号，和命题从λ演算：它的语法和语义，经典专着由巴伦德雷。首先，我们定义了一个无类型可拓λ演算理论。然后，一些句法糖，一个系统的组合逻辑，和不动点定理进行了描述。最后一节介绍了一个拓扑上的一套lambda条款，这是为了解释一个虚幻的矛盾。也就是说，定义在lambda项集合上的函数在lambda项集合本身中，后者是可数集合。然而，在lambda项的集合上的函数看起来相对于树的拓扑是连续的。
2013-10-24 cs.LO math.GN math.LO
An Invariant Cost Model for the Lambda Calculus
我们定义了一个新的成本模型的按值调用演算满足不变性命题。也就是说，在所提出的成本模型下，图灵机和按值调用算法可以在多项式时间开销内相互模拟。该模型仅依赖于通常的β-归约的组合性质，而不涉及特定的机器或评估器。特别地，单个beta reduction的成本与redex的大小和reduce的大小之间的差异成比例。通过这种方式，归一化lambda项的总成本将考虑所有中间结果的大小（以及范式的步骤数）。
2005-11-12 cs.CC cs.LO
Intersection Types for the Computational lambda-Calculus
我们研究多态类型分配系统的非类型的的影响，基于Moggi的单子方法。从单子的抽象定义出发，我们引入了一个基于Wadler的变体的按值调用的计算型微积分，该变体具有单元和绑定组合子，并且没有let。我们定义了一个概念，减少演算，并证明它是合流的，我们也涉及到我们的演算的原始工作的莫吉表明，他的无类型的元语言可以解释和模拟在我们的演算。然后，我们介绍了一个交集型系统启发Barendregt，Coppo和Dezani系统的普通λ演算，建立转换下的类型不变性，并通过逆极限和过滤器模型的构造提供了演算的模型，并将它们联系起来。我们证明了类型系统的可靠性和完备性，以及主题缩减和扩展属性。最后，我们引入了一个收敛的概念，这是完全相关的减少，并通过其类型的收敛项的特征。
2020-02-07 cs.LO
Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms
大型随机映射和随机项的结构性质可以通过研究各种感兴趣的参数的极限分布来收集。在我们的工作中，我们专注于限制类的地图和他们的对应物在Escherida演算，最近建立在这两个域之间的双射连接。在这种情况下，映射中的参数自然地对应于非参数项中的参数，反之亦然。通过一个相互作用的项和地图，我们得到各种组合规范，使我们能够访问分布的相关参数对，如：根三价映射中的桥数、闭线性二阶项中的子项数、（1，3）-叶映射中的1度顶点数、开线性二阶项中的自由变元数等。我们介绍适当的工具：一个微分方程的矩泵模式和一个由本德定理启发的组合模式。
2021-06-15 cs.LO math.CO
On the enumeration of closures and environments with an application to random generation
本文研究λ-演算中环境和闭包的渐近计数与随机生成，针对朴素与封闭两类结构，利用生成函数构造有效采样器，并讨论封闭类的相关问题。
2019-10-16 cs.LO math.CO
Embeddings between partial combinatory algebras
部分组合代数是作为计算的一般模型的代数结构。本文主要研究pca的嵌入问题。特别是，我们系统化的Kleene的模型，van Oosten的顺序计算模型，和斯科特的图模型的相对化之间的嵌入，表明两个相对化模型之间的嵌入存在的，当且仅当存在一个特定的减少之间的神谕。我们得到了类似的结果lambda演算，特别是显示，它不能嵌入在Kleene的第一个模型。
2022-11-23 cs.LO math.LO
Braids, twists, trace and duality in combinatory algebras
本文研究带状组合代数，证明其与带状范畴自反对象的双向构造关系，借助内部PRO构造给出其等式刻画，并发现它可通过带迹组合子或带对偶性的平衡组合代数两种方式表征。
2024-05-16 cs.LO
Encoding the Factorisation Calculus
Jay和Given-Wilson最近引入了因子分解（或SF-）演算作为内涵计算的最小基本模型。它是一个组合演算，包含一个特殊的组合子F，它能够检查它的第一个参数的内部结构。微积分是重要的，因为它是组合完备的，它也表现出结构完备性的性质，即它能够表示任何函数的条款可定义使用模式匹配对任意范式。特别地，它允许一项，可以决定任何两个任意范式的结构相等。由于SF-演算是组合完备的，它显然至少与我们更熟悉的、更典型的λ演算和组合逻辑的图灵-强大计算模型一样强大。然而，它与这些模型在相反方向上的关系并不那么明显。Jay和Given-Wilson认为SF-演算严格来说比上述模型更强大，但对这些模型之间的联系的详细研究还有待进行。本文开始弥合这一差距，提出了一个忠实的编码到λ演算的因式分解演算保持减少和强规范化。这种编码的存在是一个新的结果。它还表明，在某种意义上，前一种模式与后一种模式之间存在着等价性。我们讨论在何种程度上我们的结果构成了一个等价的，考虑它在一些先前定义的框架比较计算能力和表现力的上下文中。
2015-08-27 cs.LO
Addressing Machines as models of lambda-calculus
本文提出可寻址机器作为λ演算模型，通过仅操作地址的简单机器及最左归约语义，并引入类似ω和ζ_β的规则，构建完整的无类型λ演算模型。
2022-07-28 cs.LO
Linear lambda terms as invariants of rooted trivalent maps
本文的主要目的是对这种对应关系作一个简单的概念性解释（最初由Bodini，Gardy和Jacquot描述）在无边界的紧致定向曲面上的闭线性lambda项的$α$ -等价类和有根三价映射的同构类之间，作为具有自由变量上下文的线性λ项和具有自由边边界的有根三价映射之间的更一般对应关系的实例。我们首先回顾一个熟悉的图形表示的线性lambda条款，而在同一时间解释如何这样的图可以正式阅读作为一个符号的自反对象在一个对称monoidal封闭（双）范畴。从那里，对应的“容易”方向是一个简单的健忘操作，它擦除线性lambda项图上的注释，以产生一个有根的三价映射。另一个方向将线性lambda项视为其底层有根三价映射的完全不变量，通过自由边映射上的Tutte式拓扑递归重建丢失的信息。作为组合数学中的一个应用，我们使用这种分析来枚举无桥有根三价映射作为线性lambda项，不包含封闭的真子项，并得出结论，给出一个自然的四色定理的重新表述作为一个关于λ演算中的类型的声明。
2017-05-04 cs.LO math.CO math.CT
What is a Model of the Linear Lambda Calculus?
Université Paris Cité（巴黎西岱大学）；CNRS, IRIF（法国国家科学研究中心，IRIF研究所）
从代数角度研究线性λ演算模型，证明其与Curry的λ代数线性类似物和半封闭操作代数等价，给出λ代数线性变体的有限等式表示，并建立Scott表示定理的线性类似物。
2026-07-23 cs.LO
Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq
本文展示了几个版本的应用相似性和上下文近似的等价性，因此也应用双相似性和上下文等价性，在LR中，确定性的按需调用λ演算与letrec扩展的数据构造器，情况表达式和Haskell的seq运算符。LR对Haskell核心语言的非类型化版本进行建模。双相似性的使用简化了微积分中的等价性证明，并为程序转换的更方便的正确性证明开辟了一条道路。证明是通过一个完全抽象和满射转换成一个按名称调用的演算，这是一个扩展的阿布拉姆斯基的懒惰λ演算。在后一种演算中，我们的相似性和上下文近似的等价性可以通过豪的方法来证明。相似性基于归纳定义的相似性被传递回LR。从按需调用letrec演算到扩展的按名调用λ演算的转换是两种转换的组合。第一个翻译取代呼叫按需要的策略，按名称的策略和它的正确性是通过利用无穷树展开的letrec表达式出现。第二个翻译编码字母表达式，通过使用多不动点组合子和它的正确性表明语法比较减少两个演算。本文的一个进一步结果是上述演算之间的同构，这也是一个关于字母自由表达式的恒等式。
2015-03-12 cs.LO
RPO, Second-order Contexts, and Lambda-calculus
首先，我们扩展了Leifer-Milner RPO理论，给出了获得IPO标记的过渡系统（和双相似性）的一般条件，减少了一组过渡，并可能出现分支。此外，我们还研究了Leifer-Milner理论的弱变体，给出了弱双相似是同余的一般条件。然后，我们将这种扩展的RPO技术应用到具有懒惰和按值调用的Reduction策略的λ演算中。我们表明，相反的过程演算，可以直接处理的λ演算语法和应用Leifer-Milner技术一类的背景下，只要我们的工作框架中的弱双相似性。然而，即使在具有最小上下文的转换系统的情况下，所得到的双相似性也是无限分支的，这是因为在标准上下文范畴中，参数规则（如beta规则）只能由无限多个基本规则表示。为了克服这个问题，我们引入了二阶上下文范畴的一般概念。我们表明，通过在这种情况下进行RPO建设，懒惰的观测等价可以被捕获为一个弱的双相似等价的一个分支过渡系统。这个结果是通过考虑组合逻辑中的一种编码来实现的。
2009-08-06 cs.LO cs.PL
Representing operational semantics with enriched Lawvere theories
许多术语演算，如λ演算或pi演算，涉及名称的绑定器，并且绑定变量名称的数学是微妙的。Schoenfinkel在1924年引入了SKI组合子演算，通过消除量化变量来澄清它们在直觉逻辑中的作用。Yoshida演示了如何在异步pi演算中消除来自输入前缀的绑定名称，但她的组合子仍然依赖于new运算符来绑定名称。最近，Meredith和Stay展示了如何修改Yoshida的组合子，用反射算子替换new和replication，以提供第一个没有绑定名称的组合子演算，异步pi演算可以忠实地嵌入其中。在这里，我们提供了一组替代的组合子，它由SKI加上反射构建，也消除了所有的标称现象，但提供了一个忠实的嵌入反射高阶π演算。我们表明，有效地消除了语法糖的名义功能，多分类的Lawvere理论丰富的图形足以捕捉的操作语义的演算。
2017-04-10 cs.LO
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Deepomatic；CNRS（法国国家科学研究中心）；Université Sorbonne Paris Nord（索邦巴黎北大学）；Université de Paris（巴黎大学）
反向传播是一种经典的自动微分算法，用于计算由某类简单的一阶程序（称为计算图）指定的函数的梯度。它是多个领域的基本工具，最值得注意的是机器学习，它是有效训练（深度）神经网络的关键。近年来，一个名为可微程序设计的研究领域迅速发展，其目的是通过求助于实际的程序设计语言，赋予控制流算子和高阶组合子，如map和fold，更综合和模块化地表达计算图。在本文中，我们将反向传播算法扩展到这样的一个程序设计语言的一个范例：我们定义了一个组合程序转换从简单类型的λ演算本身增加了一个概念的线性否定，并证明了这计算梯度的源程序具有相同的效率作为一阶反向传播。转换是完全无效果的，因此提供了对反向传播动态的纯逻辑理解。
2019-11-06 cs.LG cs.LO cs.PL
A theory of linear typings as flows on 3-valent graphs
建立在最近建立的枚举连接之间的λ演算和嵌入图（或“地图”）的理论，本文开发了一个类比之间的类型（λ条款）和着色（地图）。我们的出发点是抽象图上的阿贝尔群值“流”的经典概念（Tutte，1954）。输入一个线性lambda项可以被自然地看作是构造一个流（在一个嵌入的3-valve图上），该流在一个更一般的代数结构中取值，该代数结构由一个配备了“蕴涵”运算的预序集和满足组合、恒等式和单位定律的单位组成。流理论中有趣的问题和结果（例如无零流的存在）可以从λ演算和逻辑的观点重新审视。例如，我们给出了一个表征时，局部流关系（跨顶点）可以被分类提升到一个全局流关系（跨边界），证明这只是在情况下的底层地图有方向的lambda项。我们还开发了一个基本的理论重写的流，建议拓扑意义的经典完整性的结果组合逻辑，并介绍了一个极化的概念流，它绘制连接到理论的证明网络在线性逻辑和双向类型。
2018-04-27 cs.LO cs.PL math.CO
On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)
λ演算是一种被广泛接受的高阶函数程序的计算模型，但目前还没有一个直接的、普遍接受的代价模型，因此，将lambda项约简为其范式的计算难度通常是通过对具体实现算法的推理来研究的。在本文中，我们表明，当头部减少的基本动力学，单位成本模型确实是不变的。这改进了已知的结果，这些结果只处理弱（按值调用或按名称调用）约简。不变性是通过显式替换的线性演算来证明的，这允许很好地将λ演算中的任何头部减少步骤分解为更基本的替换步骤，从而使头部减少的组合学更容易推理。该技术也是一个很有前途的工具来攻击我们所看到的主要开放问题，即理解哪些规范化策略推导复杂性是不变成本模型（如果有的话）。
2012-02-08 cs.LO cs.PL
On the Semantics of ReFLect as a Basis for a Reflective Theorem Prover
本文探讨了一个组合片段的reFLect，底层的函数式语言，英特尔公司用于硬件设计和验证的微积分的语义。ReFLect类似于ML，但具有基本数据类型，其元素是reFLect表达式本身的抽象语法树。遵循LCF范式，它旨在作为高阶逻辑定理证明器的对象语言，用于规范和推理-但其中对象语言和元语言是统一的。其目的是通过反射机制混合程序评估和逻辑推理。我们确定了一些困难与目前定义的reFLect的语义，并提出了一个最小的修改类型系统，以避免这些问题。
2013-09-23 cs.LO
