Lucas Dixon →
Teaching →
MSc Project: Discrimination nets for fast quantum reasoning

MSc Project Proposal: # Discrimination nets for fast quantum reasoning

Possible supervisors: Lucas Dixon,

`core-matching-tmp`

directory.
Algorithm Design

Formal methods: Specification Verification and Testing

Programming Languages and Functional Programming

Software Engineering

Formal methods: Specification Verification and Testing

Programming Languages and Functional Programming

Software Engineering

To investigate discrimination nets for the graph-based presentations
of compact closed categories and how this can speed up reasoning about
quantum information processing.

An important branch of research into quantum information has shown that quantum systems can be described as graph-based presentations of compact closed categories [1,2]. Additional structure, beyond that of the compact closed category, is captured as equations between graphs. Important characteristics of a quantum system can be seen graphically. For instance, separable states (non-entanglement) corresponds to disconnected components in a graph. By rewriting the graphical presentations, quantum information processing can be simulated and properties of quantum systems can be proved.

The process of rewriting graphs requires the left-hand side of a graphical rule to be found (matched) inside the graph being rewritten. When rules are stored in a list, the time to find the matching graphs increases linearly with the number of rules. This results in rewriting being prohibitively slow. The traditional solution employed by tree-based rewriting systems is to use a discrimination nets [3] to efficiently filter out most rewrites (typically in time logarithmic to the number of rules).

The aim of this project is to create a discrimination-net like algorithm for the graph-based presentations of compact closed categories. The project can be taken in a couple of directions, depending on the interests of the student:

- A more software-engineering based project would design, implement and empirically evaluate discrimination nets for the Quantomatic system [4].
- More theoretical analysis would design the algorithm, consider unification and/or investigate properties of the algorithms (such as correctness, completeness and run-time).

Nothing special; access to a DICE machine.

Students undertaking this project will need to be able to quickly understand the graph-matching definitions in [2]. However, given this, there are a variety of ways to tackle this project, from relatively easy metrics for filtering graphs, which can easily be implemented, to more a in-depth algorithm design and analysis.

Either knowledge of algorithms and run-time analysis, or familiarity with functional programming is needed.

- [1] A Categorical Quantum Logic. S. Abramsky, R. Duncan. In Mathematical Structures in Computer Science, 16 pages 469-489. 2006. http://www.comlab.ox.ac.uk/files/344/cql.pdf
- [2] Graphical Reasoning in Compact Closed Categories for Quantum Computation. L. Dixon and R. Duncan. Annals of Mathematics and Artificial Intelligence: Volume 56, Issue 1 (2009). http://dream.inf.ed.ac.uk/projects/quantomatic/papers/reasoning-graphically-amai08.pdf
- [3] Flatterms, discrimination nets, and fast term rewriting. Jim Christian. Journal of Automated Reasoning. 1993. http://www.springerlink.com/content/v5721675r8p0q301/
- [4] Quantomatic. http://www.dream.inf.ed.ac.uk/projects/quantomatic/