Normalisation of a Non-deterministic Type Isomorphic λ-calculus
Alejandro Díaz-Caro, Gilles Dowek
我们提供了一个强规范化的证明lambda+，最近推出的，明确类型的，非确定性的Alzida演算同构命题被确定。这样的证明是一个非平凡的适应约简候选人技术。
We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Such a proof is a non-trivial adaptation of the reducibility candidates technique.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We define a fragment of propositional logic where isomorphic propositions, such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
线性-代数演算和代数演算是用任意线性组合项扩展的无类型代数代数演算。前者以重写系统的形式呈现线性代数的公理，而后者使用等式。当重写时，代数演算不是融合的，除非增加进一步的限制。我们提供了一个类型系统的线性代数演算强制执行强规范化，这给回汇合。类型系统允许在系统F中进行抽象解释。
Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
受最近基于线性逻辑技术的λ演算的图形化形式的启发，我们引入了一种无类型的结构λ演算，称为λ j，它将距离上的动作与指数规则相结合，通过弱化、收缩和消除来分解替换.首先，我们证明了一些基本性质的lambda j，如合流和保存的β-强规范化。第二，我们添加了一个强大的互模拟λ j通过一个方程的理论，特别是捕获Regnier的西格玛等价。然后，我们完成了这两个以上的方程的互模拟（去）组成的替代品，我们证明，由此产生的演算仍然保持β-强规范化。最后，我们讨论了我们的结果的一些后果。
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Curien和Herbelin的λ mu mu-演算的按名称调用版本的直观片段被隔离，并通过嵌入到简单类型的λ mu-演算中来证明其强规范化。我们的嵌入是一个延续和垃圾传递风格的翻译，灵感来自Ikeda和Nakazawa的Parigot的λ\_mu演算的翻译。嵌入严格模拟约简，而通常的连续传递式转换删除置换约简步骤。对于我们的直觉主义微积分，我们甚至只需要传递“垃圾单元”。我们将同样的方法应用于其他演算，即简单类型演算的连续扩展导致我们的直觉系统，并且已经对于我们考虑的最简单的扩展（具有广义应用的演算），这产生了通过约简保持嵌入的强规范化的第一个证明。所得到的结果扩展到第二和更高的阶结石。
This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper the analysis is refined further by considering intensional Kripke relations (in the form of Artin glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of …
Non-idempotent intersection types and strong normalisation
我们提出了一个非幂等交集类型的分类系统，给出了一个包含纯λ-演算、显式替换演算λS和显式替换、压缩和弱化演算λlxr的术语语法.在这三个演算中，一个项是可类型的，当且仅当它是强正规化的，就像在（许多）具有幂等交集的系统中一样。非幂等性将额外的信息引入到类型树中，例如最长约简序列上的简单边界将项约简到其范式。强规范化遵循，而不需要还原技术。利用这一点，我们重新审视了基于交集类型过滤器的λ演算模型，并将其扩展到λS和λlxr。非幂等性简化了一种基于这种过滤器模型的方法，该方法为众所周知的类型系统（例如系统F）产生强规范化的模块化证明。我们还提出了一个过滤器模型，通过正交技术，即作为一个实例的抽象概念的正交模型在本文中正式和经典的可实现性的启发。与其他基于项的实例（其中一个改写了λ演算强规范化的标准证明）相比，基于过滤器的实例在证明λS和λlxr的强规范化结果方面表现得更好。最后，从我们的类型树中读取的最长约简序列的边界被细化为一个精确的度量，从一个特定的类型树（称为主树）中读取;在三个演算中的每一个中，都标识了这样长度的特定约简序列。在λ-演算的情况下，对于最长约化序列，这个复杂性结果是de Carvalho对于线性头约化序列的结果的对应。
A key result in the theory of the modal mu-calculus is the disjunctive normal form theorem by Janin & Walukiewicz, stating that every mu-calculus formula is semantically equivalent to a so-called disjunctive formula. These disjunctive formulas have good computational properties and play a pivotal role in the theory of the modal mu-calculus. It is therefore an interesting question what the best normalisation procedure is for rewriting a formula into an equivalent disjunctive formula of minimal size. The best constructions that are known from the literature are automata-theoretic in nature and c…
We present intersection type systems in the style of sequent calculus, modifying the systems that Valentini introduced to prove normalisation properties without using the reducibility method. Our systems are more natural than Valentini's ones and equivalent to the usual natural deduction style systems. We prove the characterisation theorems of strong and weak normalisation through the proposed systems, and, moreover, the approximation theorem by means of direct inductive arguments. This provides in a uniform way proofs of the normalisation and approximation theorems via type systems in sequent…
On the Simply-Typed Functional Machine Calculus: Categorical Semantics and Strong Normalisation
本文研究函数机器演算（FMC）的范畴语义与强正规化，证明其在适当等式理论下对应自由笛卡尔闭范畴，并扩展 Gandy 证明以确立带类型 FMC 项的强正规化性质。
Strong Normalisation for Asynchronous Effects
本文研究了异步效果核心算法规则的强归约性质，证明去除一般递归后仍强归约，且在引入受控中断递归行为时仍保持强归约。
Semantics of Typed Lambda-Calculus with Constructors
我们提出了一个Curry风格的二阶类型系统，具有并集和交集类型的Arbiser，Miquel和Rios的构造器的λ演算，扩展的λ演算与可变构造器的模式匹配机制。然后，我们证明了强规范化和匹配失败的限制，这个系统的情况下，通过适应标准的reductionmethod。
A new coinductive confluence proof for infinitary lambda calculus
本文提出了无穷λ演算中Böhm归约合流性与规范化的新余归纳证明，该证明更简单且技术新颖，并在Coq中形式化验证。
Resource control and strong normalisation
我们介绍了\emph{resource control cube}，一个系统，由八个直观的lambda演算与资源的隐式或显式控制，无论是自然演绎或自然演算。本文介绍了Kesner和Renaud提出的与自然演绎对应的四种立方体演算，以及与λ演算对应的四种立方体演算。该演示文稿是参数化的一组资源（削弱或收缩），这使得一个统一的治疗的八个结石的立方体。简单类型的资源控制立方体一方面将Curry-Howard对应扩展为具有隐式或显式结构规则的直觉自然演绎和直觉推理逻辑，另一方面又与子结构逻辑相关。我们提出了一个通用的交叉型系统的资源控制立方体演算。我们的主要贡献是一个强大的归一化减少在这个立方体的特征。首先，我们证明了可类型性意味着强规范化的“自然演绎基地”的立方体，通过适应reductionmethod。然后，我们证明了可类型性意味着强规范化的“cubes基地”的立方体，通过使用一个组合良好的订单和一个合适的嵌入在“自然演绎基地”。最后，我们证明了强规范化意味着在立方体中使用头部主题扩展的可键入性。所有的证明都是通用的，并且可以通过实例化资源集来针对立方体的每个演算。
Linearity in the non-deterministic call-by-value setting
我们考虑了按值调用λ演算的非确定性扩展，它对应于线性代数λ演算的加法片段。我们定义了一个细粒度的类型系统，捕捉这种形式主义中存在的正确线性。在证明了主题还原和强规范化属性之后，我们提出了将该演算翻译成具有对的系统F，其对应于线性逻辑的非线性片段。翻译提供了一个更深入的了解线性在我们的设置。
Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic
本文建立了直觉主义非交换逻辑的自然演绎或λ演算公式的规范化--它同时涉及交换和非交换连接词。这种演算首先介绍了德格罗特，而不是经典版本的Abrusci和Ruet承认充分熵，允许为了放宽到任何suborder。我们的结果还包括，作为一个特殊的情况下，正常化的自然演绎Lambek演算的产品，这是不足为奇的，但尚未证明。对于全熵的直觉非交换逻辑，至今没有一个证明网语法;对于语言应用，与自然演绎或多或少等价的逻辑演算由于缺乏标准的Curry-Howard同构而不方便。
Superdeduction in Lambda-Bar-Mu-Mu-Tilde
超级演绎是一种专门设计的方法，以简化谓词逻辑中一阶理论的使用。运用这一理论，以系统、正确、完整的方式，用新的演绎规则丰富演绎体系。一个证明项语言和一个切消约化已经存在于超演绎中，两者都是基于克里斯蒂安·厄本在经典微积分上的工作。然而，克里斯蒂安·厄本的微积分的计算内容与柯里-霍华德对应（Curry-Howard correspondence）没有直接关系。相反，Lambda bar mu mu波浪线演算是经典波浪线演算的一种波浪线演算。这个简短的文件是第一步，进一步探索的计算内容的superdeduction证明，我们延长了Lambda酒吧亩亩波浪演算，以获得一个proofterm语言一起削减消除减少superdeduction。我们还证明了强大的规范化，这种扩展的λ酒吧亩亩波浪演算。
Milner's Lambda-Calculus with Partial Substitutions
研究 Milner 的带部分替换的 lambda 演算，证明其合流性、强规范化保持性，并借助交集类型刻画强可规范化项，且与相关演算及证明网建立联系。
Characterisation of Strongly Normalising lambda-mu-Terms
我们提供了一个强规范化的条款，通过一个类型系统，使用交集和产品的类型的Euda-mu演算的表征。后者的存在和限制使用的类型欧米茄使我们能够代表特定的概念，继续在文献中使用的定义的语义的Muda-mu-演算。这使得有可能将强规范化的Arnda-terms的众所周知的特征化属性-使用交集类型-提升到Arnda-mu-演算。从这一结果的另一种证明强规范化的条款类型在Parigot的命题逻辑系统如下，通过解释该系统到我们的。
The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions of strictness. To obtain infinitary normalisation and infinitary confluence properties for these calculi, Kennaway et al. extend $β$-reduction with infinitely many `$\bot$-rules', which contract meaningless terms directly to $\bot$. Three of the resulting Böhm reduction calculi have unique infinitary normal forms corresponding to Böhm-like trees. In this paper…
Jeřábek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek's result: we give a quasipolynomial-time cut-elimination procedure for classical propositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are bo…
We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a call-by-name language whereas the latter is call-by-value; the former considers algebraic equalities whereas the latter approaches them through …
Computational interpretation of classical logic with explicit structural rules
我们提出了一个演算提供了一个Curry-Howard对应的经典逻辑中所表示的显式的结构规则，即弱化和收缩演算。这些结构规则分别引入了明确的删除和重复的条款。我们提出了一个类型系统，我们证明了类型保持下减少。详细研究了它与经典微积分之间的一种相互关系，这种关系具有隐含的结构规则。从这个分析中，我们得到强归一化性质。
This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But in contrast to [BKRDR15], our (static) systems also provides quantitative information about the dynamics of the calculus. Indeed, syste…
We present a novel lambda calculus that casts the categorical approach to the study of quantum protocols into the rich and well established tradition of type theory. Our construction extends the linear typed lambda calculus with a linear negation of "trivialised" De Morgan duality. Reduction is realised through explicit substitution, based on a symmetric notion of binding of global scope, with rules acting on the entire typing judgement instead of on a specific subterm. Proofs of subject reduction, confluence, strong normalisation and consistency are provided, and the language is shown to be a…
A Theory of Explicit Substitutions with Safe and Full Composition
已经提出了许多不同的系统与显式替代实现了一个大类的高阶语言。本文的第一部分调查的动机和挑战，指导这种演算的功能框架的发展。然后，非常简单的技术在命名变量风格的符号是用来建立一个理论的显式替代的Alzada演算享有一整套有用的属性，如完整的组成，模拟一步β-减少，保存β-强规范化，强规范化的类型条款和汇合元术语。相关结石的规范化也进行了讨论。
On the semantics of proofs in classical sequent calculus
本文探讨了经典矢列演算中对称切割归约过程的非平凡不变量问题，证明GS4中公理诱导图在规则排列下保持不变，并据此设计了一种规则排列归约为恒等式的新证明系统。
This work exploits the logical foundation of session types to determine what kind of type discipline for the pi-calculus can exactly capture, and is captured by, lambda-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session pi-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the…
A Strongly Normalising System of Dependent Types for Transparent and Opaque Probabilistic Computation
本文提出一种依赖类型系统，支持透明和不透明概率计算，并通过类型系统形式化可信性概念。
System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding isomorphisms. We provide non-standard proofs of subject reduction and strong normalisation, extending those of System I.
Since the very beginning of the theory of linear logic it is known how to represent the $λ$-calculus as linear logic proof nets. The two systems however have different granularities, in particular proof nets have an explicit notion of sharing---the exponentials---and a micro-step operational semantics, while the $λ$-calculus has no sharing and a small-step operational semantics. Here we show that the \emph{linear substitution calculus}, a simple refinement of the $λ$-calculus with sharing, is isomorphic to proof nets at the operational level. Nonetheless, two different terms with sharing can s…
In this paper we investigate the $λ$ -calculus, a $λ$-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and con-traction rules in the type assignment system. We introduce directly the class of $λ$ -terms and we provide a new treatment of substitution by its decompo-sition into atomic steps. We propose an intersection type assignment system for $λ$ -calculus which makes a clear correspondence between three roles of variables and three kinds of intersection types. Finally, we provid…
A journey through resource control lambda calculi and explicit substitution using intersection types (an account)
在本文中，我们邀请读者通过三个lambda演算与资源控制的旅程：lambda演算，lambda演算和lambda演算与显式替换。由于弱化和收缩运算符的存在，这三种演算都可以显式控制资源。在这个过程中，我们提出了所有三个资源控制演算的交集型分配系统。我们认识到需要三种变量都需要不同类型的交叉点类型。我们的主要贡献是在所有三个结石的减少强规范化的特点，使用的技术reductionary，头部主题扩展，以及订单和适当的嵌入的条款相结合。
An Algebraic Extension of Intuitionistic Linear Logic: The $L_!^S$-Calculus and Its Categorical Model
本文提出$L_!^S$-演算作为直觉线性逻辑的证明语言，通过标量乘法和项加法实现线性性的语法表达，并在范畴模型中提供语义解释。
A System F accounting for scalars
代数演算和线性代数演算扩展了代数演算，使其可以进行任意的线性组合。在本文中，我们提供了一个细粒度的，系统F型系统的线性代数演算。我们表明，这个“标量”型系统享有的主题还原属性和强规范化属性，我们的主要技术成果。后者产生了一个显着的简化的线性代数微积分本身，通过消除需要的一些限制，在其减少规则。但是，这个标量类型系统更重要的原始特性是，它跟踪每个术语中存在的“类型的数量”。作为一个使用的例子，我们证明了它可以保证一个项的范式是重心的，即它的标量和为1。
Diagrammatic techniques for reasoning about monoidal categories provide an intuitive understanding of the symmetries and connections of interacting computational processes. In the context of categorical quantum mechanics, Coecke and Kissinger suggested that two 3-qubit states, GHZ and W, may be used as the building blocks of a new graphical calculus, aimed at a diagrammatic classification of multipartite qubit entanglement that would highlight the communicational properties of quantum states, and their potential uses in cryptographic schemes. In this paper, we present a full graphical axiomati…
Justification Logic of the Lambda Calculus
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
Swapping: a natural bridge between named and indexed explicit substitution calculi
这篇文章致力于介绍lambda_rex，一个显式的替代演算与de Bruijn指数和一个简单的符号。通过与lambda_ex（一种最近的变量名称形式）同构，lambda_rex实现了beta-约简（Sim）的模拟，beta-强归一化（PSN）和元融合（MC）的保留，以及其他理想的属性。我们的演算基于lambda_dB的一种新的表示，使用了最初由de Bruijn设计的交换概念。除了lambda_rex，另外两个索引演算同构的lambda_x和lambda_xgc，展示了我们的技术应用于设计的索引版本的已知命名演算的潜力。
Continuation-passing Style Models Complete for Intuitionistic Logic
一类模型，在连续单子的形式多态的一阶个人，这是健全的和完整的最小直觉谓词逻辑。证明的健全性和完整性是建设性的，其组成的计算内容，特别是一个$β$ -规范化的评估程序简单类型的lambda演算和类型。虽然灵感来自Danvy的类型导向部分求值器，但避免了分隔控制运算符（即计算效果）的必要使用。多态性的作用是至关重要的--去掉它可以让我们获得经典谓词逻辑的模型完备的概念。我们的模型和克里普克模型之间的联系是通过加强双重否定转移图式来实现的。
A formalization of System I with type Top in Agda
本文提出带有类型Top的System I变种，并用Agda形式化了该算术，包含进度和强归约的证明。
This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the …
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. Th…
This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the characterisation of retraction in the standard intersection types is discussed.
The good properties of Plotkin's call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate, and the literature contains a number of proposals. Recently, Accattoli and Guerrieri provided detailed operational and implementative studies of these proposals, showing that they are equivalent from the point of view of termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-…
A quantum let within the lambda calculus
针对λ_ρ^∘量子λ演算因缺乏张量消除结构而表达能力受限的问题，本文利用泡利分解与谱分解提出量子let结构扩展该演算，证明其多项理论性质，以符合物理原理的方式恢复了量子比特丢弃能力与表达能力。
Toward Isomorphism of Intersection and Union types
本文研究了具有交和并类型的代数演算的类型同构。众所周知，在微积分中，两种类型之间的同构是由一对相互逆的项实现的。值得注意的是，可逆项是特定形状的线性项，称为有限遗传置换子。然后，在线性项的交、并类型的相关类型推断系统中，研究了有限遗传置换子的类型性质。特别地，定义了类型之间的同构保持约简。类型归约是汇合的和终止的，并引入了类型的范式的概念。正规类型的性质是完全刻画类型同构的关键一步。本文的主要结果是，一方面证明了具有相同范式的两个类型是同构的，另一方面证明了在范式中两个类型之间同构的特征，箭型的模同构。
Type Theory with Single Substitutions
本文为类型理论定义了仅含单一替换和弱化的单一替换演算（SSC），证明了其语法与带族范畴（CwF）语法同构，为定义类型理论提供了极简替代方案。
On the Taylor expansion of $λ$-terms and the groupoid structure of their rigid approximants
本文改进了泰勒展开范式与Böhm树同构的证明，简化步骤、引入群胚结构并扩展至非确定性设置，保留均匀性。
We propose an implementation of lambda+, a recently introduced simply typed lambda-calculus with pairs where isomorphic types are made equal. The rewrite system of lambda+ is a rewrite system modulo an equivalence relation, which makes its implementation non-trivial. We also extend lambda+ with natural numbers and general recursion and use Bekić's theorem to split mutual recursions. This splitting, together with the features of lambda+, allows for a novel way of program transformation by reduction, by projecting a function before it is applied in order to simplify it. Also, currying together w…
Lambda calculi with algebraic data types lie at the core of functional programming languages and proof assistants, but conceal at least two fundamental theoretical problems already in the presence of the simplest non-trivial data type, the sum type. First, we do not know of an explicit and implemented algorithm for deciding the beta-eta-equality of terms---and this in spite of the first decidability results proven two decades ago. Second, it is not clear how to decide when two types are essentially the same, i.e. isomorphic, in spite of the meta-theoretic results on decidability of the isomorp…
ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
提出ZX-演算，通过迹索引类型、预层非单调语义和构造性AGM信念修正，保守扩展Martin-Löf依赖类型论，并给出Coq机械化证明。
Extensional proofs in a propositional logic modulo isomorphisms
本文通过向系统I添加η-展开规则，去除了变量类型限制，构造出兼具强归一化与完整引入性质的命题逻辑证明演算。
This volume contains a final and revised selection of papers presented at the Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), held in Vienna (Austria) on July 18th, affiliated with TLCA 2014, Typed Lambda Calculi and Applications (held jointly with RTA, Rewriting Techniques and Applications) as part of FLoC and the Vienna Summer of Logic (VSL) 2014. Intersection types have been introduced in the late 1970s as a language for describing properties of lambda calculus which were not captured by all previous type systems. They provided the first characterisation of strongly …
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。