Symbolic system for Quantum computing

To install, type ] in a julia (>=1.5) REPL and then input

pkg> add https://github.com/overshiki/SymbolicCircuit.jl

To define and simplify a quantum circuit, just do

using SymbolicCircuit
x1 = UGate(gX(), [Loc(1), ])
h2 = UGate(gH(), [Loc(2), ])
y3 = UGate(gY(), [Loc(3), ])
circ = x1 * x1 * h2 * y3 * x1 * x1 * h2
ncirc = egraph_simplify(circ, Val(:default_rule))

It will simplify circ into ncirc according to commute and cancel rules.

To test if two circuit are in equivalent according to commute and cancel rules, just do

SymbolicCircuit.areequal(Val(:default_rule), circ, ncirc)

It will return true if circ and ncirc are in equivalent, otherwise missing.

SymbolicCircuit.jl also provides method to turn symbolic circuit defined above to YaoBlock in Yao.jl, so that the full power of Yao.jl would be avaliable

yao_circ = to_yao(circ; num_qubits=3)
println(yao_circ)

To plot the circuit, just do

to_yaoplot("./test/plot.png", circ)

It will plot the circuit using YaoPlots.jl

SymbolicCircuit.jl provides a symbolic system for representation of Quantum circuit, in which, one can manipulate Quantum circuit using term rewriting & equality saturation techniques. Using this package, one can easily define any syntactic rules of Quantum circuit(for example, mutation between two quantum gates), and apply it to term rewriting and equality saturation Modules provided by Metatheory.jl (Yes, This project is highly dependent on and highly motivated by Metatheory.jl). Doing so, tasks such as circuit simplification, equivalence detection, code generation become easily achievable.

In SymbolicCircuit.jl, quantum gates are represented by the instances of Gate struct, for example, the Pauli X gate on 1st Qubit is defined by

using SymbolicCircuit
x1 = UGate(gX(), [Loc(1), ])

Where UGate is alias for Gate{Normal}, where the counterpart is Gate{Dagger} which stands for daggered version of UGate.
gX() represents the type of Pauli X(gX is short for gate X), Loc(1) indicates the gate is applied on Qubit 1. We can also define multi-Qubits gate, for example, CNOT gate on 1st Qubit and controlled by 2nd Qubit

cnot_1c2 = UGate(gX(), [Loc(1), cLoc(2)])

Where cLoc(2) indicates the gate is controlled by 2nd Qubit

We can also define parametric gate such as rotate X, controlled by parameter :theta

rx = UGate(rX([:theta, ]), [Loc(3), ])

Since simplifying many VQE circuits will often result in rotate gate controlled by multiple parameters(sum of multiple rotate angles), we also allow this

rx2 = UGate(rX([:theta1, :theta2, :theta3]), [Loc(3), ])

It is wellknown that, symbolically, quantum circuit is just a chain of quantum gate, applied from left to the right. In SymbolicCircuit.jl, we define quantum circuit as expression of gates connected by * operator.

using SymbolicCircuit
x1 = UGate(gX(), [Loc(1), ])
h2 = UGate(gH(), [Loc(2), ])
y3 = UGate(gY(), [Loc(3), ])
circ = x1 * x1 * h2 * y3 * x1 * x1 * h2

This allows flexible ways of defining a circuit, for example, we can also

using SymbolicCircuit
let circ = head_circuit()
    for _ in 1:2
        for g in [x1, h2, y3]  
            circ *= g 
        end 
    end
end

The core idea of SymbolicCircuit.jl is that quantum circuit can be represented using symbolic expression and some rules(such as mutation rules) can be represented using syntactic rules of the expressions. Then term rewriting & equality saturation system could be used to manipulate the circuit. In SymbolicCircuit.jl, we provide easy ways to define different type of syntactic rules one may imagine. For example, a simple commute rule and cancel rule can be defined

using SymbolicCircuit
using Metatheory

#commute rules
com_rule = @rule a b a::Gate * b::Gate => :($(b) * $(a)) where is_commute(a, b)

#cancel rules
can_rule = @rule a b a::Gate * b::Gate => One() where is_cancel(a, b)

Where is_commute and is_cancel are functions provided in src/gate.jl to determine if two gates are commute and if they could be cancelled out. Currently, is_commute considers two cases:

• gate a and gate b do not have common Loc or cLoc
• gate a/b is a Z|S|T gate, and gate b/a is a CNOT gate, where cLoc of b/a has the same index with Loc of a/b

is_cancel considers two cases:

• gate a and gate b are identical and they belong to unitary & Hermitian gate
• gate a/b is the dagger version of gate b/a

Note that the rule defination process here is just a normal rule defination process in Metatheory.jl(users can also define rewrite rule using --> and equality rule using ==, following the document of Metatheory.jl), what SymbolicCircuit.jl provides is a system of gate expression and circuit expression where Metatheory.jl could be applied to.

