Checking Equality about pytket-docs HOT 6 CLOSED

I ask for the following reason:
I have a PyZX circuit I want to simplify and am benchmarking against FullPeepholeOptimise. So, I am doing the following:

# c is a PyZX circuit
c_tket = pyzx_to_tk(c)
FullPeepholeOptimise().apply(c_tket)

RebasePyZX().apply(c_tket)
c_opt = tk_to_pyzx(c_tket)

However, c.verify_equality(c_opt) then returns False. This could mean one of several things:

• FullPeeopholeOptimise is violating the agreement that it doesn't change what the circuit does (maybe I have a misunderstanding of this/this is not true?)
• PyZX's verify_equality has a bug
• tk_to_pyzx has a bug. This seems unlikely as I also tried by going through a QASM string and got the same error

from pytket-docs.

Pytket itself doesn't have a method for checking semantic equality; however, you can do this using one of the statevector or unitary backends, such as the AerUnitaryBackend (which computes the full unitary corresponding to a circuit).

FullPeepholeOptimise should preserve the semantics. Note that compilation passes do sometimes introduce initial and final qubit mappings, which have the effect of permuting the qubits before and after the circuit, or implicit qubit permutations, but I don't think these would apply in this case. If you slightly modify your code as follows:

from pytket.predicates import CompilationUnit
c_tket = pyzx_to_tk(c)
cu = CompilationUnit(c_tket)
FullPeepholeOptimise().apply(cu)
c_tket, initial_map, final_map = cu.circuit, cu.initial_map, cu.final_map
implicit_perm = c_tket.implicit_qubit_permutation()

then if initial_map or final_map or implicit_perm is not the identity this could explain the apparent difference.

If you could attach your circuit c (or converted circuit c_tket) I'd be happy to have a look.

from pytket-docs.

I also note that pyzx's verify_equality "returns True if full_reduce() is able to reduce the composition of the circuits to the identity." So the fact that it returns False may mean that full_reduce was not able to do this, even if the circuits were equivalent.

from pytket-docs.

Thanks so much for the help! A couple of notes:

• What do you mean in saying that FullPeepholeOptimise might introduce initial/final qubit mappings? How would one recognize this and make the appropriate swaps? Could you explain a bit more about initial_map and final_map, and the role of implicit_qubit_permutation in the above code?
• Agreed re. verify_equality. Was looking for a way to verify that it was not on the tket end of things
• I've attached the failing circuit (in QASM format but saved as a text file to keep github happy)
  qubits-10_depth-100_9.txt

from pytket-docs.

Initial and final maps are explained in the manual here. They are worth knowing about but they are not actually relevant in this case.

Implicit qubit permutations are explained in the manual here. The passes you are applying may apply an implicit permutation to the circuit, which you can inspect; this allows us to eliminate some swap gates from the circuit.

The presence of this permutation could explain the fact that pyzx doesn't see these as equivalent, because it is not taken into account by tk_to_pyzx,

You may still use the AerUnitaryBackend from pytket-qiskit to check equivalence, because this does take the implicit permutation into account. The following code shows that they are in fact unitarily equivalent. (I just had to rename your file to end in ".qasm".)

from pytket.passes import FullPeepholeOptimise, RebasePyZX
from pytket.qasm import circuit_from_qasm
from pytket.backends.ibm import AerUnitaryBackend
import numpy as np

b = AerUnitaryBackend()

c_tket = circuit_from_qasm("qubits-10_depth-100_9.qasm")

u = b.get_unitary(c_tket)

FullPeepholeOptimise().apply(c_tket)
RebasePyZX().apply(c_tket)

u1 = b.get_unitary(c_tket)

assert np.allclose(u, u1)

from pytket-docs.

Thank you so much!

from pytket-docs.