The (meta)logic underlying classical theory of computation is Boolean (two-valued) logic. Quantum logic was proposed by Birkhoff and von Neumann as a logic of quantum mechanics more than sixty years ago. The major difference between Boolean logic and quantum logic is that the latter does not enjoy distributivity in general. The rapid development of quantum computation in recent years stimulates us to establish a theory of computation based on quantum logic. The present paper is the first step toward such a new theory and it focuses on the simplest models of computation, namely finite automata. It is found that the universal validity of many properties of automata depend heavily upon the distributivity of the underlying logic. This indicates that these properties does not universally hold in the realm of quantum logic. On the other hand, we show that a local validity of them can be recovered by imposing a certain commutativity to the (atomic) statements about the automata under consideration. This reveals an essential difference between the classical theory of computation and the computation theory based on quantum logic.
Propositional Gödel logic extends intuitionistic logic with the non-constructive principle of linearity $A\rightarrow B\ \lor\ B\rightarrow A$. We introduce a Curry-Howard correspondence for this logic and show that a particularly simple natural deduction calculus can be used as a typing system. The resulting functional language enriches the simply typed lambda calculus with a synchronous communication mechanism between parallel processes. Our normalization proof employs original termination arguments and sophisticated proof transformations with a meaningful computational reading. Our results …
We study generalized possibilistic computation tree logic model checking in this paper, which is an extension of possibilistic computation logic model checking introduced by Y.Li, Y.Li and Z.Ma (2014). The system is modeled by generalized possibilistic Kripke structures (GPKS, in short), and the verifying property is specified by a generalized possibilistic computation tree logic (GPoCTL, in short) formula. Based on generalized possibility measures and generalized necessity measures, the method of generalized possibilistic computation tree logic model checking is discussed, and the correspondi…
Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the exploration of the computational content of mathematical and logical principles, aiming to bring together researchers from both fields and exchange ideas. In this fifth edition we received 18 submissions of both short and full papers. Fourteen (14) of these were selected to present at the meeting in Vienna, and six (6) full papers were accepted to appear at this ETP…
This special issue cover the seventh and last conference of the CL&C series, started in 2006 in San Servolo. Topics are the computational content of logics between intuitionistic logic and classical logic, through normalization, and a new topic, cyclic proofs and the complexity of checking the correctness of a cyclic proof. Accepted papers include an empirical comparison of time consumption of different normalization algorithms, and new reductions sets for several extensions of intuitionistic logic having the Herbrand disjunction property. Another paper provides a reduction set for admissible …
We present a logical separability analysis for a functional quantum computation language. This logic is inspired by previous works on logical analysis of aliasing for imperative functional programs. Both analyses share similarities notably because they are highly non-compositional. Quantum setting is harder to deal with since it introduces non determinism and thus considerably modifies semantics and validity of logical assertions. This logic is the first proposal of entanglement/separability analysis dealing with a functional quantum programming language with higher-order functions.
This paper describes a quantum algorithm for proof search in sequent calculus of a subset of Linear Logic using the Grover Search Algorithm. We briefly overview the Grover Search Algorithm and Linear Logic, show the detailed steps of the algorithm and then present the results obtained on quantum simulators.
Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum p…
We introduce a generic extension of the popular branching-time logic CTL which refines the temporal until and release operators with formal languages. For instance, a language may determine the moments along a path that an until property may be fulfilled. We consider several classes of languages leading to logics with different expressive power and complexity, whose importance is motivated by their use in model checking, synthesis, abstract interpretation, etc. We show that even with context-free languages on the until operator the logic still allows for polynomial time model-checking despite …
This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, our objective is to provide a high-level presentation of the logical aspects of quantum theory. Mateus' and Sernadas' EQPL logic is illustrated with a small example, namely the state of an entangled pair of qubits. The "KT" logic of van der Meyden and Patra is demonstr…
This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide…
We add local variables to quantum relational Hoare logic (Unruh, POPL 2019). We derive reasoning rules for supporting local variables (including an improved "adversary rule"). We extended the qrhl-tool for computer-aided verification of qRHL to support local variables and our new reasoning rules.
CL&C'12 was the fourth of a conference series on "Classical Logic and Computation", held as satellite to ICALP'12 on Sunday July 8, 2012 in Warwick, England. CL&C intends to cover all work aiming to explore computational aspects of classical logic and mathematics, and is focused on the exploration of the computational content of mathematical and logical principles. The scientific aim of this workshop is to bring together researchers from both fields and exchange ideas. The intention of the organisers is for CL&C to be an informal workshop. Participants are encouraged to present work in progres…
Technically speaking, the transcendental syntax is about designing logics with a computational foundation. It suggests a new framework for proof theory where logic (proofs, formulas, truth, ...) is no more primitive but computation is. All the logical entities and activities will be presented as formatting/structuring on a given model of computation which should be as general, simple and natural as possible. The selected ground for logic in the transcendental syntax is a model of computation I call "stellar resolution" which is basically a logic-free reformulation of Robinson's first-order cla…
The two major systems of formal verification are model checking and algebraic model-based testing. Model checking is based on some form of temporal logic such as linear temporal logic (LTL) or computation tree logic (CTL). One powerful and realistic logic being used is CTL, which is capable of expressing most interesting properties of processes such as liveness and safety. Model-based testing is based on some operational semantics of processes (such as traces, failures, or both) and its associated preorders. The most fine-grained preorder beside bisimulation (mostly of theoretical importance) …
The goal of computational logic is to allow us to model computation as well as to reason about it. We argue that a computational logic must be able to model interactive computation. We show that first-order logic cannot model interactive computation due to the incompleteness of interaction. We show that interactive computation is necessarily paraconsistent, able to model both a fact and its negation, due to the role of the world (environment) in determining the course of the computation. We conclude that paraconsistency is a necessary property for a logic that can model interactive computation…
Classical computations can not capture the essence of infinite computations very well. This paper will focus on a class of infinite computations called convergent infinite computations}. A logic for convergent infinite computations is proposed by extending first order theories using Cauchy sequences, which has stronger expressive power than the first order logic. A class of fixed points characterizing the logical properties of the limits can be represented by means of infinite-length terms defined by Cauchy sequences. We will show that the limit of sequence of first order theories can be defin…
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirq's tutorial on t…
Abstract interpretation, Hoare logic, and incorrectness (or reverse Hoare) logic are powerful techniques for static analysis of computer programs. All of them have been successfully extended to the quantum setting, but largely developed in parallel. In this paper, we examine the relationship between these techniques in the context of verifying quantum while-programs, where the abstract domain and the set of assertions for quantum states are well-structured. In particular, we show that any complete quantum abstract interpretation induces a quantum Hoare logic and a quantum incorrectness logic, …
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning. In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed $λ$-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the co…
We begin by discussing the history of quantum logic, dividing it into three eras or lives. The first life has to do with Birkhoff and von Neumann's algebraic approach in the 1930's. The second life has to do with attempt to understand quantum logic as logic that began in the late 1950's and blossomed in the 1970's. And the third life has to do with recent developments in quantum logic coming from its connections to quantum computation. We discuss our own work connecting quantum logic to quantum computation (viewing quantum logic as the logic of quantum registers storing qubits), and make some …
Although quantum logic by using exogenous approach has been proposed for reasoning about closed quantum systems, an improvement would be worth to study quantum logic based on density operators instead of unit vectors in the state logic point of view. In order to achieve this, we build an exogenous quantum operator logic(EQOL) based on density operators for reasoning about open quantum systems. We show that this logic is sound and complete. Just as the exogenous quantum propositional logic(EQPL), by applying exogenous approach, EQOL is extended from the classical propositional logic, and is use…
Process algebra and temporal logic are two popular paradigms for the specification, verification and systematic development of reactive and concurrent systems. These two approaches take different standpoint for looking at specifications and verifications, and offer complementary advantages. In order to mix algebraic and logic styles of specification in a uniform framework, the notion of a logic labelled transition system (LLTS) has been presented and explored by Luttgen and Vogler. This paper intends to propose a LLTS-oriented process calculus which, in addition to usual process-algebraic oper…
Algebraic characterization of logic programs has received increasing attention in recent years. Researchers attempt to exploit connections between linear algebraic computation and symbolic computation in order to perform logical inference in large scale knowledge bases. This paper proposes further improvement by using sparse matrices to embed logic programs in vector spaces. We show its great power of computation in reaching the fixpoint of the immediate consequence operator from the initial vector. In particular, performance for computing the least models of definite programs is dramatically …
A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by introducing a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables. Examples are presented to show our logic is particularly suit…
A logical system derived from linear logic and called QMLL is introduced and shown able to capture all unitary quantum circuits. Conversely, any proof is shown to compute, through a concrete GoI interpretation, some quantum circuits. The system QMLL, which enjoys cut-elimination, is obtained by endowing multiplicative linear logic with a quantum modality.
The satisfiability problem of the branching time logic CTL is studied in terms of computational complexity. Tight upper and lower bounds are provided for each temporal operator fragment. In parallel, the minimal model size is studied with a suitable notion of minimality. Thirdly, flat CTL is investigated, i.e., formulas with very low temporal operator nesting depth. A sharp dichotomy is shown in terms of complexity and minimal models: Temporal depth one has low expressive power, while temporal depth two is equivalent to full CTL.
Categorical Universal Logic is a theory of monad-relativised hyperdoctrines (or fibred universal algebras), which in particular encompasses categorical forms of both first-order and higher-order quantum logics as well as classical, intuitionistic, and diverse substructural logics. Here we show there are those dual adjunctions that have inherent hyperdoctrine structures in their predicate functor parts. We systematically investigate into the categorical logics of dual adjunctions by utilising Johnstone-Dimov-Tholen's duality-theoretic framework. Our set-theoretical duality-based hyperdoctrines …
Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpo…
Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this paper, we propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably,…
Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces "ghost variables" to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoa…
We present a logic for reasoning about pairs of interactive quantum programs - quantum relational Hoare logic (qRHL). This logic follows the spirit of probabilistic relational Hoare logic (Barthe et al. 2009) and allows us to formulate how the outputs of two quantum programs relate given the relationship of their inputs. Probabilistic RHL was used extensively for computer-verified security proofs of classical cryptographic protocols. Since pRHL is not suitable for analyzing quantum cryptography, we present qRHL as a replacement, suitable for the security analysis of post-quantum cryptography a…
We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satisfied that refer to the relationship between the programs inputs/outputs.
In this paper, we introduce a model of quantum concurrent program, which can be used to model the behaviour of reactive quantum systems and to design quantum compilers. We investigate quantum temporal logic, QTL, for the specification of quantum concurrent systems by suggesting the time-dependence of events. QTL employs the projections on subspaces as atomic propositions, which was established in the Birkhoff and von Neumann's classic treatise on quantum logic. For deterministic functional quantum program, We prove a quantum Böhm-Jacopini theorem which states that any such program is equivalen…
This volume contains the proceedings of the 17th International Conference on Quantum Physics and Logic (QPL 2020), which was held June 2-6, 2020. Quantum Physics and Logic is an annual conference that brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behavior in general. Work that applies struct…
The main contribution of this paper is the introduction of a dynamic logic formalism for reasoning about information flow in composite quantum systems. This builds on our previous work on a complete quantum dynamic logic for single systems. Here we extend that work to a sound (but not necessarily complete) logic for composite systems, which brings together ideas from the quantum logic tradition with concepts from (dynamic) modal logic and from quantum computation. This Logic of Quantum Programs (LQP) is capable of expressing important features of quantum measurements and unitary evolutions of …
We discuss quantum non-locality and contextuality, emphasising logical and structural aspects. We also show how the same mathematical structures arise in various areas of classical computation.
The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of multiplication and order (x,<) behaves differently in the above mentioned domains of numbers. By a theorem of Robinson, addition is definable by multiplication and order in the domain of natural numbers…
This volume contains the proceedings of the ninth workshop on Quantum Physics and Logic (QPL2012) which took place in Brussels from the 10th to the 12th of October 2012. QPL2012 brought together researchers working on mathematical foundations of quantum physics, quantum computing, and spatio-temporal causal structures. The particular focus was on the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical techniques, and other computer science methods for the study of physical behaviour in general.
We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is i…
In the present article, we explore a new approach for the study of orthomodular lattices, where we replace the problematic conjunction by a binary operator, called the Sasaki projection. We present a characterization of orthomodular lattices based on the use of an algebraic version of the Sasaki projection operator (together with orthocomplementation) rather than on the conjunction. We then define of a new logic, which we call Sasaki Orthologic, which is closely related to quantum logic, and provide a rule-based definition of this logic.
While quantum computers are expected to yield considerable advantages over classical devices, the precise features of quantum theory enabling these advantages remain unclear. Contextuality--the denial of a notion of classical physical reality--has emerged as a promising hypothesis. Magic states are quantum resources critical for practically achieving universal quantum computation. They exhibit the standard form of contextuality that is known to enable probabilistic advantages in a variety of computational and communicational tasks. Strong contextuality is an extremal form of contextuality desc…
Scholars have wondered for a long time whether the language of quantum mechanics introduces a quantum notion of truth which is formalized by quantum logic (QL) and is incompatible with the classical (Tarskian) notion. We show that QL can be interpreted as a pragmatic language of assertive formulas which formalize statements about physical systems that are empirically justified or unjustified in the framework of quantum mechanics. According to this interpretation, QL formalizes properties of the metalinguistic notion of empirical justification within quantum mechanics rather than properties of …
This volume contains the proceedings of the 13th International Conference on Quantum Physics and Logic (QPL 2016), which was held June 6-10, 2016 at the University of Strathclyde. QPL is a conference that brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behaviour in general.
First-order logic is known to have limited expressive power over finite structures. It enjoys in particular the locality property, which states that first-order formulae cannot have a global view of a structure. This limitation ensures on their low sequential computational complexity. We show that the locality impacts as well on their distributed computational complexity. We use first-order formulae to describe the properties of finite connected graphs, which are the topology of communication networks, on which the first-order formulae are also evaluated. We show that over bounded degree netwo…
We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare logic for quantum programs" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.
