-
Cut elimination for propositional cyclic proof systems with fixed-point operators
Authors:
Hiromasa Hori,
Koji Nakazawa,
Makoto Tatsuta
Abstract:
Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corresponding infinitary proof system. Hence, these proof systems are generally not the same, as in the cyclic system may be weaker than the infinitary system. For several logics, the infinitary proof systems are shown to be c…
▽ More
Infinitary and cyclic proof systems are proof systems for logical formulas with fixed-point operators or inductive definitions. A cyclic proof system is a restriction of the corresponding infinitary proof system. Hence, these proof systems are generally not the same, as in the cyclic system may be weaker than the infinitary system. For several logics, the infinitary proof systems are shown to be cut-free complete. However, cyclic proof systems are characterized with many unknown problems on the (cut-free) completeness or the cut-elimination property. In this study, we show that the provability of infinitary and cyclic proof systems are the same for some propositional logics with fixed-point operators or inductive definitions and that the cyclic proof systems are cut-free complete.
△ Less
Submitted 20 December, 2023;
originally announced December 2023.
-
Dressed-state control of effective dipolar interaction between strongly-coupled solid-state spins
Authors:
Junghyun Lee,
Mamiko Tatsuta,
Andrew Xu,
Erik Bauch,
Mark J. H. Ku,
Ronald. L. Walsworth
Abstract:
Strong interactions between spins in many-body solid-state quantum system is a crucial resource for exploring and applying non-classical states. In particular, electronic spins associated with defects in diamond system are a leading platform for the study of collective quantum phenomena and for quantum technology applications. While such solid-state quantum defect systems have the advantage of sca…
▽ More
Strong interactions between spins in many-body solid-state quantum system is a crucial resource for exploring and applying non-classical states. In particular, electronic spins associated with defects in diamond system are a leading platform for the study of collective quantum phenomena and for quantum technology applications. While such solid-state quantum defect systems have the advantage of scalability and operation under ambient conditions, they face the key challenge of controlling interactions between the defects spins, since the defects are spatially fixed inside the host lattice with relative positions that cannot be well controlled during fabrication. In this work, we present a dressed-state approach to control the effective dipolar coupling between solid-state spins; and then demonstrate this scheme experimentally using two strongly-coupled nitrogen vacancy (NV) centers in diamond. Including Rabi driving terms between the m$_s$ = 0 and $\pm$1 states in the NV spin Hamiltonian allows us to turn on and off or tune the effective dipolar coupling between two NV spins. Through Ramsey spectroscopy, we detect the change of the effective dipolar field generated by the control NV spin prepared in different dressed states. To observe the change of interaction dynamics, we then deploy spin-lock-based polarization transfer measurements via a Hartmann-Hahn matching condition between two NV spins in different dressed states. We perform simulations that indicate the promise for this robust scheme to control the distribution of interaction strengths in strongly-interacting spin systems, including interaction strength homogenization in a spin ensemble, which can be a valuable tool for studying non-equilibrium quantum phases and generating high fidelity multi-spin correlated states for quantum-enhanced sensing.
△ Less
Submitted 2 May, 2023; v1 submitted 14 March, 2022;
originally announced March 2022.
-
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
Authors:
Yukihiro Oda,
James Brotherston,
Makoto Tatsuta
Abstract:
A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with inductive definitions does not hold. This paper shows that the conjecture is correct by giving a sequent not provable without the cut rule but provable in the cyclic p…
▽ More
A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with inductive definitions does not hold. This paper shows that the conjecture is correct by giving a sequent not provable without the cut rule but provable in the cyclic proof system.
△ Less
Submitted 14 February, 2024; v1 submitted 22 June, 2021;
originally announced June 2021.
-
Quantum metrology based on symmetry-protected adiabatic transformation: Imperfection, finite time duration, and dephasing
Authors:
Takuya Hatomura,
Atsuki Yoshinaga,
Yuichiro Matsuzaki,
Mamiko Tatsuta
Abstract:
The aim of quantum metrology is to estimate target parameters as precisely as possible. In this paper, we consider quantum metrology based on symmetry-protected adiabatic transformation. We introduce a ferromagnetic Ising model with a transverse field as a probe and consider the estimation of a longitudinal field. Without the transverse field, the ground state of the probe is given by the Greenber…
▽ More
The aim of quantum metrology is to estimate target parameters as precisely as possible. In this paper, we consider quantum metrology based on symmetry-protected adiabatic transformation. We introduce a ferromagnetic Ising model with a transverse field as a probe and consider the estimation of a longitudinal field. Without the transverse field, the ground state of the probe is given by the Greenberger-Horne-Zeilinger state, and thus the Heisenberg limit estimation of the longitudinal field can be achieved through parity measurement. In our scheme, full information of the longitudinal field encoded on parity is exactly mapped to global magnetization by symmetry-protected adiabatic transformation, and thus the parity measurement can be replaced with global magnetization measurement. Moreover, this scheme requires neither accurate control of individual qubits nor that of interaction strength. We discuss the effects of the finite transverse field and nonadiabatic transitions as imperfection of adiabatic transformation. By taking into account finite time duration for state preparation, sensing, and readout, we also compare performance of the present scheme with a classical scheme in the absence and presence of dephasing.
△ Less
Submitted 12 December, 2021; v1 submitted 6 April, 2021;
originally announced April 2021.
-
Entanglement-enhanced sensing using a chain of qubits with always-on nearest-neighbor interactions
Authors:
Atsuki Yoshinaga,
Mamiko Tatsuta,
Yuichiro Matsuzaki
Abstract:
Quantum metrology is the use of genuinely quantum properties such as entanglement as a resource to outperform classical sensing strategies. Typically, entanglement is created by implementing gate operations or inducing many-body interactions. However, existing sensing schemes with these approaches require accurate control of the probe system such as switching on and off the interaction among qubit…
▽ More
Quantum metrology is the use of genuinely quantum properties such as entanglement as a resource to outperform classical sensing strategies. Typically, entanglement is created by implementing gate operations or inducing many-body interactions. However, existing sensing schemes with these approaches require accurate control of the probe system such as switching on and off the interaction among qubits, which can be challenging for practical applications. Here, we propose an entanglement-enhanced sensing scheme with an always-on nearest-neighbor interaction between qubits. We adopt the transverse field Ising chain as the probe system, making use of the so-called quantum domino dynamics for the generation of the entangled states. In addition to the advantage that our scheme can be implemented without controlling the interactions, it only requires initialization of the system, projective measurements on a single qubit, and control of the uniform magnetic fields. We can achieve an improved sensitivity beyond the standard quantum limit even under the effect of realistic decoherence.
△ Less
Submitted 9 June, 2021; v1 submitted 8 January, 2021;
originally announced January 2021.
-
Quantum metrology with generalized cat states
Authors:
Mamiko Tatsuta,
Yuichiro Matsuzaki,
Akira Shimizu
Abstract:
We show a general relationship between a superposition of macroscopically distinct states and sensitivity in quantum metrology. Generalized cat states are defined by using an index which extracts the coherence between macroscopically distinct states, and a wide variety of states, including a classical mixture of an exponentially large number of states, has been identified as the generalized cat st…
▽ More
We show a general relationship between a superposition of macroscopically distinct states and sensitivity in quantum metrology. Generalized cat states are defined by using an index which extracts the coherence between macroscopically distinct states, and a wide variety of states, including a classical mixture of an exponentially large number of states, has been identified as the generalized cat state with this criterion. We find that, if we use the generalized cat states for magnetic field sensing without noise, we achieve the Heisenberg limited sensitivity. Moreover, we even show that sensitivity of generalized cat states achieves the ultimate scaling sensitivity beyond the standard quantum limit under the effect of dephasing. As an example, we investigate the sensitivity of a generalized cat state that is attainable through a single global manipulation on a thermal equilibrium state and find an improvement of a few orders of magnitude from the previous sensors. Clarifying a wide class that includes such a peculiar state as metrologically useful, our results significantly broaden the potential of quantum metrology.
△ Less
Submitted 15 September, 2019; v1 submitted 5 February, 2019;
originally announced February 2019.
-
Completeness of Cyclic Proofs for Symbolic Heaps
Authors:
Makoto Tatsuta,
Koji Nakazawa,
Daisuke Kimura
Abstract:
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of inductive definitions, and shows its soundness and completeness. The decision procedure for entailments of symbolic heaps with inductive definitions is also given. Deci…
▽ More
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of inductive definitions, and shows its soundness and completeness. The decision procedure for entailments of symbolic heaps with inductive definitions is also given. Decidability for entailments of symbolic heaps with inductive definitions is an important question. Completeness of cyclic proof systems is also an important question. The results of this paper answer both questions. The decision procedure is feasible since it is nondeterministic double-exponential time complexity.
△ Less
Submitted 28 May, 2018; v1 submitted 11 April, 2018;
originally announced April 2018.
-
Decidability for Entailments of Symbolic Heaps with Arrays
Authors:
Daisuke Kimura,
Makoto Tatsuta
Abstract:
This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential quantifiers. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially quantified. This condit…
▽ More
This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential quantifiers. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially quantified. This condition is different from that proposed by Brotherston et al. in 2017 and one of them does not imply the other. The main idea is a novel translation from an entailment of symbolic heaps into a formula in Presburger arithmetic. The second result is the decidability for a system with both arrays and lists. The key idea is to extend the unroll collapse technique proposed by Berdine et al. in 2005 to arrays and arithmetic as well as double-linked lists.
△ Less
Submitted 10 May, 2021; v1 submitted 16 February, 2018;
originally announced February 2018.
-
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs
Authors:
Stefano Berardi,
Makoto Tatsuta
Abstract:
A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in Martin-Löf's style, and conjectured the equivalence. The equivalence has been left an open question since…
▽ More
A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in Martin-Löf's style, and conjectured the equivalence. The equivalence has been left an open question since 2011. This paper shows that CLKID-omega and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKID-omega, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.
△ Less
Submitted 31 July, 2019; v1 submitted 27 December, 2017;
originally announced December 2017.
-
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic
Authors:
Stefano Berardi,
Makoto Tatsuta
Abstract:
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the provability of the classical cyclic proof system and that of the classical system of Martin-Lof's inductive definitions.
This paper studies the conjecture for intuitionistic logic.
This paper first points out that t…
▽ More
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the provability of the classical cyclic proof system and that of the classical system of Martin-Lof's inductive definitions.
This paper studies the conjecture for intuitionistic logic.
This paper first points out that the countermodel of FOSSACS 2017 paper by the same authors shows the conjecture for intuitionistic logic is false in general. Then this paper shows the conjecture for intuitionistic logic is true under arithmetic, namely, the provability of the intuitionistic cyclic proof system is the same as that of the intuitionistic system of Martin-Lof's inductive definitions when both systems contain Heyting arithmetic HA.
For this purpose, this paper also shows that HA proves Podelski-Rybalchenko theorem for induction and Kleene-Brouwer theorem for induction. These results immediately give another proof to the conjecture under arithmetic for classical logic shown in LICS 2017 paper by the same authors.
△ Less
Submitted 10 December, 2017;
originally announced December 2017.
-
Decision Procedure for Entailment of Symbolic Heaps with Arrays
Authors:
Daisuke Kimura,
Makoto Tatsuta
Abstract:
This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al, namely, one…
▽ More
This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al, namely, one of them does not imply the other. For improving efficiency of the decision procedure, some techniques are also presented. The main idea of the decision procedure is a novel translation of an entailment of symbolic heaps into a formula in Presburger arithmetic, and to combine it with an external SMT solver. This paper also gives experimental results by an implementation, which shows that the decision procedure works efficiently enough to use.
△ Less
Submitted 28 August, 2017; v1 submitted 22 August, 2017;
originally announced August 2017.
-
Conversion of Thermal Equilibrium States into Superpositions of Macroscopically Distinct States
Authors:
Mamiko Tatsuta,
Akira Shimizu
Abstract:
A simple procedure for obtaining superpositions of macroscopically distinct states is proposed and analyzed. We find that a thermal equilibrium state can be converted into such a state when a single global measurement of a macroscopic observable, such as the total magnetization, is made. This method is valid for systems with macroscopic degrees of freedom and finite (including zero) temperature. T…
▽ More
A simple procedure for obtaining superpositions of macroscopically distinct states is proposed and analyzed. We find that a thermal equilibrium state can be converted into such a state when a single global measurement of a macroscopic observable, such as the total magnetization, is made. This method is valid for systems with macroscopic degrees of freedom and finite (including zero) temperature. The superposition state is obtained with a high (low) probability when the measurement is made with a high (low) resolution. We find that this method is feasible in an experiment.
△ Less
Submitted 17 January, 2018; v1 submitted 15 March, 2017;
originally announced March 2017.
-
Micro-Clustering: Finding Small Clusters in Large Diversity
Authors:
Takeaki Uno,
Hiroki Maegawa,
Takanobu Nakahara,
Yukinobu Hamuro,
Ryo Yoshinaka,
Makoto Tatsuta
Abstract:
We address the problem of un-supervised soft-clustering called micro-clustering. The aim of the problem is to enumerate all groups composed of records strongly related to each other, while standard clustering methods separate records at sparse parts. The problem formulation of micro-clustering is non-trivial. Clique mining in a similarity graph is a typical approach, but it results in a huge numbe…
▽ More
We address the problem of un-supervised soft-clustering called micro-clustering. The aim of the problem is to enumerate all groups composed of records strongly related to each other, while standard clustering methods separate records at sparse parts. The problem formulation of micro-clustering is non-trivial. Clique mining in a similarity graph is a typical approach, but it results in a huge number of cliques that are of many similar cliques. We propose a new concept data polishing. The cause of huge solutions can be considered that the groups are not clear in the data, that is, the boundaries of the groups are not clear, because of noise, uncertainty, lie, lack, etc. Data polishing clarifies the groups by perturbating the data. Specifically, dense subgraphs that would correspond to clusters are replaced by cliques. The clusters are clarified as maximal cliques, thus the number of maximal cliques will be drastically reduced. We also propose an efficient algorithm applicable even for large scale data. Computational experiments showed the efficiency of our algorithm, i.e., the number of solutions is small, (e.g., 1,000), the members of each group are deeply related, and the computation time is short.
△ Less
Submitted 6 June, 2016; v1 submitted 11 July, 2015;
originally announced July 2015.
-
Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types
Authors:
Daisuke Kimura,
Makoto Tatsuta
Abstract:
This paper extends the dual calculus with inductive types and coinductive types. The paper first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the same duality of the original dual calculus, it has the duality of inductive and coinductive types, that is, the duality of terms and coterms for inductive and coinductive types, and the duality of their redu…
▽ More
This paper extends the dual calculus with inductive types and coinductive types. The paper first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the same duality of the original dual calculus, it has the duality of inductive and coinductive types, that is, the duality of terms and coterms for inductive and coinductive types, and the duality of their reduction rules. Its strong normalization is also proved, which is shown by translating it into a second-order dual calculus. The strong normalization of the second-order dual calculus is proved by translating it into the second-order symmetric lambda calculus. This paper then introduces a call-by-value system and a call-by-name system of the dual calculus with inductive and coinductive types, and shows the duality of call-by-value and call-by-name, their Church-Rosser properties, and their strong normalization. Their strong normalization is proved by translating them into the non-deterministic dual calculus with inductive and coinductive types.
△ Less
Submitted 27 March, 2013; v1 submitted 23 February, 2013;
originally announced February 2013.
-
Type Inference for Bimorphic Recursion
Authors:
Makoto Tatsuta,
Ferruccio Damiani
Abstract:
This paper proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this paper can be nested…
▽ More
This paper proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this paper can be nested. This paper shows bimorphic recursion has principal types and decidable type inference. Hence bimorphic recursion gives us flexible ty** for recursion with decidable type inference. This paper also shows that its typability becomes undecidable because of nesting of recursions when one removes the instantiation property from the bimorphic recursion.
△ Less
Submitted 6 June, 2011;
originally announced June 2011.