Addtionally, SymbolicCircuit.jl also provides some built-in rules for applications including circuit simplification, equivalence detection(and code generation in the next release). They are included in src/rule.jl. Users of SymbolicCircuit.jl could of course define more rules they would like to. For more details, one can refer to the tutorial on how to do this.

The core operation of SymbolicCircuit.jl is to apply a variaty of syntactic rules to term rewriting & equality saturation system provided by Metatheory.jl, which allows powerful circuit manipulate functions. For example, term rewriting could be used to transform all Pauli Z gates in a circuit into H X H following rewriting rule Z=HXH. This could be easily handled using SymbolicCircuit.jl

using SymbolicCircuit
using SymbolicCircuit: is_Z, is_commute, is_cancel
using Metatheory
using Metatheory: PassThrough, Postwalk

x1 = UGate(gX(), [Loc(1), ])
y3 = UGate(gY(), [Loc(3), ])
z2 = UGate(gZ(), [Loc(2), ])
z3 = UGate(gZ(), [Loc(3), ])

circ = x1 * z2 * y3 * z3 * x1 * z3

function get_HXH(a::Gate)
    h = UGate(gH(), a.loc)
    x = UGate(gX(), a.loc)
    return :($(h) * $(x) * $(h))
end

r = @rule a a::Gate => get_HXH(a) where is_Z(a)
r = Postwalk(PassThrough(r))
@show Circuit(r(circ.expr))

Of course, this is just a simple rewriting rule, and could be done using any non-symbolic systems such as direct coding in qiskit|Yao.jl|mindquantum|...(for example, in mindquantum, circuits are represented as object of List class in python, such manipulation could be easily done using pop and insert operations).

The full power of SymbolicCircuit.jl comes from the qquality saturation techniques in symbolic & compiler community. In equality saturation(Eqsat), the term rewriting are allowed to be handled without an order. For example, bidirectional rules such as gate commute rule a*b==b*a are allowed. The key point of Eqsat is that it allows all combination of rewriting operations to be stored in memory(usually in efficient EGraph data structure as implemented in Metatheory.jl), and efficiently traversed. Thus one could set the search goal to search for specific expressions in all equivalent expressions resulted from the rewriting rules, which would be a complex task for non-symbolic systems without Eqsat techniques, such as qiskit|Yao.jl|mindquantum|...

To demonstrate, let's consider circuit simplification operation. We consider only a combination of commute rule a*b==b*a where a, b commute and cancel rule a*b->0 where a, b could be cancelled. These simple rules already provide a strategy to simplify a circuit, i.e. for any pair of gates in a circuit, commute if possible, cancel if possible, and then try more commutation and cancellation, until no progress could be made. In a non-symbolic system without Eqsat, such strategy could only be implemented using a heuristic approach without a saturation guarantee(or it could have saturation guarantee but need a lot of codings). In SymbolicCircuit.jl it would be easily achiveable and has a guarantee that all possible combination are traversed.

using SymbolicCircuit
using Metatheory
using Metatheory.Library: @right_associative, @left_associative
v = AbstractRule[]
push!(v, @rule a b a::Gate * b::Gate => :($(b) * $(a)) where is_commute(a, b))
push!(v, @rule a b a::Gate * b::Gate => One() where is_cancel(a, b))
push!(v, @rule a b b::One * a::Gate => :($(a)))
push!(v, @rule a b a::Gate * b::One => :($(a)))

ra = @right_associative (*)
la = @left_associative (*)
push!(v, ra)
push!(v, la)

function simplify(circuit)
    g = EGraph(circuit)
    params = SaturationParams(timeout=10, eclasslimit=40000)
    report = saturate!(g, v, params)
    circuit = extract!(g, astsize)
    return circuit
end 

circ = x1 * x1 * h2 * y3 * x1 * x1 * h2
ncirc = simplify(circ)

result:

UGate(gY(), Q[Loc(3)])

Another powerful function provided by the system is that, it allows to detect if two circuit are in equivalence under certain rules. For example, continue from the above circuit simplification task, just do

areequal(v, circ, ncirc)

results in:

true

will tell if circ and ncirc are in equivalent under the rules v.

For those want to use SymbolicCircuit.jl as openbox toolset for some practical task, SymbolicCircuit.jl currently provides built-in functions including: circuit simplification, equivalence detection, where a default set of syntactic rules is used. (more simplification target and code generation function are on the way) The list of the functions are:

egraph_simplify: circuit simplification using default set of rules

circ = x1 * x1 * h2 * y3 * x1 * x1 * h2
circ = egraph_simplify(circ, Val(:default_rule); verbose=false)

areequal: overload of areequal function in Metatheory.jl, using default set of rules

SymbolicCircuit.areequal(Val(:default_rule), circ1, circ2, circ3)

For more information, please refer to test folder. Issue and PR are welcomed.

- Some examples in example folder
- More rewriting rules
- T-gate reduction functions
- Codegen for numerical simulation
- Documentations!