



@article {2858,
	title = {Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra},
	year = {2021},
	month = {10/13/2021},
	abstract = {<p>We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA as well as their appropriate quantum interpretations. In light of applications of KAT, we are able to demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following the rules of effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.</p>},
	doi = {https://doi.org/10.1145/3519939.3523713},
	url = {https://arxiv.org/abs/2110.07018},
	author = {Yuxiang Peng and Mingsheng Ying and Xiaodi Wu}
}
@article {2306,
	title = {Quantitative Robustness Analysis of Quantum Programs (Extended Version)},
	journal = {Proc. ACM Program. Lang.},
	volume = {3},
	year = {2018},
	month = {2018/12/1},
	pages = {Article 31},
	abstract = {<p>Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called ε-robustness, which characterizes possible \&quot;distance\&quot; between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.</p>},
	doi = {https://doi.org/10.1145/3290344},
	url = {https://arxiv.org/abs/1811.03585},
	author = {Shih-Han Hung and Kesha Hietala and Shaopeng Zhu and Mingsheng Ying and Michael Hicks and Xiaodi Wu}
}
@article {1438,
	title = {Ancilla-Assisted Discrimination of Quantum Gates},
	year = {2008},
	month = {2008/09/02},
	abstract = {  The intrinsic idea of superdense coding is to find as many gates as possible
such that they can be perfectly discriminated. In this paper, we consider a new
scheme of discrimination of quantum gates, called ancilla-assisted
discrimination, in which a set of quantum gates on a $d-$dimensional system are
perfectly discriminated with assistance from an $r-$dimensional ancilla system.
The main contribution of the present paper is two-fold: (1) The number of
quantum gates that can be discriminated in this scheme is evaluated. We prove
that any $rd+1$ quantum gates cannot be perfectly discriminated with assistance
from the ancilla, and there exist $rd$ quantum gates which can be perfectly
discriminated with assistance from the ancilla. (2) The dimensionality of the
minimal ancilla system is estimated. We prove that there exists a constant
positive number $c$ such that for any $k\leq cr$ quantum gates, if they are
$d$-assisted discriminable, then they are also $r$-assisted discriminable, and
there are $c^{\prime}r\textrm{}(c^{\prime}>c)$ different quantum gates which
can be discriminated with a $d-$dimensional ancilla, but they cannot be
discriminated if the ancilla is reduced to an $r-$dimensional system. Thus, the
order $O(r)$ of the number of quantum gates that can be discriminated with
assistance from an $r-$dimensional ancilla is optimal. The results reported in
this paper represent a preliminary step toward understanding the role ancilla
system plays in discrimination of quantum gates as well as the power and limit
of superdense coding.
},
	url = {http://arxiv.org/abs/0809.0336v1},
	author = {Jianxin Chen and Mingsheng Ying}
}
@article {1453,
	title = {Existence of Universal Entangler},
	journal = {Journal of Mathematical Physics},
	volume = {49},
	year = {2008},
	month = {2008/01/01},
	pages = {012103},
	abstract = {  A gate is called entangler if it transforms some (pure) product states to
entangled states. A universal entangler is a gate which transforms all product
states to entangled states. In practice, a universal entangler is a very
powerful device for generating entanglements, and thus provides important
physical resources for accomplishing many tasks in quantum computing and
quantum information. This Letter demonstrates that a universal entangler always
exists except for a degenerated case. Nevertheless, the problem how to find a
universal entangler remains open.
},
	doi = {10.1063/1.2829895},
	url = {http://arxiv.org/abs/0704.1473v2},
	author = {Jianxin Chen and Runyao Duan and Zhengfeng Ji and Mingsheng Ying and Jun Yu}
}
@article {1441,
	title = {The LU-LC conjecture is false},
	year = {2007},
	month = {2007/09/09},
	abstract = {  The LU-LC conjecture is an important open problem concerning the structure of
entanglement of states described in the stabilizer formalism. It states that
two local unitary equivalent stabilizer states are also local Clifford
equivalent. If this conjecture were true, the local equivalence of stabilizer
states would be extremely easy to characterize. Unfortunately, however, based
on the recent progress made by Gross and Van den Nest, we find that the
conjecture is false.
},
	url = {http://arxiv.org/abs/0709.1266v2},
	author = {Zhengfeng Ji and Jianxin Chen and Zhaohui Wei and Mingsheng Ying}
}
