Quantum algebra development

[wwitzel]

Make enhancements and fixes to the quantum algebra package, including the following as a first batch of updates:

1. Fix the bra_def axiom and KEEP the qmult_of_bra_as_map theorem. qmult_of_bra_as_map has the proper form (accounting for the different conventions between Physicists and Mathematicians as noted above qmult_of_bra_as_map).
   a) Replace bra_def with this form (and move the 'different conventions' comment to above 'bra_def') EXCEPT remove the Qmult(..) wrapper around Bra(varphi).
   b) KEEP qmult_of_bra_as_map in the quantum algebra theorems.
   c) RESTORE occurrences of 'qmult_of_bra_as_map' (e.g., in qmult.py).
2. Add a Qmult.projection method that will instantiate the bra_def
   a) Decorate this method with "@equality_prover('projected', 'project')
   b) Check that there are two operands we'll denote here as M and |ψ⟩. Otherwise, raise ValueError.
   c) Add the following lines near the top of Qmult.linmap_reduction:
   from proveit.physics.quantum import QmultCodomain
   # In the process of proving that 'self' is in QmultCodomain,
   # it will prove it is a linear map if it can.
   QmultCodomain.membership_object(self).conclude()
   d) Execute "linmap_eq = Qmult(M).linmap_reduction()"
   e) import and instantiate 'qmult_op_ket ' with {A:Qmult(<φ|), Hspace: known Hilbert space of |psi>, X: Complex, var_ket_psi: |ψ⟩}. Assign to 'qmult_eq'. NOTE CHANGE: where 'Qmult' now appears.
   f) return linmap_eq.sub_right_side_into(qmult_eq.inner_expr().rhs.operator)
   g) NOTE CHANGE: no bra_def instantiation. Test on the demonstrations page.
3. Add a theorem for that equates the self-projection to its norm:
   a) Something like: forall_{𝓗 in the class of Hilbert spaces} forall_{|ψ⟩ in 𝓗} ⟨ψ||ψ⟩ = || |ψ⟩ ||^2
   b) Handle this special case in Qmult.projection
   c) As a bonus, prove this theorem via bra_def and norm_def (in proveit.linear_algebra.inner_products)
4. Implement and test Qmult.evaluation.
   a) In Qmult.shallow_simplification, insert an 'if' block before the return statement check if 'must_evaluate' is True. If so,
   b) If expr is an instance of ScalarMult, do
   expr = eq.update(expr.inner_expr().scaled.projection())
   c) Otherwise do:
   expr = eq.update(expr.projection())
   d) Then, either way, do "expr = eq.update(expr.evaluation())".
   e) Test on demonstration page.

[sudhindu]

Comment for Testing purposes.

[wwitzel]

I see your comment. Your test worked, Sudhindu. 😊

[vsprasannaa]

Test comment.

[wwitzel]

Note that I modified steps 1 and 2 above, @sudhindu. In the previous instructions, I wasn't appreciating the subtle distinction between a Bra and the Qmult of a Bra (they are logically equal to each other but different expressions). I hope the instructions are clear. I did test it out, so it should work if I've managed to explain it correctly. You'll have to undo some of the changes you made before, but it shouldn't be too bad. Good luck and best wishes.

[wwitzel]

And here's a bonus as step 5.
5. Prove the 'qmult_of_bra_as_map' theorem.
Hints: import defaults from proveit and set 'defaults.assumptions' to 'qmult_of_bra_as_map.conditions'
import and instantiate 'bra_def', and 'qmult_of_bra'
You can use default instantiation but with 'num_forall_eliminations=2'.
When instantiating 'qmult_of_bra', you'd want to also use 'auto_simplify=False'. Try it both ways to see what happens. auto-simplification is nice, but sometimes it can have undesirable effects on occasion.
'apply_transitivity' of one of these equations on the other.
Then '%qed'. That should cover it.

[wwitzel]

As step 6, I suggest that you add "no_cloning" as a theorem in proveit.physics.quantum.algebra. Go to the proveit.physics.quantum.algebra theorems page and insert a cell for specifying the "no_cloning" between %begin and %end. This step is just to formulate the expression for the "no_cloning", not to prove it just yet. I'm thinking this expression would look something like
forall_{N in NaturalPos} notexists_{U in Unitary(N)} forall_{a, b | |a> in C^N, |b> in C^N} ...
Think carefully about how this should be stated as a formal expression.

[wwitzel]

As a next step for the "no_cloning", you may want to add the following to the quantum.algebra package:
adjoint_binary_distribution = ∀_{H, X, Y ∈_c HilbertSpaces} ∀_{A, B | [A] ∈ LinMap(X, Y), [B] ∈ LinMap(H, X)} Adj(Qmult(A, B)) = Qmult(Adj(B), Adj(A))

Just copy qmult_op_op for everything except the equality instance expression.

If you are implementing the Wootters and Zurek proof of the no-cloning theorem, this step may not be necessary. Feel free to skip it if you don't need it. But if you do not it, the following describes how to implement a method for applying this theorem.

