Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCategorical models of Linear Logic with fixed points of formulas
130
0
0.0
(
0
)
Added by
Thomas Ehrhard
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Authors
Thomas Ehrhard
Ask ChatGPT about the research
No Arabic abstract
We develop a denotational semantics of muLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baeldes propositional muMALL with exponentials. Our general categorical setting is based on the notion of Seely category and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving them, least and greatest fixed points have distinct interpretations. This latter model shows that muLL enjoys a denotational form of normalization of proofs.
rate research
Read More
We develop a denotational semantics of Linear Logic with least and greatest fixed points in coherence spaces (where both fixed points are interpreted in the same way) and in coherence spaces with totality (where they have different interpretations). These constructions can be carried out in many different denotational models of LL (hypercoherences, Scott semantics, finiteness spaces etc). We also present a natural embedding of G{o}del System T in LL with fixed points thus enforcing the expressive power of this system as a programming language featuring both normalization and a huge expressive power in terms of data types.
Linear Logic was introduced by Girard as a resource-sensitive refinement of classical logic. It turned out that full propositional Linear Logic is undecidable (Lincoln, Mitchell, Scedrov, and Shankar) and, hence, it is more expressive than (modalized) classical or intuitionistic logic. In this paper we focus on the study of the simplest fragments of Linear Logic, such as the one-literal and constant-only fragments (the latter contains no literals at all). Here we demonstrate that all these extremely simple fragments of Linear Logic (one-literal, $bot$-only, and even unit-only) are exactly of the same expressive power as the corresponding fu
Categorical quantum mechanics exploits the dagger-compact closed structure of finite dimensional Hilbert spaces, and uses the graphical calculus of string diagrams to facilitate reasoning about finite dimensional processes. A significant portion of quantum physics, however, involves reasoning about infinite dimensional processes, and it is well-known that the category of all Hilbert spaces is not compact closed. Thus, a limitation of using dagger-compact closed categories is that one cannot directly accommodate reasoning about infinite dimensional processes. A natural categorical generalization of compact closed categories, in which infinite dimensional spaces can be modelled, is *-autonomous categories and, more generally, linearly distributive categories. These notes start the development of this direction of generalizing categorical quantum mechanics. An important first step is to establish the behaviour of the dagger in these more general settings. Thus, these notes simultaneously develop the categorical semantics of multiplicative dag-linear logic. The notes end with the definition of a mixed unitary category. It is this structure which is subsequently used to extend the key features of categorical quantum mechanics.
We develop a fixed-point extension of quantitative equational logic and give semantics in one-bounded complete quantitative algebras. Unlike previous related work about fixed-points in metric spaces, we are working with the notion of approximate equality rather than exact equality. The result is a novel theory of fixed points which can not only provide solutions to the traditional fixed-point equations but we can also define the rate of convergence to the fixed point. We show that such a theory is the quantitative analogue of a Conway theory and also of an iteration theory; and it reflects the metric coinduction principle. We study the Bellman equation for a Markov decision process as an illustrative example.
Process calculi based on logic, such as $pi$DILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the $pi$-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. (2019) introduced Hypersequent Classical Processes (HCP), which addresses this mismatch using hypersequents (collections of sequents) to register parallelism in the typing judgements. However, the step from CP to HCP is a big one. As of yet, HCP does not have reduction semantics, and the addition of delayed actions means that CP processes interpreted as HCP processes do not behave as they would in CP. We introduce HCP-, a variant of HCP with reduction semantics and without delayed actions. We prove progress, preservation, and termination, and show that HCP- supports the same communication protocols as CP.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
