Richard Moot
We present a proof net calculus for the Displacement calculus and show its correctness. This is the first proof net calculus which models the Displacement calculus directly and not by some sort of translation into another formalism. The proof net calculus opens up new possibilities for parsing and proof search with the Displacement calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We extend the textual calculus for interaction nets by generic rules and propose constraints to preserve uniform confluence. Furthermore, we discuss the implementation of generic rules in the language inets, which is based on the lightweight interaction nets calculus.
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 show how to interpret a language featuring concurrency, references and replication into proof nets, which correspond to a fragment of differential linear logic. We prove a simulation and adequacy theorem. A key element in our translation are routing areas, a family of nets used to implement communication primitives which we define and study in detail.
This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.
We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys a bisimulation result, and is suitable for practical model checking.
We introduce the process calculus Multi-CCS, which extends conservatively CCS with an operator of strong prefixing able to model atomic sequences of actions as well as multiparty synchronization. Multi-CCS is equipped with a labeled transition system semantics, which makes use of a minimal structural congruence. Multi-CCS is also equipped with an unsafe P/T Petri net semantics by means of a novel technique. This is the first rich process calculus, including CCS as a subcalculus, which receives a semantics in terms of unsafe, labeled P/T nets. The main result of the paper is that a class of Mul…
Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that (a) there should be a canonical function from sequent proofs to proof nets, (b) it should be possible to check the correctness of a net in polynomial time, (c) every correct net should be obtainable from a sequent …
Proof Nets for PiL (Full Version)
本文提出PiL的证明网络，扩展了第一阶乘积加法线性逻辑，引入新运算以浅层编码π演算过程。提供正确性准则、序列化过程及证明翻译算法，展示证明网络是序列演算推导的规范表示。
We present a restriction of the solos calculus which is stable under reduction and expressive enough to contain an encoding of the pi-calculus. As a consequence, it is shown that equalizing names that are already equal is not required by the encoding of the pi-calculus. In particular, the induced solo diagrams bear an acyclicity property that induces a faithful encoding into differential interaction nets. This gives a (new) proof that differential interaction nets are expressive enough to contain an encoding of the pi-calculus. All this is worked out in the case of finitary (replication free) …
We offer a simple graphical representation for proofs of intuitionistic logic, which is inspired by proof nets and interaction nets (two formalisms originating in linear logic). This graphical calculus of proofs inherits good features from each, but is not constrained by them. By the Curry-Howard isomorphism, the representation applies equally to the lambda calculus, offering an alternative diagrammatic representation of functional computations.
This paper explores the connection between two central results in the proof theory of classical logic: Gentzen's cut-elimination for the sequent calculus and Herbrands "fundamental theorem". Starting from Miller's expansion-tree-proofs, a highly structured way presentation of Herbrand's theorem, we define a calculus of weakening-free proof nets for (prenex) first-order classical logic, and give a weakly-normalizing cut-elimination procedure. It is not possible to formulate the usual counterexamples to confluence of cut-elimination in this calculus, but it is nonetheless nonconfluent, lending c…
The goal of our Macro Lambda Calculus project (MLC) is to encode lambda terms into interaction nets. Its software implementation will accept input in the notation similar to lambda calculus allowing macro definitions. Output is similar to interaction calculus and is suitable for our Interaction Nets Compiler program (INC). In this paper, we describe the interaction system for call-by-need evaluation and the mechanism of encoding lambda terms into this system which MLC is based on.
To study implementations and optimisations of interaction net systems we propose a calculus to allow us to reason about nets, a concrete data-structure that is in close correspondence with the calculus, and a low-level language to create and manipulate this data structure. These work together so that we can describe the compilation process for interaction nets, reason about the behaviours of the implementation, and study the efficiency and properties.
Linear logic and the linear λ-calculus have a long standing tradition in the study of natural language form and meaning. Among the proof calculi of linear logic, proof nets are of particular interest, offering an attractive geometric representation of derivations that is unburdened by the bureaucratic complications of conventional prooftheoretic formats. Building on recent advances in set-theoretic learning, we propose a neural variant of proof nets based on Sinkhorn networks, which allows us to translate parsing as the problem of extracting syntactic primitives and permuting them into alignme…
The displacement calculus $\mathbf{D}$ is a conservative extension of the Lambek calculus $\mathbf{L1}$ (with empty antecedents allowed in sequents). $\mathbf{L1}$ can be said to be the logic of concatenation, while $\mathbf{D}$ can be said to be the logic of concatenation and intercalation. In many senses, it can be claimed that $\mathbf{D}$ mimics $\mathbf{L1}$ in that the proof theory, generative capacity and complexity of the former calculus are natural extensions of the latter calculus. In this paper, we strengthen this claim. We present the appropriate classes of models for $\mathbf{D}$ …
We interpret Linear Logic Proof Nets in a term language based on Solos calculus. The system includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables to define non-deterministic behaviours and multiparty sessions.
We present a concurrent operational Petri net semantics for the join-calculus, a process calculus for specifying concurrent and distributed systems. There often is a gap between system specifications and the actual implementations caused by synchrony assumptions on the specification side and asynchronously interacting components in implementations. The join-calculus is promising to reduce this gap by providing an abstract specification language which is asynchronously distributable. Classical process semantics establish an implicit order of actually independent actions, by means of an interlea…
The situation calculus logic model is convenient for modelling the actions that can occur in an information system application. The interplay of pre-conditions and post-conditions determines a semantically justified partial order of the defined actions and serves to enforce integrity constraints. This form of specification allows the use of plan-generation algorithms to investigate, before the system is adopted, whether the proposed specification allows all desirable use cases, and effectively disallows undesirable ones. Especially for legacy applications, implemented without a prior specifica…
We present two rewriting systems that define labelled explicit substitution lambda-calculi. Our work is motivated by the close correspondence between Levy's labelled lambda-calculus and paths in proof-nets, which played an important role in the understanding of the Geometry of Interaction. The structure of the labels in Levy's labelled lambda-calculus relates to the multiplicative information of paths; the novelty of our work is that we design labelled explicit substitution calculi that also keep track of exponential information present in call-by-value and call-by-name translations of the lam…
The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the lambda-calculus optimal reduction. Recently Ehrhard and Regnier have introduced an extension of the Multiplicative Exponential fragment of Linear Logic (MELL) that is able to express non-deterministic behaviour of programs and a proofnet-like calculus: Differential Interaction Nets. This paper constructs a proper Geometry of Interaction (GoI) for this extension…
These are the notes for a 5-lecture-course given at ESSLLI 2006 in Malaga, Spain. The URL of the school is http://esslli2006.lcc.uma.es/ . This version slightly differs from the one which has been distributed at the school because typos have been removed and comments and suggestions by students have been worked in. The course is intended to be introductory. That means no prior knowledge of proof nets is required. However, the student should be familiar with the basics of propositional logic, and should have seen formal proofs in some formal deductive system (e.g., sequent calculus, natural ded…
We introduce a new interaction net implementation of optimal reduction for the pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of the interaction net reduction strategy using the approach of so-called token-passing nets and a non-deterministic extension for interaction nets. Another new feature is the read-back mechanism implemented without leaving the formalism of interaction nets.
Handsome proof nets were introduced by Retoré as a syntax for multiplicative linear logic. These proof nets are defined by means of cographs (graphs representing formulas) equipped with a vertices partition satisfying simple topological conditions. In this paper we extend this syntax to multiplicative linear logic with units and exponentials. For this purpose we develop a new sound and complete sequent system for the logic, enforcing a stronger notion of proof equivalence with respect to the one usually considered in the literature. We then define combinatorial proofs, a graphical proof system…
First-order multiplicative intuitionistic linear logic (MILL1) can be seen as an extension of the Lambek calculus. In addition to the fragment of MILL1 which corresponds to the Lambek calculus (of Moot & Piazza 2001), I will show fragments of MILL1 which generate the multiple context-free languages and which correspond to the Displacement calculus of Morrilll e.a.
Since its discovery, differential linear logic (DLL) inspired numerous domains. In denotational semantics, categorical models of DLL are now commune, and the simplest one is Rel, the category of sets and relations. In proof theory this naturally gave birth to differential proof nets that are full and complete for DLL. In turn, these tools can naturally be translated to their intuitionistic counterpart. By taking the co-Kleisly category associated to the ! comonad, Rel becomes MRel, a model of the \Lcalcul that contains a notion of differentiation. Proof nets can be used naturally to extend the…
The original idea of proof nets can be formulated by means of interaction nets syntax. Additional machinery as switching, jumps and graph connectivity is needed in order to ensure correspondence between a proof structure and a correct proof in sequent calculus. In this paper we give an interpretation of proof nets in the syntax of string diagrams. Even though we lose standard proof equivalence, our construction allows to define a framework where soundness and well-typeness of a diagram can be verified in linear time.
$Δ$-Nets: Interaction-Based System for Optimal Parallel $λ$-Reduction
提出Δ-网通用并行计算模型及λ项与Δ-网转换方法，构成最优并行λ-归约算法，解决长期谜题，揭示λ演算与Δ-网关系，突破限制，为高效并行编程语言和计算机架构发展提供可能。
In this paper, we introduce a new interaction net implementation of optimal reduction for pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of interaction net reduction strategy using the approach of so-called token-passing nets. Another new feature is the read-back mechanism also implemented without leaving the formalism of interaction nets.
Proofs as Execution Trees for the π-Calculus
本研究基于演绎即计算范式，为π演算构建新型逻辑框架，通过扩展一阶乘法加法线性逻辑的无切割矢列式演算，将进程对应为公式、证明对应为计算，并设计证明网给出推导的典范表示。
In structural proof theory, designing and working on large calculi make it difficult to get intuitions about each rule individually and as part of a whole system. We introduce two novel tools to help working on calculi using the approach of graph theory and automata theory. The first tool is a Proof Tree Automaton (PTA): a tree automaton which language is the derivation language of a calculus. The second tool is a graphical representation of a calculus called Proof Tree Graph (PTG). In this directed hypergraph, vertices are sets of terms (e.g. sequents) and hyperarcs are rules. We explore prop…
Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process …
Spurious ambiguity is the phenomenon whereby distinct derivations in grammar may assign the same structural reading, resulting in redundancy in the parse search space and inefficiency in parsing. Understanding the problem depends on identifying the essential mathematical structure of derivations. This is trivial in the case of context free grammar, where the parse structures are ordered trees; in the case of categorial grammar, the parse structures are proof nets. However, with respect to multiplicatives intrinsic proof nets have not yet been given for displacement calculus, and proof nets for…
Since proof-nets for MLL- were introduced by Girard (1987), several studies have appeared dealing with its soundness proof. Bellin & Van de Wiele (1995) produced an elegant proof based on properties of subnets (empires and kingdoms) and Robinson (2003) proposed a straightforward generalization of this presentation for proof-nets from sequent calculus for classical logic. In 2014 it was presented an extension of these studies to obtain a proof of the sequentialization theorem for the fragment of N-Graphs with conjunction, disjunction and negation connectives, via the notion of sub-N-Graphs. N-G…
We consider tensor grammars, which are an example of \commutative" grammars, based on the classical (rather than intuitionistic) linear logic. They can be seen as a surface representation of abstract categorial grammars ACG in the sense that derivations of ACG translate to derivations of tensor grammars and this translation is isomorphic on the level of string languages. The basic ingredient are tensor terms, which can be seen as encoding and generalizing proof-nets. Using tensor terms makes the syntax extremely simple and a direct geometric meaning becomes transparent. Then we address the pro…
Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic
研究扩展线性逻辑证明结构正确性标准的性质，提出对证明结构的几何限制使其成为充分性质，引入VMELL片段，将!演算项翻译为证明网，分解λ演算翻译，证明消去切割模拟!归约并给出!演算项的证明网特征。
The elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required, and it is well known that the operational semantics of call-by-value becomes problematic in this case. Here we study the intermediate setting -- that we call Open Call-by-Value -- of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. Various calculi for Open Call-by-Value already exist, each on…
Thirty years ago, I introduced a non-commutative variant of classical linear logic, called "pomset logic", issued from a particular categorical interpretation of linear logic known as coherence spaces. In addition to the usual commutative multiplicative connectives of linear logic, pomset logic includes a non-commutative connective, "$\triangleleft$" called "before", associative and self-dual: $(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$. The conclusion of a pomset logic proof is a Partially Ordered MultiSET of formulas. Pomset logic enjoys a proof net calculus with cut-elimination…
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view it suggests a compact representation of proofs in classical first- and higher-order logic by recording the information which instances have been chosen for which quantifiers, known in the literature as expansion trees. Such a representation is inherently analytic and hence corresponds to a cut-free sequent calculus proof. Recently several extensions of such proof representations to proofs with cut have been proposed. These extensions are based on graphical formalisms similar to proof nets and …
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
本文提出指数替换演算（ESC），基于显式替换思想为IMELL切割消除提供新表示，设计了具有子项性质的切割消除策略，首次为无约束指数的切割消除提供多项式代价模型，并证明了无类型合流与有类型强规范化。
We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indexes, which allows us to extend Girard's systems while keeping the same complexity properties. In particular, it turns out that Girard's syste…
The exponential logic of sequentialization
本文通过将跳跃机制内化到乘法线性逻辑（MLL）的扩展中，引入跳跃公式约束图的序列化过程，揭示了序列化的指数逻辑。
Logic Programming with Multiplicative Structures
本文研究纯乘法片段下基于证明网构造的逻辑编程框架，展示如何仅用资源保持且上下文无关的广义乘法操作实现上下文敏感方法，并证明部分方法超出线性逻辑MLL片段。
Infrared Safety from ZX-Diagrams: A Categorical Proof of Soft-QED as Open Quantum System
利用丢弃ZX演算给出QED红外发散的Bloch-Nordsieck抵消的非微扰范畴证明，将软光子视为开放量子系统的环境，通过图论恒等式验证了软光子定理和退相干效应。
Maintaining data consistency among multiple parties requires nodes to repeatedly send data to all other nodes. For example, the nodes of a blockchain network have to disseminate the blocks they create across the whole network. The scientific literature typically takes the ideal perspective that such data distribution is performed by broadcasting to all nodes directly, while in practice data is distributed by repeated multicast. Since correctness and security of consistency maintenance protocols usually have been established for the ideal setting only, it is vital to show that these properties …
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。