Ancilla use in dagger context

[GBoydQ]

Assignment, being non-reversible, is not supported in a dagger context. However given how this will impact the use of ancilla in programs I thought it was worth making a discussion about two main approaches to using ancilla given that this will determine how guppy-algorithms moves forwards.

The first is that this is just managed at the program level, so unitaries never allocate and always take in ancilla that are assumed to be in $\ket{0}$, and leave them back in the $\ket{0}$ state.

Another option is that alternative/argument for discard is added which acts as a promise to the compiler that the discarded qubits are in $\ket{0}$

For example, the following function should not compile as the final ancilla state is unknown.

@guppy(dagger=True)
def foo(q: array[qubit,n])->None:
    a = qubit()
    # unitary body
    discard(a)

but when replacing discard(a) with "discard(a, zero=True)" (which the compiler of course cannot verify is the case) it is now at least in theory possible to tell that this is reversible, (although I do not know how hard matching up allocations and deallocations will be in general).

I would be interested to hear any thoughts on this, apologies if it has already been discussed elsewhere.

[ss2165]

how hard matching up allocations and deallocations will be in general

Not generally possible - imagine a program that swaps two qubits depending on a measurement. In theory the compiler could fail only when such a proof isn't possible and accept the dagger otherwise.

[GBoydQ]

True, but perhaps I should clarify that by 'in general' I mean working under the assumptions on foo above, where the function would have been daggerable if the ancilla were inout arguments (so must either not include measurements, or only have them because someone has overloaded a dagger so that it does contain measurements)

[ss2165]

Yes under these conditions it should be possible. Does it need to be "discard zero" or is "discard separable" sufficient?

[GBoydQ]

I think the state has to be known for the qubit to be initialised properly when daggering.
You also run into a similar problem when controlling, where ancilla not returned to their initial state will result in some spurious entangement.