Quipper.Algorithms.BF.BooleanFormula

This module contains the implementation of the various quantum circuits that make up the boolean formula algorithm. Please see Quipper.Algorithms.BF.Main for an overview of the boolean formula algorithm.

Classical data structures

Oracle description

We define a data structure to hold the various parameters that are used to define an oracle.

data BooleanFormulaOracle

The input to the BF Algorithm is the description of an oracle to represent a given size of hex board, and a given size for the phase estimation register.

Constructors

BFO

Fields

• oracle_x_max :: Int

  The x-dimension of hex board.

• oracle_y_max :: Int

  The y-dimension of hex board.

• oracle_t :: Int

  Size of phase estimation register.

• oracle_s :: Int

  Number of moves remaining. This should start as x⋅y, if no moves have been made.

• oracle_m :: Int

  Size of the direction register, i.e., size of labels on the BF tree. This should be the ceiling of log(x⋅y).

• start_board :: HexBoard

  A description of the starting state of the board, and can be used to calculate s.

• oracle_hex :: HexCircuit

  An extra flag that we can use so that different HEX circuits can be used instead of the full circuit.

data HexCircuit

A type to define which Hex circuit to use.

Constructors

Hex

The actual Hex circuit.

Dummy

A Dummy Hex circuit.

EmptyHex

Nothing.

createOracle :: Int -> Int -> Int -> BooleanFormulaOracle

Create an oracle description. This only requires x, y, and t to be specified, as the remaining values can be calculated. The number of moves remaining, s, is calculated as the total number of squares on the board, and m is calculated as the number of bits required to represent s+1.

update_hex :: BooleanFormulaOracle -> HexCircuit -> BooleanFormulaOracle

A function to set the "Dummy" flag in the given oracle to the given HexCircuit value.

update_start_board :: BooleanFormulaOracle -> HexBoard -> BooleanFormulaOracle

Update the start_board in the given oracle, with the given HexBoard. This also updates the oracle_s field of the oracle to be in line with the new start_board.

full_oracle :: BooleanFormulaOracle

An oracle for a 9 by 7 Hex board, with the parameters: x=9, y=7, t=189. The calculated values are: s=63, m=6.

test_oracle :: BooleanFormulaOracle

A smaller oracle for testing purposes. The numbers should be chosen such that x⋅y = 2ⁿ−1 for some n. Here, we set x=3 and y=5, to give x⋅y=15. We arbitrarily set the size of the phase estimation register to t=4.

Hex boards

type HexBoard = ([Bool], [Bool])

A hex board is specified by a pair of lists of booleans. For a board of size x by y, each list should contain x⋅y elements. The first list is the "blue" bitmap, and the second is the "red" maskmap.

moves_made :: HexBoard -> Int

A function to determine how many moves have been made on a given HexBoard. This function assumes that the given HexBoard is valid, in the sense that no duplicate moves have been made.

empty_spaces :: HexBoard -> [Int]

A function to determine which spaces are still empty in the given HexBoard. This function assumes that the given HexBoard is valid, in the sense that no duplicate moves have been made. This function will return a list of all the empty spaces remaining, in strictly increasing order.

Quantum data structures

Some data structures to help in defining the algorithm.

type PhaseEstimationRegister = [Qubit]

The phase estimation register is a simple register of qubits. This is kept separate from the rest of the BooleanFormulaRegister as it is this register which will be measured at the end of the algorithm.

type GenericDirectionRegister a = [a]

The direction register is a simple register of qubits, made explicit here so we can see that a "position" is a list of directions.

type DirectionRegister = GenericDirectionRegister Qubit

A type synonym defined as the Qubit instance of a GenericDirectionRegister.

data GenericBooleanFormulaRegister a

The rest of the boolean formula algorithm requires a register which is split into 3 main parts.

Constructors

BFR

Fields

• position_flags :: (a, a)

  The position register is split into two parts: the leaf and paraleaf "flags".

• position :: [GenericDirectionRegister a]

  The current position, and how we got there, i.e., directions we followed. Any position can be reached by at most x⋅y directions.

• work_leaf :: a
• work_paraleaf :: a
• work_binary :: a
• work_height :: a
• work_r :: a
• work_rp :: a
• work_rpp :: a

  Seven flags that make up the work register.

• direction :: GenericDirectionRegister a

  The direction register.

Instances

Show a => Show (GenericBooleanFormulaRegister a)

Defined in Quipper.Algorithms.BF.BooleanFormula

Methods

showsPrec :: Int -> GenericBooleanFormulaRegister a -> ShowS

show :: GenericBooleanFormulaRegister a -> String

showList :: [GenericBooleanFormulaRegister a] -> ShowS

QCData a => QCData (GenericBooleanFormulaRegister a)

Defined in Quipper.Algorithms.BF.BooleanFormula

Methods

qcdata_mapM :: Monad m => GenericBooleanFormulaRegister a -> (q -> m q') -> (c -> m c') -> QCType q c (GenericBooleanFormulaRegister a) -> m (QCType q' c' (GenericBooleanFormulaRegister a))

