首页/论文/0705.4228

arXiv 0705.42282007-05-29cs.LO

Curry式类型同构与博弈语义

Curry-style type Isomorphisms and Game Semantics

Joachim De Lataillade

备注：: Accepté à Mathematical Structures for Computer Science, Special Issue on Type Isomorphisms

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

咖喱风格的系统F，即。从程序设计语言的角度来看，系统F没有显式的类型，可以被看作是多态性的核心表示。本文利用一个博弈模型，从语法和博弈语义域两方面给出了该语言类型同构的一个刻画。该模型包括：一个非类型化部分解释术语，一个博弈概念解释类型，一个类型化部分表示一个非类型化策略在一个博弈中起作用的事实。通过分析模型中的同构，我们证明了Curry型系统F的型同构所对应的方程组是Church型同构方程组的推广，并给出了一个新的非平凡方程：对于所有X. A = A[对于所有Y.Y/X]，如果X只在A中出现.

英文摘要：

Curry-style system F, ie. system F with no explicit types in terms, can be seen as a core presentation of polymorphism from the point of view of programming languages. This paper gives a characterisation of type isomorphisms for this language, by using a game model whose intuitions come both from the syntax and from the game semantics universe. The model is composed of: an untyped part to interpret terms, a notion of game to interpret types, and a typed part to express the fact that an untyped strategy plays on a game. By analysing isomorphisms in the model, we prove that the equational system corresponding to type isomorphisms for Curry-style system F is the extension of the equational system for Church-style isomorphisms with a new, non-trivial equation: forall X.A = A[forall Y.Y/X] if X appears only positively in A.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time

This is a survey of λ-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and early 2000s. We discuss logical aspects, modal λ-calculi, and their categorical semantics. The logics underlying the calculi surveyed are constructive versions of K, K4, S4, and LTL.

2016-05-26cs.LO

直觉一阶逻辑：通过Curry-Howard同构的范畴语义

Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism

本文在范畴论的框架内，通过对基于Curry-Howard同构的一阶直觉主义逻辑的计算解释，提出了一种新的可靠而完备的语义.此外，一个健全的和完整的语义相应的Alzoda-calculus的派生，太。这种语义学在某种程度上扩展了由Heyting范畴、拓扑理论解释和Kripke模型给出的更传统的意义。证明引入这种新颖语义的特征是它是“无点”的事实，即，没有一个宇宙的元素被用来解释逻辑术语。换句话说，术语并不表示某些集合的个体，而是表示将语句的解释保持在一起的“胶水”，类似于形式拓扑中发生的情况。由于所提出的语义学可以平凡地扩展到所有基于直觉主义系统的一阶逻辑理论（并且，稍微注意一下，也可以扩展到最小系统），所以语义学也涵盖了所有的谓词理论，即使这些理论的一些特殊方面应该被注意到。

2013-06-29cs.LOmath.LO

Church-Style和Curry-Style子类型的关系

Relating Church-Style and Curry-Style Subtyping

具有高阶子类型或单例类型的类型论是变量的计算规则受上下文中的类型信息影响的系统的示例。这些系统的一个复杂之处是，在上下文中声明的边界不能很好地与完整性或终止性的逻辑关系证明交互。本文对F-Omega-Sub的类型语法提出了一种自然的修改，将变量的绑定添加到变量类型构造函数中，从而将变量的计算行为与上下文分离。F-Omega-Sub中的子类型算法可以在没有上下文或种类信息的类型上给出。因此，元理论遵循了上下文中没有计算信息的类型系统的一般方法，包括一个简单的逻辑关系定义，而没有上下文的Kripke风格索引。这种新的表示系统被证明是等价于传统的表示没有界限的变量类型构造函数。

2011-01-24cs.LOcs.PL

A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic

