Email Gateway (Aug 22 2022 at 18:56): Email Gateway (Aug 22 2022 at 18:56):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi José,
I only skimmed over the paper, and from what I saw it is not clear to me whether
existing Isabelle libraries can do the computations:
1) In the paper I mostly see operations like matrix-addition, multiplication, etc.
All of these operations will be efficiently computed, by either using the
matrices in HOL-Analysis/Euclidean_Space or AFP/Jordan_Normal_Form/Matrix.
2) However, the oracle also mentions some library Sympy for symbolic manipulations.
So, if this would involve calculations over matrices with symbolic expressions inside, then
I’m not so sure whether that is supported.
Best,
René
Email Gateway (Aug 22 2022 at 18:58):From: Dominique Unruh <unruh@ut.ee>
Hi,
in https://github.com/dominique-unruh/qrhl-tool/ (file
isabelle-thys/QRHL_Code.thy), I have used AFP/Jordan_Normal_Form as a
backend for checking verification-conditions for finite-dimensional
predicates in a quantum Hoare calculus (so far, a lot in my developent is
only axiomatized, not proven, but it mostly just invokes the algorithms
from AFP/Jordan_Normal_Form). That works well. In my case, the predicates
involved are modeled as subspaces, and thus the verification conditions are
subspace inclusions. In [liu2016theorem], they consider a quantum Hoare
calculus where the predicates are Hermitian operators, so the
verification-conditions are of the form "A is a positive operator" which is
a more difficult problem. I have not checked whether the algorithms from
AFP/Jordan_Normal_Form can do that.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:01):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Dominique,
I’m not an expert here, but a quick web-search led me to the page:
https://www.gaussianwaves.com/2013/04/tests-for-positive-definiteness-of-a-matrix/
Here, 3 sufficient criteria are provided which can ensure positiveness. (I’m not sure about completeness)
All of these criteria can be implemented via the algorithms available in AFP/Jordan_Normal_Form:
1) only positive pivots: well this is an easy test, since Gauss-Jordan-elimination is available.
2) only positive determinants of upper-left sub-matrices: also easy, since determinants and taking
sub-matrices is supported.
3) only positive eigenvalues: in combination with algebraic numbers (AFP/Algebraic_Numbers) this is easy, since you just invoke
the factorization algorithm on the charateristic polynomial to compute the eigenvalues.
Only limitation: the input matrix must contain rational numbers as input, since otherwise the factorization
algorithm will most likely fail.
Cheers,
René
signature.asc
Email Gateway (Aug 22 2022 at 19:01):From: Dominique Unruh <unruh@ut.ee>
Hi René,
thanks for those pointers. I assume that the authors of [liu2016theorem]
either were not aware of AFP/Jordan_Normal_Form, or went for an external
oracle for simplicity or speed.
Some comments on the three approaches:
Here, 3 sufficient criteria are provided which can ensure positiveness.
(I’m not sure about completeness)
We need to be clear what we mean by "positive". In the context of
[liu2016theorem],
I think we need what is called more precisely "positive semidefinite"
(usually called positive in the quantum community). The page you linked, I
think, refers to positive-definite. So the criteria are slightly different.
All of these criteria can be implemented via the algorithms available in
AFP/Jordan_Normal_Form:1) only positive pivots: well this is an easy test, since
Gauss-Jordan-elimination is available.
I don't know what they mean by this. Consider the (0 1 \\ 1 0). This matrix
is negative. Gaussian elimination gives the identity which has only 1's on
the diagonal. So something's wrong here.
2) only positive determinants of upper-left sub-matrices: also easy, since
determinants and taking
sub-matrices is supported.
For positive-semidefinite, we need to check all sub-matrices (not just
upper-left). (https://en.wikipedia.org/wiki/Sylvester%27s_criterion) Thus
exponentially many!
3) only positive eigenvalues: in combination with algebraic numbers
(AFP/Algebraic_Numbers) this is easy, since you just invoke
the factorization algorithm on the charateristic polynomial to compute
the eigenvalues.
Only limitation: the input matrix must contain rational numbers as
input, since otherwise the factorization
algorithm will most likely fail.
And you can read off the eigenvalues directly from the Jordan normal form.
But the limitation to rational inputs might be a problem: Matrices involved
in quantum computing often involve [image: \frac{1}{\sqrt{2}}].
That being said, I think it might be interesting to explore this in more
detail to make [liu2016theorem] not rely on oracles.
Best wishes,
Dominique.
Cheers,
René
Email Gateway (Aug 22 2022 at 19:01):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Some comments on the three approaches:
Here, 3 sufficient criteria are provided which can ensure positiveness. (I’m not sure about completeness)
We need to be clear what we mean by "positive". In the context of [liu2016theorem], I think we need what is called more precisely "positive semidefinite" (usually called positive in the quantum community). The page you linked, I think, refers to positive-definite. So the criteria are slightly different.
Ok, agreed.
All of these criteria can be implemented via the algorithms available in AFP/Jordan_Normal_Form:
2) only positive determinants of upper-left sub-matrices: also easy, since determinants and taking
sub-matrices is supported.For positive-semidefinite, we need to check all sub-matrices (not just upper-left). (https://en.wikipedia.org/wiki/Sylvester%27s_criterion) Thus exponentially many!
Indeed, but still it is executable. So, if the matrices are small enough, this might be a feasible approach.
3) only positive eigenvalues: in combination with algebraic numbers (AFP/Algebraic_Numbers) this is easy, since you just invoke
the factorization algorithm on the charateristic polynomial to compute the eigenvalues.
Only limitation: the input matrix must contain rational numbers as input, since otherwise the factorization
algorithm will most likely fail.And you can read off the eigenvalues directly from the Jordan normal form.
Well, this does not help in algorithm in AFP/Jordan_Normal_Form: there, the JNF-computation demands a factorization
of the characteristic polynomial: it is based on Schur-decomposition which as input takes the list of eigenvalues.
But the limitation to rational inputs might be a problem: Matrices involved in quantum computing often involve 1/sqrt(2).
Interesting. Then perhaps approach 2) can be used now, and it will give me some motivation by trying to extend the
formalized factorization algorithm so that it can also deal with polynomials that have algebraic coefficients, not just rational.
Best,
René
Email Gateway (Aug 22 2022 at 19:01):From: Dominique Unruh <unruh@ut.ee>
Hi René,
2) only positive determinants of upper-left sub-matrices: also easy,
since determinants and takingsub-matrices is supported.
For positive-semidefinite, we need to check all sub-matrices (not just
upper-left). (https://en.wikipedia.org/wiki/Sylvester%27s_criterion) Thus
exponentially many!Indeed, but still it is executable. So, if the matrices are small enough,
this might be a feasible approach.
But we should not forget that this means that we also have to prove
Sylvester's theorem.
I don't know how difficult that is.
An easier approach (both algorithmically and in terms of what development
already exists) might be the following:
- Input: Matrix A.
- If A is not hermitian, return false. (Positive matrices are hermitian
by definition.)
- Compute the characteristic polynomial p of A. (Since A is hermitian, A
has only real eigenvalues, thus p is a polynomial with only real roots, and
thus has only real coefficients.)
- We use Sturm's theorem/algorithm (over the algebraic reals) to find
out if all roots of p are >=0. If so, return true. Otherwise, return false.
Of course, there might be even better algorithms for deciding positivity. I
am not an expert in that area.
Best wishes,
Dominique.
3) only positive eigenvalues: in combination with algebraic numbers
(AFP/Algebraic_Numbers) this is easy, since you just invoke
the factorization algorithm on the charateristic polynomial to
compute the eigenvalues.
Only limitation: the input matrix must contain rational numbers as
input, since otherwise the factorization
algorithm will most likely fail.And you can read off the eigenvalues directly from the Jordan normal
form.Well, this does not help in algorithm in AFP/Jordan_Normal_Form: there,
the JNF-computation demands a factorization
of the characteristic polynomial: it is based on Schur-decomposition which
as input takes the list of eigenvalues.But the limitation to rational inputs might be a problem: Matrices
involved in quantum computing often involve 1/sqrt(2).Interesting. Then perhaps approach 2) can be used now, and it will give me
some motivation by trying to extend the
formalized factorization algorithm so that it can also deal with
polynomials that have algebraic coefficients, not just rational.Best,
René
Email Gateway (Aug 22 2022 at 19:02):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Just to emphasize that the decision problem
INPUT: A Hermitian matrix H of order n whose entries are computable complex
numbers.
OUTPUT: Is H positive semidefinite?
is undecidable.
Indeed, consider an arbitrary computational real number x. Let H be the
matrix of order 1 whose single entry is x. Notice that x is equal to zero
if and only if both H and -H are positive semidefinite. On the one hand, if
the above-mentioned problem was decidable, then we will be able to decide
whether x is equal to zero or not. On the other hand, we can encode the
halting problem as the proposition: x is equal to zero. Thus, the
above-mentioned problem is undecidable.
Therefore, the function of the oracle in
Liu T, Li Y, Wang S, Ying M, Zhan N. A theorem prover for quantum Hoare
logic and its applications. arXiv preprint arXiv:1601.03835. 2016 Jan 15.
https://arxiv.org/pdf/1601.03835.pdf
is not to decide whether the matrix H is positive semidefinite, but just to
provide a proof in cases where it is possible to do it in Python, e.g., if
the entries of H are algebraic numbers, etc. Of course, we can think about
an oracle solving the above-mentioned decision problem, but such an oracle
will be non-computable.
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 19:02):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
I tend to be skeptical with respect to the mathematical meaning of the
claims of the paper:
Liu T, Li Y, Wang S, Ying M, Zhan N. A theorem prover for quantum Hoare
logic and its applications. arXiv preprint arXiv:1601.03835. 2016 Jan 15.
https://arxiv.org/pdf/1601.03835.pdf
https://github.com/ijcar2016/propitious-barnacle
I feel that something essential is missing in the space between
Isabelle/HOL and Python. For example, in the lemma
lemma grover: "valid I
((((Init q0 0);Init q1 1;Init q 2;Init r 3;
Utrans Delta 2;Utrans H 0;Utrans H 1;Utrans H 2);
While M0 M1 C Q);
Cond [(N0,SKIP,p0),(N1,SKIP,p1),(N2,SKIP,p2),(N3,SKIP,p3)] )
P"
on the one hand, we have that both I and P are just formal symbols
satisfying some axioms, which happens to be satisfied also by square
matrices having complex coefficients. On the other hand, in Python, these
symbols are interpreted as concrete matrices. I feel a gap. I propose two
approaches in order to make sense of this situation.
---Approach I.
I think that the rigorous way to justify the use of the oracle in Python is
as follows:
(a) we need to define I, P, and all the other formal symbols, as matrices
having complex numbers as entries in Isabelle/HOL;
(b) we need to embed Python in Isabelle/HOL;
(c) we need to prove the correctness of the algorithm for deciding the
positive semidefiniteness of the matrices (assuming that the entries are
algebraic numbers) in the embedding of Python in Isabelle/HOL.
Of course, we can forget Python and implement the algorithm for deciding
the positive semidefiniteness of the matrices (assuming that the entries
are algebraic numbers) in Isabelle/HOL. I recall that for any complex
number z, we have:
AlgebraicNumber(z) = there exists a polynomial P(X) ,having integer
coefficients, such that P(z) = 0.
I think that the hypothesis AlgebraicNumber(z) is essential for the oracle
to make sense, because without any restriction, the problem concerning the
positive semidefiniteness is undecidable.
---Approach II. Do everything in Python and formally verify what we did in
Isabelle/HOL using an embedding of Python.
I am not claiming that there is a problem in this paper. I am only pointing
out the parts where I am not convinced yet. Suggestions and criticism are
welcome.
Kind Regards,
José M.
Last updated: Apr 25 2024 at 12:23 UTC