qcdata_zip :: GenericBooleanFormulaRegister a -> q -> c -> q' -> c' -> QCType q c (GenericBooleanFormulaRegister a) -> QCType q' c' (GenericBooleanFormulaRegister a) -> ErrMsg -> QCType (q, q') (c, c') (GenericBooleanFormulaRegister a)

qcdata_promote :: BType (GenericBooleanFormulaRegister a) -> GenericBooleanFormulaRegister a -> ErrMsg -> BType (GenericBooleanFormulaRegister a)

Labelable a String => Labelable (GenericBooleanFormulaRegister a) String

Defined in Quipper.Algorithms.BF.BooleanFormula

Methods

label_rec :: GenericBooleanFormulaRegister a -> String -> LabelMonad ()

type QCType x y (GenericBooleanFormulaRegister a)

Defined in Quipper.Algorithms.BF.BooleanFormula

type QCType x y (GenericBooleanFormulaRegister a) = GenericBooleanFormulaRegister (QCType x y a)

type QTypeB (GenericBooleanFormulaRegister a)

Defined in Quipper.Algorithms.BF.BooleanFormula

type QTypeB (GenericBooleanFormulaRegister a) = GenericBooleanFormulaRegister (QTypeB a)

type BooleanFormulaRegister = GenericBooleanFormulaRegister Qubit

A type synonym defined as the Qubit instantiation of a GenericBooleanFormulaRegister.

labelBFR :: BooleanFormulaRegister -> Circ ()

A function to add labels to the wires that make up a BooleanFormulaRegister. These labels correspond to the parts of the register.

type BoolRegister = GenericBooleanFormulaRegister Bool

A type synonym defined as the Bool instantiation of a GenericBooleanFormulaRegister.

toTuple :: GenericBooleanFormulaRegister a -> ((a, a), [[a]], (a, a, a, a, a, a, a), [a])

Helper function to simplify the QCData instance for BooleanFormulaRegister. Create a tuple from a GenericBooleanFormulaRegister.

fromTuple :: ((a, a), [[a]], (a, a, a, a, a, a, a), [a]) -> GenericBooleanFormulaRegister a

Helper function to simplify the QCData instance for BooleanFormulaRegister. Create a GenericBooleanFormulaRegister from a tuple.

createRegister :: BooleanFormulaOracle -> BoolRegister

Create an initial classical BooleanFormulaRegister for a given oracle description. The position register is initialized in the zero state that represents being at label zero, or node rpp in the tree. The work qubits are all initialized to zero, as the first call to the oracle circuit will set them accordingly for the position we are currently in. The direction register is also set to zero as this is the direction in which the node rp is in. The given BooleanFormulaOracle is used to make sure the registers are of the correct size, i.e., number of qubits.

registerShape :: BooleanFormulaOracle -> BooleanFormulaRegister

Create a shape parameter for a BooleanFormulaRegister of the correct size.

initializeRegister :: BooleanFormulaOracle -> Circ BooleanFormulaRegister

Initialize a BooleanFormulaRegister from a BooleanFormulaOracle.

Oracle implementation

The functions in this implementation follow a separation of the boolean formula algorithm into two parts. The first part corresponds to the algorithms defined in this module. The second part consists of the algorithms defined in Quipper.Algorithms.BF.Hex. This separation relates to the first part defining the quantum parts of the algorithm, including the phase estimation, and the quantum walk, whereas the remaining four define the classical implementation of the circuit for determining which player has won a completed game of Hex, which is converted to a quantum circuit using Quipper's "build_circuit" keyword.

Note that the circuits for the algorithms in this module have been tested for performing a quantum walk on the tree defined for a given oracle (but with a dummy function taking the place of the call to HEX).

qw_bf :: BooleanFormulaOracle -> Circ [Bit]

The overall Boolean Formula Algorithm. It initializes the phase estimation register into an equal super-position of all 2^t states, and the other registers as defined previously. It then maps the exponentiated version of the unitary u, as per phase estimation, before applying the inverse QFT, and measuring the result.

subroutine_inverse_qft :: BooleanFormulaOracle -> [Qubit] -> Circ [Qubit]

The inverse quantum Fourier transform as a boxed subroutine.

map_exp_u :: BooleanFormulaOracle -> [Qubit] -> BooleanFormulaRegister -> Int -> Circ ()

"Map" the application of the exponentiated unitary u over the phase estimation register. That is, each qubit in the phase estimation register is used as a control over a call to the unitary u, exponentiated to the appropriate power.

exp_u :: BooleanFormulaOracle -> Integer -> BooleanFormulaRegister -> Circ ()

Exponentiate the unitary u. In this implementation, this is achieved by repeated application of u.

u :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

The unitary u represents a single step in the walk on the NAND tree. A call to the oracle determines what type of node we are at (so we know which directions are valid to step to), the call to diffuse sets the direction register to be a super-position of all valid directions, the call to walk performs the step, and then the call to undo oracle has to clean up the work registers that were set by the call to the oracle. Note that the undo oracle step is not simply the inverse of the oracle, as we have walked since the oracle was called.

