[isabelle] [Isabelle] Abstract Field Theory (was: Quantum Computing)

[José Manuel Rodriguez Caballero]

I would like to point out a project I started a few weeks ago in case some
of you might be interested. It is a formalization of quantum computing
<https://github.com/AnthonyBordg/Isabelle_marries_Dirac> in Isabelle.
I should add a README file soon, but in the meantime if you have any
question please ask, you can also drop me an email.
There is a formalization of quantum mechanics which is part of a HOL
Light library of complex function vector spaces (
https://github.com/jrh13/hol-light/tree/master/Functionspaces). Using
this library, a tool for the verification of optical quantum circuits was
developed (https://github.com/beillahi/FMV-QC-HOL).

Just a little remark about the importance of abstraction (with respect to
the mathematical structure).

The main lesson of quantum physics is that nature is finite at its most
elementary level, with the only exception of the complex numbers in the
superpositions... Nevertheless, Felix Lev thinks that this is not an
exception, but just an approximation. According to Lev, the complex numbers
may be substituted in the future by a finite field F_q, where q is some
huge prime power, which will be determined in an experimental way, i.e.,
the prime power q will be a fundamental constant of the universe in the
same sense than the speed of light c or the universal gravitational
constant. Reference: Lev, Felix M. "Quantum theory and Galois fields."
*International
Journal of Modern Physics B* 20.11n13 (2006): 1761-1777.
https://www.worldscientific.com/doi/abs/10.1142/S0217979206034273?journalCode=ijmpb

So, a way to be prepared for a possible change in the formulation of
quantum mechanics is to develop a theory in Isabelle which contains both,
the quantum mechanics formulated with complex numbers (the traditional
quantum mechanics) and this new proposal of quantum mechanics over a finite
field, as particular cases, i.e., making abstraction with respect to the
field as it is done in Abstract Algebra. The following preprint contains a
description of the quantum computation over finite fields: James, Roshan
P., Gerardo Ortiz, and Amr Sabry. "Quantum computing over finite
fields." *arXiv
preprint arXiv:1101.3764*(2011). https://arxiv.org/abs/1101.3764

Maybe, when trying to build the first practical quantum computer, the
theory of quantum mechanics over F_q will begin to play a significative
role. Of course, the use of complex vector spaces is fine according to the
state of the art in quantum mechanics, but quantum physics is continuously
developing...

Kind Regards,
José Manuel Rodriguez Caballero