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 still have the same proof nets representation---a further result is the characterisation of the equality induced by proof nets over terms with sharing. Finally, such a detailed analysis of the relationship between terms and proof nets, suggests a new, abstract notion of proof net, based on rewriting considerations and not necessarily of a graphical nature.
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.
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.
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…
We present a method for hierarchically generating sound workflow nets by substitution of nets with multiple inputs and outputs. We show that this method is correct and generalizes the class of nets generated by other hierarchical approaches. The method involves a new notion of soundness which is preserved by the generalized type of substitution that is presented in this paper. We show that this notion is better suited than *-soundness for use with the presented type of generalized substitution, since {*}-soundness is not preserved by it. It is moreover shown that it is in some sense the optima…
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 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.
This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this calculus provides a cumbersome encoding of substitution composition, an operation that is important to the efficient realization of reduction. This encoding is simplified here, resulting in a treatment that is easy to use directly in applications. The rationalization consists of the elimination of a practically inconsequential flexibility in the unravelling of…
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.
We present a full formalization in Martin-Löf's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple substitution. Our formalization is based on a proof by Ryo Kashima, in which a notion of beta-reducibility with a standard sequence is captured by an inductive relation. The proof uses only structural induction over the syntax and the relations defined, which is possible due to the specific formulation of substitution that we employ. The whole development has bee…
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 …
SBV is a deep inference system that extends the set of logical operators of multiplicative linear logic with the non commutative operator Seq. We introduce the logical system SBVr which extends SBV by adding a self-dual atom-renaming operator to it. We prove that the cut elimination holds on SBVr. SBVr and its cut free subsystem BVr are complete and sound with respect to linear lambda calculus with explicit substitutions. Under any strategy, a sequence of evaluation steps of any linear lambda-term M becomes a process of proof-search in SBVr (BVr) once M is mapped into a formula of SBVr. Comple…
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) …
Hereditary substitution is a form of type-bounded iterated substitution, first made explicit by Watkins et al. and Adams in order to show normalization of proof terms for various constructive logics. This paper is the first to apply hereditary substitution to show normalization of a type theory corresponding to a non-constructive logic, namely the lambda-Delta calculus as formulated by Rehof. We show that there is a non-trivial extension of the hereditary substitution function of the simply-typed lambda calculus to one for the lambda-Delta calculus. Then hereditary substitution is used to prov…
The intrinsic treatment of binding in the lambda calculus makes it an ideal data structure for representing syntactic objects with binding such as formulas, proofs, types, and programs. Supporting such a data structure in an implementation is made difficult by the complexity of the substitution operation relative to lambda terms. In this paper we present the suspension calculus, an explicit treatment of meta level binding in the lambda calculus. We prove properties of this calculus which make it a suitable replacement for the lambda calculus in implementation. Finally, we compare the suspensio…
In this paper we introduce a typed, concurrent $λ$-calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we recover strong normalization. The proof is based on a reducibility technique and an original interactive property reminiscent of the Game Semantics approach.
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…
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 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.
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…
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.
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…
$λ\upsilon$ is an extension of the $λ$-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of $λ\upsilon$ focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for $λ\upsilon$-terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random $λ\upsilon$-terms. We show that typical $λ\upsilon$-terms represent, in a strong sense, non-strict computations in the classic $λ$-calculus. Moreover, typically almost …
This paper introduces a new proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured ex…
Substitution resolution supports the computational character of $β$-reduction, complementing its execution with a capture-avoiding exchange of terms for bound variables. Alas, the meta-level definition of substitution, masking a non-trivial computation, turns $β$-reduction into an atomic rewriting rule, despite its varying operational complexity. In the current paper we propose a somewhat indirect average-case analysis of substitution resolution in the classic $λ$-calculus, based on the quantitative analysis of substitution in $λ\upsilon$, an extension of $λ$-calculus internalising the $\upsil…
We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then design generic tools to construct admissible monad morphismsfrom basic data. These tools automate ubiquitous standard patternslike (1) defining auxiliary functions in successive, potentiallydependent layers, and (2) proving properties of auxiliary functions byinduction on syntax. We cover significant examples from theliterature, including the standard lambda-calculus withcapture-avoiding substitution, a lambda-calculu…
We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$λ$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $$λ$$-calculus equipped with a type system equivalent to classical second-order predicate logic, representing one step towards proving the normalization of the call-by-need classical second-order arithm…
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…
Inspired by a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda j, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and derelicition. First, we prove some fundamental properties of lambda j such as confluence and preservation of beta-strong normalisation. Second, we add a strong bisimulation to lambda j by means of an equational theory which captures in particular Regnier's sigma-equivalence. We then complete this bisimulati…
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.
This paper introduces a new term rewriting system that is similar to the embedded read-back mechanism for interaction nets presented in our previous work, but is easier to follow than in the original setting and thus to analyze its properties. Namely, we verify that it correctly represents the lambda calculus. Further, we show that there is exactly one reduction sequence that starts with any term in our term rewriting system. Finally, we represent the leftmost strategy which is known to be normalizing.
This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinar…
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…
Algebraic Petri nets are a formalism for modeling distributed systems and algorithms, describing control and data flow by combining Petri nets and algebraic specification. One way to specify correctness of an algebraic Petri net model $N$ is to specify a linear equation $E$ over the places of $N$ based on term substitution, and coefficients from an abelian group $G$. Then, $E$ is valid in $N$ iff $E$ is valid in each reachable marking of $N$ . Due to the expressive power of Algebraic Petri nets, validity is generally undecidable. Stable linear equations form a class of linear equations for whi…
Recent work on combinatory logic demonstrates a compositional translation from lambda calculus that gives meaning to open terms. As the meaning of open terms is a key difficulty in the study of metaprogramming, we investigate whether this idea can be extended to metaprogramming systems with hygienic and unhygienic substitution, specifically $λ_{e}^{\rightarrow \Box}$ and $λ_{\mathcal{S}}$. We conclude that there is quantitative evidence to support the claim that metaprogramming with unhygienic substitution is more powerful than metaprogramming with hygienic substitution.
In this paper, we present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. We first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. We then present a weak head normalization procedure which performs both substitutions lazily and in a single pass thereby combining substitution walks for the two different classes of variables. Finally, we describe a bidirectional type checki…
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.
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…
In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda calculus with explicit substitution. All three calculi enable explicit control of resources due to the presence of weakening and contraction operators. Along this journey, we propose intersection type assignment systems for all three resource control calculi. We recognise the need for three kinds of variables all requiring different kinds of intersection types. Our main contribution is the characterisation of strong normalisation o…
In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easily proved, only one of them is usually established (and sometimes none). We propose here a connection between them which helps to get SN when one already has PSN. For this purpose, we formalize a general proof technique of SN which consists in expanding substitutions into "pure" lambda-terms and to inherit SN of the whole calculus by SN of the "pure" calculus and by PSN. We apply it successfully to a large set of calc…
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL. Our formalization is based on work by Stefan Berghofer, which we have since updated to use Isabelle's declarative proof style Isar (Archive of Formal Proofs, Entry FOL-Fitting, August 2007 / July 2018). We represent variables with de Bruijn indices; this makes subst…
Utrecht Institute of Linguistics OTS, Utrecht University（乌得勒支大学乌得勒支语言学研究所OTS）；LIRMM, Université de Montpellier, CNRS（法国国家科学研究中心蒙彼利埃大学计算机信息与机器人微电子实验室）
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…
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…
This article is devoted to the presentation of lambda_rex, an explicit substitution calculus with de Bruijn indexes and a simple notation. By being isomorphic to lambda_ex - a recent formalism with variable names -, lambda_rex accomplishes simulation of beta-reduction (Sim), preservation of beta-strong normalization (PSN) and meta-confluence (MC), among other desirable properties. Our calculus is based on a novel presentation of lambda_dB, using a swap notion that was originally devised by de Bruijn. Besides lambda_rex, two other indexed calculi isomorphic to lambda_x and lambda_xgc are presen…
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…
