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