Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality.
This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.
Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality.
This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.
Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.
The standard model of quantum circuits assumes operations are applied in a fixed sequential “causal” order. In recent years, the possibility of relaxing this constraint to obtain causally indefinite computations has received significant attention. The quantum switch, for example, uses a quantum system to coherently control the order of operations. Several computational and information-theoretical advantages have been demonstrated, raising questions as to whether advantages can be obtained in a more unified complexity theoretic framework. In this paper, we approach this problem by studying the query complexity of Boolean functions under general higher-order quantum computations. To this end, we generalize the framework of query complexity from quantum circuits to quantum supermaps to compare different models on an equal footing. We show that the recently introduced class of quantum circuits with quantum control of causal order cannot lead to any reduction in query complexity, and that any potential advantage arising from causally indefinite supermaps can be bounded by the polynomial method, as is the case with quantum circuits. Nevertheless, we find some functions for which the minimum error with which they can be computed using two queries is strictly lower when exploiting causally indefinite supermaps. Published by the American Physical Society 2024
Quantum programming languages permit a hardware independent, high-level description of quantum algo rithms. In particular, the quantum lambda-calculus is a higher-order programming language with quantum primitives, mixing quantum data and classical control. Giving satisfactory denotational semantics to the quantum lambda-calculus is a challenging problem that has attracted significant interest in the past few years. Several models have been proposed but for those that address the whole quantum λ-calculus, they either do not represent the dynamics of computation, or they lack the compositionality one often expects from denotational models. In this paper, we give the first compositional and interactive model of the full quantum lambda-calculus, based on game semantics. To achieve this we introduce a model of quantum games and strategies, combining quantum data with a representation of the dynamics of computation inspired from causal models of concurrent systems. In this model we first give a computationally adequate interpretation of the affine fragment. Then, we extend the model with a notion of symmetry, allowing us to deal with replication. In this refined setting, we interpret and prove adequacy for the full quantum lambda-calculus. We do this both from a sequential and a parallel interpretation, the latter representing faithfully the causal independence between sub-computations.
Quantum supermaps are transformations that map quantum operations to quantum operations.It is known that quantum supermaps which respect a definite, predefined causal order between their input operations correspond to fixed-order quantum circuits, also called quantum combs.A systematic understanding of the physical interpretation of more general types of quantum supermaps-in particular, those incompatible with a definite causal structure-is however lacking.In this paper, we identify two types of circuits that naturally generalize the fixed-order case and that likewise correspond to distinct classes of quantum supermaps, which we fully characterize.We first introduce "quantum circuits with classical control of causal order," in which the order of operations is still well defined, but not necessarily fixed in advance: it can, in particular, be established dynamically, in a classically controlled manner, as the circuit is being used.We then consider "quantum circuits with quantum control of causal order," in which the order of operations is controlled coherently.The supermaps described by these classes of circuits are physically realizable, and the latter encompasses all known examples of physically realizable processes with indefinite causal order, including the celebrated "quantum switch."Interestingly, it also contains other examples arising from the combination of dynamical and coherent control of causal order, and we detail explicitly one such process.Nevertheless, we show that quantum circuits with quantum control of causal order can only generate "causal" correlations, compatible with a well-defined causal order.We furthermore extend our considerations to probabilistic circuits that produce also classical outcomes, and we demonstrate by an example how the characterizations derived in this work allow us to identify advantages for quantum information processing tasks that could be demonstrated in practice.
Logical consistency with free local operations is compatible with nontrivial classical communications, where all parties can be both in each other’s past and future—a phenomenon known as noncausality. Noncausal processes, such as the “Lugano process,” violate causal inequalities, yet their physical realizability remains an open question. In contrast, the quantum switch—a physically realizable process with indefinite causal order—can only generate causal correlations. Building on a recently established correspondence [Kunjwal and Baumeler, ] between the SHIFT measurement, which exhibits nonlocality without entanglement, and the Lugano process, we demonstrate that the SHIFT measurement can be implemented using a quantum switch of classical communications in a scenario with quantum inputs. This shows that the structure of the Lugano process can be simulated by a quantum switch and that successful SHIFT discrimination witnesses causal nonseparability rather than noncausality. Finally, we identify a broad class of “superposition of classical communications” derived from classical processes without global past capable of realizing similar causally indefinite measurements. We examine these results in relation to the ongoing debate on implementations of indefinite causal orders.
We present a categorical construction for modelling causal structures within a general class of process theories that include the theory of classical probabilistic processes as well as quantum theory. Unlike prior constructions within categorical quantum mechanics, the objects of this theory encode fine-grained causal relationships between subsystems and give a new method for expressing and deriving consequences for a broad class of causal structures. We show that this framework enables one to define families of processes which are consistent with arbitrary acyclic causal orderings. In particular, one can define one-way signalling (a.k.a. semi-causal) processes, non-signalling processes, and quantum n-combs. Furthermore, our framework is general enough to accommodate recently-proposed generalisations of classical and quantum theory where processes only need to have a fixed causal ordering locally, but globally allow indefinite causal ordering. To illustrate this point, we show that certain processes of this kind, such as the quantum switch, the process matrices of Oreshkov, Costa, and Brukner, and a classical three-party example due to Baumeler, Feix, and Wolf are all instances of a certain family of processes we refer to as SOCn in the appropriate category of higher-order causal processes. After defining these families of causal structures within our framework, we give derivations of their operational behaviour using simple, diagrammatic axioms. Comment: Extended version of a LICS 2017 paper with the same title