To apply this theorem, you could make a "@equality_prover('distributed', 'distribute')" method in the Adj class called "distribution". The Adj class is in the linear_algebra package (under inner_products). The theorem we want to apply is a Qmult theorem. We don't want the linear_algebra package to refer to the quantum_algebra package because linear algebra should be independent of anything quantum. But we can exploit Python's duck-typing flexibility -- we don't need to know what class something is to call one of its methods. In the Adj.distribution method we can check to see if the operand has a method called "adjoint_distribution" via hasattr. If it does, have it return "self.operand.adjoint_distribution()". Then make an "@equality_prover('adjoint_distributed', 'adjoint_distribute')" method in the Qmult class called "adjoint_distribution" that does the actual instantiation of adjoint_binary_distribution. I think you can use "containing_hilbert_space_linmap_sets" to get the H, X, Y values for instantiation (from the "to_vspace" and "from_vspace" attributes); you can look at examples in qmult.py for how to do this (search form "containing_hilbert_space_linmap_sets").

[wwitzel]

Another step that we discussed when we met last is a quantum algebra version of
tensor_prod_of_linear_maps (which is a theorem in proveit.linear_algebra.tensors).
The quantum algebra theorem form would use Qmult in place of Function:
"Qmult(TensorProd(A_1_to_n), TensorProd(v_1_to_n))" instead of
"Function(TensorProd(A_1_to_n), TensorProd(v_1_to_n))"
and
"Qmult(A_i, v_i)" instead of "Function(A_i, v_i)".
As an exercise, you may want to prove this quantum algebra form from the linear_algebra using qmult_op_is_linmap and qmult_op_ket (I think).

We'll want an equality_prover method to apply this theorem. I'm not sure what a good name might be. I kind of think of it as a kind of distribution, but they may not be an appropriate term for this way of pairing up tensor product operands. I'll leave this name (along with the different tense forms for the @equality_prover) up for debate. As for its implementation, TensorProd.compute_norm might be a reasonably good example to follow and adapt. It's an example of dealing with any number of operands. In this case, we have two operands, but they both have some arbitrary number of TensorProd operands. To instantiate the theorem, you need get this 'n' by calling num_elements() on one of the two TensorProd operands. You'd get V1, ..., Vn from VecSpaces.known_vec_spaces, and you'd get W1, ..., Wn from "containing_hilbert_space_linmap_sets", the "to_vspace" attribute in particular. You can look at examples in qmult.py for how to use "containing_hilbert_space_linmap_sets".

This is going to be a little more challenging than previous exercises. Dealing with arbitrary numbers of operands takes some practice and there are some nuances. I expect there to be questions and roadblocks. Try not to get discourages. We are happy to help and understand that this takes practice.

[sudhindu]

@wwitzel thanks for your suggestions, I will do it.

[wwitzel]

When we met last @sudhindu and Akshaya were noting an error occuring when running their demonstrations notebook in the quantum algebra package. The error was in proving a certain Qmult is logically in the QmultCodomain class (note that class membership is more general than set membership -- all mathematical objects in a class share certain properties but you can't always form subclasses in the same way that you can form subsets). We dug into what was happening into the failing call to InClass.conclude and compared it to the old version that succeeds. What we found was that InClass.conclude "tries" Relation.conclude and if that fails with a ProofFailure then it moves on to try "self.membership_object.conclude()" which succeeds. In @sudhindu's version, however, the Relation.conclude method fails with a different error than a ProofFailure. There are two ways we can fix this. One way is to implement "_readily_provable" in the QmultCodomainMembership class (Python 'class', not logical 'class') in qmult.py. The other is to make sure that the Relation.conclude method fails with a ProofFailure. The former has the benefit that it won't bother trying Relation.conclude to prove such things in the first place. But it wouldn't be so easy to implement this. One would have to go through all of the cases that are handled in QmultCodomainMembership.conclude and mirror them in QmultCodomainMembership._readily_provable and return True for all of the cases that would succeed when calling that conclude method (without actually executing the instantiation of a Prove-It judgment). It may not be terrible but would require some thought. Perhaps I'll do it in the near future, but it may not be this weekend. The latter fix should be simple and is what I recommend for @sudhindu. The reason Relation.conclude is failing with something other than ProofFailure is because linmap_reductionin qmult.py returns None in certain instances when it isn't applicable. Let's do this:

1. At the end of Qmult.linmap_reduction, put
   raise ValueError("%s does not evaluate to a linear map"%self")
2. In Qmult.shallow_simplification where it is calling linmap_reduction, wrap it in "try: ... except ValueError: pass" blocks. So then when it gets a ValueError, it will just move on.
   Let me know if that works.

[sudhindu]

@wwitzel I followed your instructions as you directed. I inserted the "raise ValueError("%s does not evaluate to a linear map" % self)" statement at the end of the Qmult.linmap_reduction method. The linmap_reduction() method is not directly called from Qmult.shallow_simplification(). Instead, within the shallow_simplification() method, the projection() method is invoked, and within the projection() method, the linmap_reduction() is implemented. Consequently, I enclosed the exception handler in the Qmult.shallow_simplification() method, specifically where the projection() method is called [at line number 159 of Qmult.py]. Despite these changes, I am still encountering an error, and the error message reads: "ValueError: [|varphi〉] does not evaluate to a linear map.