subroutine_u :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

The circuit for u as a boxed subroutine.

oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

Call the oracle to determine some extra information about where we are in the tree. Essentially, the special cases are when were are at one of the three "low height" nodes, or when we are at a node representing a complete game of Hex, and we need to determine if this is a leaf, by calling the hex circuit, which determines whether the node represents a completed game of hex in which the red player has won.

subroutine_oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

The circuit for the oracle as a boxed subroutine.

controls :: Qubit -> [DirectionRegister] -> [ControlList]

The controls to use, to see if we're at a "low height" node.

diffuse :: BooleanFormulaRegister -> Circ ()

Diffuse the direction register, to be a super-position of all valid directions from the current node. Note, that this implementation of the boolean formula algorithm does not applying the correct weighting scheme to the NAND graph, which would require this function to diffuse with respect to the weighting scheme.

subroutine_diffuse :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

The circuit for diffuse as a boxed subroutine.

data Where

A datatype to use instead of passing integers to toParent and toChild to define what needs to be shifted. This is used as only three different shift widths are ever used in the algorithm.

Constructors

Width

corresponds to shifting all qubits.

M

corresponds to shifting only m+1 qubits.

M2

corresponds to shifting only 2m+1 qubits.

Instances

Eq Where

Defined in Quipper.Algorithms.BF.BooleanFormula

Methods

(==) :: Where -> Where -> Bool

(/=) :: Where -> Where -> Bool

walk :: BooleanFormulaRegister -> Circ ()

Define a step on the NAND graph, in the direction specified by the direction register, and updates the direction register to be where we have stepped from. For this algorithm we have developed the if_then_elseQ construct, which gives us a nice way of constructing if/else statements acting on boolean statements over qubits (see Quipper.Libraries.QuantumIf).

subroutine_walk :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

The circuit for walk as a boxed subroutine.

undo_oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

Uncompute the various flags that were set by the initial call to the oracle. It has to uncompute the flags depending on where we were before the walk step, so isn't just the inverse of the oracle.

subroutine_undo_oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()

The circuit for undo_oracle as a boxed subroutine.

toParent :: Where -> BooleanFormulaRegister -> Circ ()

Define the circuit that updates the position register to be the parent node of the current position.

copy_from_to :: Qubit -> Qubit -> Circ (Qubit, Qubit)

copy_from_to a b: Sets the state of qubit b to be the state of qubit a, (and the state of a is lost in the process, so this is not cloning). It falls short of swapping a and b, as we're not interested in preserving a.

toChild :: Where -> BooleanFormulaRegister -> Circ ()

Define the circuit that updates the position register to be the child node of the current position.

shift_left :: [DirectionRegister] -> Circ ()

Shift every qubit in a register to the left by one.

shift_right :: [DirectionRegister] -> Circ ()

Shift every qubit in a register to the right by one.

Possible main functions

The following functions define various main functions that can be called from an overall main function to display various parts of the overall Boolean Formula Algorithm. The Boolean Formula Algorithm is split into 13 sub-algorithms, each of which can be displayed separately, or in various combinations.

main_circuit :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Displays the overall Boolean Formula circuit for a given oracle description.

main_u :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display just 1 time-step of the given oracle, i.e., one iteration of the u from exp_u, with no controls.

main_walk :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display just 1 time-step of the walk algorithm for the given oracle, i.e., one iteration of walk, with no controls.

main_diffuse :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display just 1 time-step of the diffuse algorithm for the given oracle, i.e., one iteration of diffuse, with no controls.

main_oracle :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display just 1 time-step of the oracle algorithm for the given oracle, i.e., one iteration of oracle, with no controls.

main_undo_oracle :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display just 1 time-step of the undo_oracle algorithm for the given oracle, i.e., one iteration of undo_oracle, with no controls.

main_hex :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display the circuit for the Hex algorithm, for the given oracle, i.e., one iteration of hex_oracle, with no controls.

main_checkwin_red :: Format -> GateBase -> BooleanFormulaOracle -> IO ()

Display the circuit for the Checkwin_red algorithm, for the given oracle, i.e., one iteration of checkwin_red_circuit, with no controls.

Running the Boolean Formula Algorithm

The following functions define the way that the Boolean Formula Algorithm would be run, if we had access to a quantum computer. Indeed, the functions here interface with the Quipper.Libraries.Simulation.QuantumSimulation quantum simulator so that they can be built.

main_bf :: BooleanFormulaOracle -> IO Bool

Approximation of how the algorithm would be run if we had a quantum computer: uses QuantumSimulation run_generic_io function. The output of the algorithm will be all False only in the instance that the Blue player wins the game.

whoWins :: BooleanFormulaOracle -> IO ()

Display the result of main_bf, i.e., either "Red Wins", or "Blue Wins" is the output.

main_whoWins :: BooleanFormulaOracle -> IO ()

Run whoWins for the given oracle, and its "initial" board.