Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userClassical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
85
0
0.0
(
0
)
Added by
Mathys Rennela
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.
rate research
Read More
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.
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
A genoid is a category of two objects such that one is the product of itself with the other. A genoid may be viewed as an abstract substitution algebra. It is a remarkable fact that such a simple concept can be applied to present a unified algebraic approach to lambda calculus and first order logic.
We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete.
The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
