Non determinism through type isomorphism
Alejandro Díaz-Caro, Gilles Dowek
我们定义了一个等价关系的命题和一个证明系统，其中等价的命题有相同的证明。这种方法得到的系统类似于几个已知的非确定性和代数微积分。
We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Typed Non-determinism in Functional and Concurrent Calculi
针对非确定性与线性资源控制的冲突，本文分别提出受会话类型约束的非确定性 π-演算和受交集类型约束的资源 λ-演算，并以正确翻译建立二者联系。
Call-by-value non-determinism in a linear logic type discipline
我们考虑按值调用演算扩展了一个可能收敛的非确定性选择和一个必须收敛的并行组合。灵感来自最近的作品的关系语义的线性逻辑和非幂等交集类型，我们赋予这种演算的类型系统的基础上，所谓的吉拉德的第二个翻译的直觉逻辑线性逻辑。我们证明了一个术语是可类型的，当且仅当它是收敛的，并且它的类型树携带足够的信息，以给出其懒惰的按值调用约简的长度上的界。此外，当类型树是最小的，这样的界限成为减少的确切长度。
Typed Non-determinism in Concurrent Calculi: The Eager Way
本文提出一种基于急切语义的会话类型π-演算，以处理非确定性与线性性的张力，确保无死锁性，并通过翻译资源λ-演算展示其表达能力。
Two Guarded Recursive Powerdomains for Applicative Simulation
时钟立方类型论是一种新的类型论，它结合了保护递归的能力、单值和高级归纳类型（HIT）。这种类型论可以被用来作为一种元语言的合成守护域理论，其中可以解决守护递归型方程，也与负变量的出现，并使用这些来构建模型的推理程序设计语言。将其与HIT相结合，允许使用基于集合论的语义方法中熟悉的类型构造器，例如这些模型中的幂集和有限幂集。在本文中，我们展示了如何推理的组合有限的非决定性和递归在这个类型论。与传统的论域理论不同，它把程序的排序作为原语，综合保护论域理论把计算步骤的概念作为模态算子的原语。我们使用这个额外的内涵信息来定义两个守护递归（有限）powerdomain建设不同的方式非确定性与计算步骤的相互作用。作为一个例子，这些应用程序，我们展示了如何证明适用的相似性的情况下，可能和必须收敛的有限非确定性的无类型的λ演算的同余。这些结果通常使用操作推理和Howe方法来证明。在这里，我们使用一个适应的指称方法开发的皮茨域理论的背景下。
The Power of Non-Determinism in Higher-Order Implicit Complexity
我们研究了高阶类型的纯函数式程序设计语言中的非确定性的力量。具体来说，我们考虑不同的数据顺序，配备明确的非确定性选择的无缺点的程序。Cons-freeness大致意味着数据构造函数不能出现在函数体中，因此所有对存储空间的操作都必须使用调用堆栈间接发生。虽然无缺点的程序以前已经被一些作者用来计算复杂性类，但非确定性程序的工作几乎只考虑数据阶为0的程序。以前的工作已经表明，添加明确的非确定性的无缺点的程序，以0的顺序数据不增加表达能力，我们证明，这是显着的情况下，更高的数据顺序：添加非确定性的程序，数据顺序至少为1允许整个类的特征的基本时间可判定集。最后，我们将展示如何，即使是非确定性的选择，原来的层次结构的特征恢复施加不同的限制。
Isomorphism within Naive Type Theory
我们提供了一个治疗的同构内的一套理论制定的依赖类型论。类型表达式被赋予其自然的集合论组合意义。类型分为小类型和大类型-分别是集合和真类。每一个真类，如“群”或“拓扑空间”，都有一个与标准定义相对应的同构概念。同构是通过在所有可定义值的空间上定义一个广群结构来处理的。这些值同时是对象（oid）和态射-它们是“形态体”。合理性，然后可以证明简单和自然的推理规则，推导同构和同构的替代。
Toward Isomorphism of Intersection and Union types
本文研究了具有交和并类型的代数演算的类型同构。众所周知，在微积分中，两种类型之间的同构是由一对相互逆的项实现的。值得注意的是，可逆项是特定形状的线性项，称为有限遗传置换子。然后，在线性项的交、并类型的相关类型推断系统中，研究了有限遗传置换子的类型性质。特别地，定义了类型之间的同构保持约简。类型归约是汇合的和终止的，并引入了类型的范式的概念。正规类型的性质是完全刻画类型同构的关键一步。本文的主要结果是，一方面证明了具有相同范式的两个类型是同构的，另一方面证明了在范式中两个类型之间同构的特征，箭型的模同构。
Towards Races in Linear Logic
本文提出非确定性 HCP，扩展 HCP 以支持非确定性和竞态，利用有界线性逻辑提供强类型描述，同时保持无死锁等元理论性质。
On Isomorphism of "Functional" Intersection and Union Types
类型同构对于检索库组件很有用，因为库中的函数可以具有与用户期望的类型不同但同构的类型。此外，类型同构免费提供了在用户程序中包含正确类型的函数所需的强制。本文研究了具有交类型和并类型的系统的类型同构问题。在交和并的存在下，同构不是一个同余，不能用等式的方式来描述。仍然可以给出一个特征，但由于函数类型和非函数类型之间的干扰而变得非常复杂。在本文中，我们将每个原子类型解释为将任何参数映射到类型本身的解释中的函数集，从而面临这个缺点。这一选择是由斯科特的逆极限模型的初始投影提出的。本文的主要结果是保证型同构的条件，基于同构保持约简。
Isomorphisms of types in the presence of higher-order references (extended version)
我们调查的问题，类型同构的高阶引用的存在。我们首先介绍了一个有限的程序设计语言与总和类型和高阶引用，我们建立一个完全抽象的游戏模型，阿布拉姆斯基，本田和McCusker的工作。解决一个公开的问题，劳伦特，我们表明，两个分支的竞技场是同构的当且仅当它们是几何相同的，到更名的动作（劳伦特的森林同构）。我们由此推导出一个等式理论的特点同构的类型在我们的语言。然而，我们表明，洛朗的猜想不举行无限分支的舞台上，产生新的非平凡型同构在我们的语言与自然数的一个变体。
Second-Order Type Isomorphisms Through Game Semantics
二阶同构的刻画是一个纯语法问题，我们建议在博弈语义学的启发下进行研究。我们在二阶$μ$ -演算的情况下研究这个问题，它可以被看作是系统F到经典逻辑的扩展，并且我们为它定义了一个范畴框架：控制超理论。我们的游戏模型的$μ$ -演算是基于多态竞技场（密切相关的休斯的超森林），在发挥（以下的想法Murawski Ong）。我们发现，类型同构与“平等”的舞台上与类型相一致。最后，我们从这个等式推出了型同构的等式刻画。我们也从相同的模型恢复Roberto Di Cosmo对系统F的型同构的刻画。这种方法导致几何理解的问题上的二阶型同构，它可以很容易地扩展到其他一些多态演算，包括额外的编程功能。
Dependent Type Theory as Related to the Bourbaki Notions of Structure and Isomorphism
本文开发了一个版本的依赖类型论，其中同构是通过处理直接推广1939年的定义布尔巴基。更具体地说，我们将Bourbaki结构的定义从简单类型签名推广到依赖类型签名。布尔巴基最初的同构概念和这里给出的它的推广都定义了两个结构$N$和$N'$之间的同构，由它们的种类之间的双射组成，这些双射将$N$的结构转换为$N'$的结构。在这里，运输定义的交换性条件与集合论的平等。这不同于在群胚模型和同伦类型论中给出的同构的依赖类型论处理方法，其中没有类似的直接的集合论运输定义。运输的直接定义也导致了一个直接的建设性证明（建设性内容）的有效性替代同构-这是困难的群模型或同伦类型论。
Abstract computation over first-order structures. Part IIb: Moschovakis' operator and other non-determinisms
本文基于BSS RAM框架，研究了一阶结构上不同类型的二元非确定性，比较了非确定性分支、常量猜测限制及Moschovakis算子等机制，并揭示了恒等关系与常量集合的可判定性对机器性能和效率的影响程度。
Curry-style type Isomorphisms and Game Semantics
咖喱风格的系统F，即。从程序设计语言的角度来看，系统F没有显式的类型，可以被看作是多态性的核心表示。本文利用一个博弈模型，从语法和博弈语义域两方面给出了该语言类型同构的一个刻画。该模型包括：一个非类型化部分解释术语，一个博弈概念解释类型，一个类型化部分表示一个非类型化策略在一个博弈中起作用的事实。通过分析模型中的同构，我们证明了Curry型系统F的型同构所对应的方程组是Church型同构方程组的推广，并给出了一个新的非平凡方程：对于所有X. A = A[对于所有Y.Y/X]，如果X只在A中出现.
Process Algebra as Abstract Data Types
本文以抽象数据类型的形式介绍了进程代数的代数语义。为此，我们开发了一种特殊类型的代数，种子代数，它精确地描述了标记转移系统中进程的行为。我们已经证明了两个进程的互模拟与它们相应的种子代数的同构的可能性。我们指出，传统的代数同构概念在这里并不适用，因为两个种子代数的元素之间甚至不存在一一对应。这种一一对应的缺乏来自于过程转换的非确定性选择。我们引入了一种隐藏操作的技术来屏蔽种子代数元素中不需要的细节，这些细节只反映了进程转换的非确定性或其他隐式控制机制。种子代数的元素被认为是不可区分的，如果他们表现出相同的行为后，这些不必要的细节被掩盖。每一类不可区分的元素称为非隐藏闭包。我们证明了两个过程的互模拟等价于表示这两个过程的两个种子代数的非隐闭包的同构。我们称这种同构为深层同构。通过对同一个签名指定不同的公理系统，得到了不同的种子代数模型。每个模型对应于不同类型的互模拟。通过证明这些模型之间的关系，我们还建立了10个不同的互模拟之间的关系，形成一个无环有向图。
Session Type Isomorphisms
在使用类型作为搜索关键字检索函数库中的函数方面，已经做了大量的工作。丰富的组件规范以行为类型的形式可用，使得能够进行类似的查询，其中可以使用组件的行为类型作为搜索关键字来搜索组件库。然而，就像函数库一样，组件库将包含其类型在消息顺序或分支点位置上与搜索到的类型不同的组件。因此，也有必要寻找那些类型不同于但同构于所搜索的组件的组件。本文给出了同构会话类型的语义和公理化刻画。会话类型同构的理论是微妙的。部分原因是它依赖于进程之间的非标准等效概念。此外，我们不知道公理化是否完全。众所周知，箭头，产品和总和类型的同构是不可公理化的，但目前还不清楚是否这个负面的结果也适用于家庭的类型，我们认为在这项工作中。
Type Isomorphisms for Multiplicative-Additive Linear Logic
本文研究了乘法-加法线性逻辑中的类型同构，通过扩展结果到完整MALL，揭示了分配律和消去律等更丰富的等式理论。
Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)
研究含非确定性与失败的 lambda-calculus 到 pi-calculus 的类型化编码，提出新演算 lambdafail 并证明其到 spi 的编码正确性，揭示了顺序求值失败可编码为交互协议。
Isomorphism Revisited
同构是数学结构的核心，并在依赖类型论中以各种方式形式化。所有以前的处理都是通过用某种形式的群胚上的量化来代替集合上的量化来实现的-在这些群胚中，每个态射都是同构。集合上的量化在广群模型中被标准广群上的量化、在同伦类型论中被无穷广群上的量化以及在态胚模型中被态胚上的量化所取代。在这里，我们给一个治疗的同构的基础上的直观概念的集合没有内部结构的集合。集合上的量化仍然是集合上的量化。同构和广群结构，然后出现从简单的，但微妙的句法限制集理论的语言。这种方法更充分地统一了经典的ZFC基础与严格的同构，对称性，规范性，函子和自然变换的治疗。这一切都是在不涉及范畴论的情况下完成的。
Abstract computation over first-order structures. Part IIa: Moschovakis' operator and other non-determinisms
本文探讨一阶结构上的 BSS RAMs 模型是否足够通用，通过引入非确定性算子扩展其能力，以便与 Moschovakis 基于递归可定义性提出的抽象可计算性概念进行比较。
On Resolving Non-determinism in Choreographies
本文提出全谱实现概念，解决编排中非确定性选择与确定性实现的对应关系，并给出类型规则检查方法，以POP协议为案例验证。
Isomorphisms of types in the presence of higher-order references
我们研究了具有高阶引用的程序设计语言中的类型同构问题。我们首先回顾了Abramsky，Honda和McCusker的高阶参考的博弈论模型。解决一个公开的问题，劳伦特，我们表明，两个分支的竞技场是同构的当且仅当它们是几何相同的，到更名的动作（劳伦特的森林同构）。我们由此推导出一个等式理论，它描述了具有高阶引用的有限语言中类型的同构。然而，我们表明，洛朗的猜想并不持有无限分支的舞台上，产生一个非平凡的类型同构的扩展，这种语言与自然数。
Logical Relations for Monadic Types
逻辑关系及其推广是证明微积分性质的基本工具，例如，从而得出观测等价性的合理原则。我们提出了一个自然的概念，逻辑关系能够处理的单子类型的莫吉的计算计算的微积分。治疗是绝对的，是基于subsconing，单因子分解系统和单子态射的概念。我们的方法有一些有趣的应用程序，包括非确定性（在逻辑关系意味着是bisilimeric），动态名称创建，和概率系统的情况下，Alcuda演算。
The Yoneda Reduction of Polymorphic Types (Extended Version)
在本文中，我们探讨了一个家庭的类型同构的系统F的有效性，语义对应的某种形式的Yoneda同构从范畴论。这些同构在比β-η-等价更强的等价理论下成立，就像那些由参数性和非自然性引起的理论一样。我们表明，米田型同构产生重写的类型，我们称之为米田减少，它可以用来消除量词从多态类型，取代它们与单态类型构造函数的组合。我们建立了一些充分条件下，量词可以完全消除多态类型，我们展示了一些应用这些条件来计算居民的类型和计算程序等价系统F的一些片段。
Axioms and Decidability for Type Isomorphism in the Presence of Sums
我们考虑的问题的特点同构的类型，或等价地，建设性的基数集，同时存在的不相交的工会，笛卡尔产品，和指数。主要依赖于在我们的上下文中没有使用的关于具有指数的多项式的结果，我们得到：通常的有限公理化被称为高中恒等式（HSI）对于类型的重要子类是完备的;当两个类型同构时，它对于该子类是可判定的;对于整个类型集，HSI公理的递归扩展是完备的;并且，对于整个类型集，当基类型被解释为有限集时，关于两个类型是否同构的问题是可判定的。我们还指出了一些相关的开放性问题。
MathZero, The Classification Problem, and Set-Theoretic Type Theory
AlphaZero通过只给游戏规则的自我游戏，以超人的水平学习下围棋、国际象棋和将棋。这就提出了一个问题，是否可以为数学做类似的事情-MathZero。MathZero需要一个正式的基础和目标。我们提出了集合论依赖类型论的基础和一个根据分类问题定义的目标--将概念实例分类到同构的问题。自然数是作为有限集合分类问题的解决方案而出现的。在这里，我们推广经典布尔巴基集理论同构集理论依赖类型论。据我们所知，我们给出了第一个同构推理规则的集合论依赖类型论与命题集合论等式。演示文稿的目的是访问数学家没有事先接触到类型论。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。