What is it about?
We motivate the problem by explaining why self-dual nominal quantifiers are not suited to modelling fresh names in languages with parallelism, such as the nu construct in the pi-calculus. This argument applies when we adopt a processes as formulae approach to modelling processes, where the constructs of the process language are embedded directly as formula in a logic specially designed for this purpose. The resulting logical system introduced extends the established systems MALL1 with mix (linear logic with additives modelling choices and first-order quantifiers which can model input binders) and BV (a system with a non-commutative operator that can model causal dependencies, i.e., a ``happens before'' relation). By adding also the pair of nominal quantifiers, we obtain a richly expressive system that is none-the-less decidable. The bulk of the paper is dedicated to proving cut elimination --- the cornerstone result of a proof system. The main technique used is the splitting technique. This technique basically checks all ways in which operators can commute and interact with each other as we normalise a proof. Due to the large number of operators in the system, this is the largest splitting proof conducted in the literature. It is also the first splitting proof for first-order quantifiers and, since all cut elimination proofs in the presence of BV of this kind so far require splitting at some point, it is the first cut elimination proof for a system where first-order quantifiers and the ``happens before'' relation coexist.
Featured Image
Why is it important?
We introduce and provide motivation for a new pair of nominal operators. Nominal quantifiers provide a scoping mechanism for fresh names, but previously such quantifiers have been self-dual. We show the splitting technique, a key ingredient used to prove cut elimination in deep inference, can be applied in this rich setting. Deep inference is required to define systems admitting a cut elimination result in this branch of non-commutative logic. We establish a foundation for modelling rich processes directly in logic as formulae. Here implication is a process preorder sensitive to the underlying partial-order structure of processes, which is a semantics difficult to achieve using regular methods for providing semantics to process calculi with names.
Perspectives
The logical system MAV1 can be used to reason about useful process models. However, it can benefit from being extended still further to match the power of processes in calculi such as applied pi-calculus which exchange more than just channel names when they send and receive messages. E.g., we should be able to account for the fact that formulae modelling two processes that send different encrypted messages using keys that have not been shared may be considered to be equivalent. Another beneficial modelling feature would be to allow operators that can model unbounded sessions, noting that such features likely require more than splitting in order to prove cut elimination. An initial investigation and discussion on the semantics of MAV1, from a process calculus perspective, is conducted in the following companion paper. Constructing weak simulations from linear implications for processes with private names. R Horne, A Tiu. Mathematical Structures in Computer Science 29 (8), 1275-1308. 2019
Ross Horne
Universite du Luxembourg
Read the Original
This page is a summary of: De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic, ACM Transactions on Computational Logic, October 2019, ACM (Association for Computing Machinery),
DOI: 10.1145/3325821.
You can read the full text:
Resources
Constructing Weak Simulations from Linear Implications for Processes with Private Names
This is a companion paper proving that implication in the logic defines a form of simulation preorder.
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
Open access version on arXiv, incorporating full proofs.
Contributors
The following have contributed to this page
