@article {2330, title = {Mathematical methods for resource-based type theories}, year = {2018}, abstract = {

With the wide range of quantum programming languages on offer now, efficient program verification and type checking for these languages presents a challenge -- especially when classical debugging techniques may affect the states in a quantum program. In this work, we make progress towards a program verification approach using the formalism of operational quantum mechanics and resource theories. We present a logical framework that captures two mathematical approaches to resource theory based on monoids (algebraic) and monoidal categories (categorical). We develop the syntax of this framework as an intuitionistic sequent calculus, and prove soundness and completeness of an algebraic and categorical semantics that recover these approaches. We also provide a cut-elimination theorem, normal form, and analogue of Lambek\&$\#$39;s lifting theorem for polynomial systems over the logics. Using these approaches along with the Curry-Howard-Lambek correspondence for programs, proofs and categories, this work lays the mathematical groundwork for a type checker for some resource theory based frameworks, with the possibility of extending it other quantum programming languages.

}, url = {https://arxiv.org/abs/1812.08726}, author = {Aarthi Sundaram and Brad Lackey} } @article {2279, title = {Morphisms in categories of nonlocal games}, year = {2018}, abstract = {

Synchronous correlations provide a class of nonlocal games that behave like functions between finite sets. In this work we examine categories whose morphisms are games with synchronous classical, quantum, or general nonsignaling correlations. In particular, we characterize when morphisms in these categories are monic, epic, sections, or retractions.

}, url = {https://arxiv.org/abs/1810.10074}, author = {Brad Lackey and Nishant Rodrigues} } @article {1859, title = {Mapping contrained optimization problems to quantum annealing with application to fault diagnosis}, journal = {Frontiers in ICT}, volume = {3}, year = {2016}, month = {2016/07/28}, pages = {14}, abstract = {

Current quantum annealing (QA) hardware suffers from practical limitations such as finite\ temperature, sparse connectivity, small qubit numbers, and control error. We propose new algorithms for\ mapping Boolean constraint satisfaction problems (CSPs) onto QA hardware mitigating these limitations.\ In particular, we develop a new embedding algorithm for mapping a CSP onto a hardware Ising model with\ a fixed sparse set of interactions and propose two new decomposition algorithms for solving problems too\ large to map directly into hardware. The mapping technique is locally structured, as hardware compatible\ Ising models are generated for each problem constraint, and variables appearing in different constraints are\ chained together using ferromagnetic couplings. By contrast, global embedding techniques generate a\ hardware-independent Ising model for all the constraints, and then use a minor-embedding algorithm to\ generate\ a hardware compatible Ising model. We give an example of a class of CSPs for which the scaling\ performance\ of the D-Wave hardware using the local mapping technique is significantly better than global\ embedding. We validate\ the approach by applying D- Wave\’s QA hardware to circuit-based fault diagnosis.\ For circuits that embed directly, we\ find that the hardware is typically able to find all solutions from a\ min-fault diagnosis set of size N using 1000 N samples,\ using an annealing rate that is 25 times faster than\ a leading SAT-based sampling method. Furthermore, we apply\ decomposition algorithms to find min-cardinality\ faults for circuits that are up to 5 times larger than can be solved directly on current hardware.

}, url = {http://journal.frontiersin.org/article/10.3389/fict.2016.00014/full}, author = {Bian, Zhengbing and Chudak, Fabian and Robert Brian Israel and Brad Lackey and Macready, William G and Aiden Roy} } @article {lackey2000metric, title = {Metric Equivalence of Path Spaces}, journal = {Nonlinear Studies}, volume = {7}, number = {2}, year = {2000}, month = {2000/01/01}, abstract = {Local equivalence and the invariants of systems of second order differential equations were studied in a series of papers by Kosambi, Cartan, and Chern. The resulting theory, deemed KCC-theory, is a rich geometric study which in many ways generalizes Riemannian and Finsler geometry. Yet, in many applications one requires a metric structure in addition to the systems of second order differential equations. We pose a geometry which is equipped with both of these structures, and solve the problem of local equivalence and thus determining a preferred connection and finding a generating set for all the invariants of the theory.}, author = {Brad Lackey} } @article {lackey1999model, title = {A model of trophodynamics}, journal = {Nonlinear Analysis: Theory, Methods \& Applications}, volume = {35}, number = {1}, year = {1999}, month = {1999/01/01}, pages = {37{\textendash}57}, publisher = {Pergamon}, doi = {10.1016/S0362-546X(98)00097-2}, author = {Brad Lackey} }