In this paper we introduce a term calculus ${\cal B}$ which adds to the affine $λ$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between ${\cal B}$ and the sub-structural logical system which we call "minimal Łukasiewicz logic", also known in the literature as the logic of hoops (a generalisation of MV-algebras). This logic lies strictly in between affine minimal logic and standard minimal logic. We prove that ${\cal B}$ is strongly normalising and has the Church-Rosser property. We also give examples of terms in ${…

2018-09-12cs.LO

关于强规范化语义的约简候选集的完备性

On completeness of reducibility candidates as a semantics of strong normalization

本文定义了一个健全的和完整的语义标准，基于reductioncandidates，强规范化的理论表示在最小的演绎模LA咖喱。使用咖喱风格的证明条款允许建立这一标准的经典概念前海廷代数，并使该标准涉及所有的理论表示最小的演绎模。与使用Church风格的证明项相比，该方法提供了更简单的准则定义和更简单的完备性证明。

2012-02-15cs.LO

带构造函数的类型化λ演算的语义

Semantics of Typed Lambda-Calculus with Constructors

我们提出了一个Curry风格的二阶类型系统，具有并集和交集类型的Arbiser，Miquel和Rios的构造器的λ演算，扩展的λ演算与可变构造器的模式匹配机制。然后，我们证明了强规范化和匹配失败的限制，这个系统的情况下，通过适应标准的reductionmethod。

2011-03-16cs.LO

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

归纳和共归纳计算的全局语义类型

Global semantic typing for inductive and coinductive computing

归纳和共归纳类型通常被解释为本体（教会式）类型，表示规范的数据集，如自然数，列表和流。出于各种目的，特别是在全局语义上下文中研究程序，最好将类型视为语义属性（Curry风格）。内在理论是在20世纪90年代后期引入的，为程序及其语义类型的推理提供了一个纯粹的逻辑框架。在这里，我们将它们扩展到由归纳和共归纳定义的任何组合给出的数据。这种方法是有趣的，因为它与形式逻辑的语法，语义和证明理论基础紧密配合，在隐式计算复杂性以及从证明中提取程序方面具有潜在的应用。我们证明了一个规范性定理，表明程序类型的全球定义，通过通常的（塔斯基）语义的一阶逻辑，同意其操作语义在预期的模型。最后，我们表明，每一个内在的理论是一个保守的一阶算术扩展解释。这意味着对无限数据对象的量化本身不会导致证明理论的强度超过皮亚诺算术。内在理论完全服从于Curry-Howard态射公式，并被用来表征主要的计算复杂性类。

2014-12-24cs.LO

λ演算的证明逻辑

Justification Logic of the Lambda Calculus

Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）

研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。

2026-07-28cs.LOmath.LO

A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction

We introduce Probabilistic Dependent Type Systems (PDTS) via a functional language based on a subsystem of intuitionistic type theory including dependent sums and products, which is expanded to include stochastic functions. We provide a sampling-based semantics for the language based on non-deterministic beta reduction. Further, we derive a probabilistic logic from the PDTS introduced as a direct result of the Curry-Howard isomorphism. The probabilistic logic derived is shown to provide a universal representation for finite discrete distributions.

2016-02-23cs.LOcs.PL

通过幂等交集类型实现强规范性：一种新的语法方法

Strong normalization through idempotent intersection types: a new syntactical approach

Università di Torino（都灵大学）；CONICET—Universidad de Buenos Aires（阿根廷国家科学研究委员会—布宜诺斯艾利斯大学）；Universidad Nacional de Quilmes（基尔梅斯国立大学）

本文提出了一种基于幂等交集类型的语法方法，通过度量证明强规范性，扩展到两种交集类型系统。

2026-02-27cs.LO

Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages

The $\mathitΠ$ family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language, using the language of weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of reversible circuits. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-…

2021-10-11cs.LOcs.PL

基于博弈语义的命令式程序证明

Imperative Programs as Proofs via Game Semantics

游戏语义学将Curry-Howard同构扩展到三种对应：证明，程序，策略。但是策略的范围超出了直觉逻辑和λ演算，它可以捕获有状态的程序。在本文中，我们描述了一个逻辑对应的扩展，证明表示这样的策略。这个系统是表达性的：它包含了直觉线性逻辑的所有连接词和一阶量化。使用Laird的sequoid运算符可以表达具有命令行为的证明。因此，我们可以将一阶直觉线性逻辑嵌入到这个系统中，极化线性逻辑和命令式全程序设计语言。证明系统与一个简单的游戏模型有着紧密的联系，在这个模型中，游戏是游戏的森林。公式被建模为游戏，证明作为历史敏感的获胜策略。我们提供了一个强大的完整的结果，就这个模型：每个有限的战略是一个独特的分析（免割）证明的外延。无限策略对应于无限深度的分析证明。因此，我们可以通过语义规范化证明。

2013-07-08cs.LO

一阶逻辑的博弈语义

Game semantics for first-order logic

我们完善HO/N游戏语义的指针（μ指针）的额外概念，并将其扩展到一阶经典逻辑的完整性结果。我们使用一个教堂风格的扩展Parigot的Mu-演算来表示一阶经典逻辑的证明。我们提出了一些关系Krivine的经典的可实现性和应用类型同构。

2010-10-20cs.LO

基于范畴论的消息传递语言（CaMPL）用于程序员

Categorical Message Passing Language (CaMPL) for programmers

Universidade Federal do Rio de Janeiro（里约热内卢联邦大学）；University of Calgary（卡尔加里大学）；Tallinn University of Technology（塔林科技大学）

CaMPL是一种基于范畴论的并发编程语言，通过类型通信通道实现消息传递，支持受控非确定性、高阶过程和自定义通道类型，确保程序不会死锁或活锁。

2026-05-10cs.DCcs.LOcs.PL

Contextual Modal Types for Algebraic Effects and Handlers

Programming languages with algebraic effects often track the computations' effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a computation as a variable context; consequently, we propose to track algebraic effects of a computation with \emph{contextual modal types}. We develop ECMTT, a novel calculus which tracks algebraic effects by a contextualized variant of the modal $\Box$ (necessity) operator, that it inherits from Contextual Modal Type Theory (CMTT). Whereas type-and-effect systems add effect annotations on top of a prior programming …

2021-08-22cs.LOcs.PL