Linear type and quantum logic

[rht]

o/ I am currently figuring out how to do Birkhoff-von Neumann quantum logic operation in a quantum circuit, and found that the linear type (a subset of linear logic) has already been manifested in Rust, in particular in its borrow checker. I am looking for an advice / resource recommendation on:

• which file I should look at in this repo to see the borrow checker being used to ensure the no-cloning property.
• how you could solve systems that can be modeled in linear logic in RustQIP.
• if you know a specific example of a large scale system that is solved with linear logic, given that the resource interpretation. implies that it could be used to model energy-based currency/trade between systems.
• how to implement quantum logic in the language of quantum logic gates, essentially a reverse of [1], cc: @udallago

Another interpretation of linear logic, is to be considered as a 2-player game, as can be found in [2]

In A ⊗ B, play continues with both games in parallel. If it is our turn in either game, then it is our turn overall; if it is their turn in both games, then it is their turn overall. If either game ends, then play continues in the other game; if both games end, then the overall game ends. If we have won both games, then we have won overall; if they have won either game, then they have won overall.

[1] https://arxiv.org/abs/1210.0613
[2] https://ncatlab.org/nlab/show/linear+logic#game_semantics_2

[Renmusxd]

Hi,

Its not so much that a single file is supporting the no-cloning stuff. Rather it's that qubit registers are tied to handles which don't support copy or clone, so the user is forced to only ever have a single handle to a given qubit. The upshot of this restriction is that it enforces the order of unitary gates. You cannot, for example, have two references to a single qubit before a unitary is applied, you cannot "clone" the state before the gate.

• I have not directly supported linear logic or such abstractions in this library, really this library focuses on quickly building circuits and simulating them efficiently using a custom schrodinger-style algorithm (see qip-iterators). I do not yet support graph manipulation inside the circuit well, it's something I'd like to work on.