Idris2Doc : Quantum.Gates

Quantum.Gates

Reexports

importpublic Matrix

Definitions

gate : Numa=> (1_ : Matrixr1c1a) -> (1_ : Matrixc1na) ->Matrixr1na
  Apply a quantum gate to a quantum system via matrix multiplication.
Example: `gate (H >< ID) myVec`
Note: Both inputs to `gate` are linear.

Visibility: export
(|>) : Numa=> (1_ : Matrixc1na) -> (1_ : Matrixr1c1a) ->Matrixr1na
  An infix operator for `gate`.
m |> g = gate g m

This is useful for chaining gates together.

Visibility: export
Fixity Declaration: infixl operator, level 4
ID : Matrix22Double
  The Identity gate. This gate does nothing.

Visibility: public export
IDN : (n : Nat) ->MatrixnnDouble
  The Identity gate of size `n`. where `n` is the rows and cols of the matrix.

Visibility: public export
X : Matrix22Double
  The Pauli-X gate. This gate flips the state of a qubit.
This is equivalent to the classical NOT gate.

Visibility: public export
H : Matrix22Double
  The Hadamard Gate.
This gate acts upon a single qubit and puts it into a superposition.

Visibility: public export
CNOT : Matrix44Double
  Controlled Not Gate.
This gate flips the second qubit if the first qubit is in the state |1>.

NOTE: This gate is only defined for 2 qubits that are adjacent to each other.
Use `CNOTN` for non adjacent qubits.

Visibility: public export
pow2 : Numa=>Nat->a
  A helper function to calculate the powers of 2.

Visibility: public export
COND : (n : Nat) ->Matrix (pow2 (minusn1)) (pow2 (minusn1)) Double->Matrix (2*pow2 (minusn1)) (2*pow2 (minusn1)) Double
  Conditional gate. Applies a gate to a system if the control bit is |1>
n is the number of qbits in the system (including the control bit)
See https://quantumcomputing.stackexchange.com/questions/4252/how-to-derive-the-cnot-matrix-for-a-3-qubit-system-where-the-control-target-qu

Visibility: public export
measurePure : Double-> (1_ : QSystemn) ->QSystemn
  Deterministically measure a quantum system

Visibility: export
measure : (1_ : QSystemn) ->Q (QSystemn)
  Non-deterministically measure a quantum system

Visibility: export