Quantum redefinition through quantum control behaviour inconsistent depending on scope

[marco-lewis]

TL;DR: Cannot redefine quantum variable under quantum control in a subroutine, but the quantum variable under quantum control can be redefined in the environment/scope it is defined in

Whilst I have a more complex scenario, the behaviour also occurs in this simple example. Here is a program that takes a variable (q) and based on quantum control, changes the value:

n := 3;

def main(){
    q := 1 :uint[n];
    p := H(0:B);
    if p {
        q = 3:uint[n];
    }
    measure(p);
    return q;
}

This is accepted in Silq and runs as expected (before measurement the state is 1/sqrt(2) * (|1>|0> + |3>|1>)). This is helpful for generating oracles as you can just tell Silq what value you want the variable to take based on classical variables and there is no need to explicitly define all the operations that need to take place for the new value.

In one of my programs, I want to avoid code duplication and would like to put the if statement into a function and replace the if statement in main with q := func(p, q). However, an error occurs when doing so:

def func(const p:B, q:uint[n]){
    if p {
        q = 3:uint[n];  // Error: cannot reassign quantum variable
    }
    return q;
}

I do not think this error should occur.

[tgehr]

An assignment q = expr; is essentially syntax sugar for:

forget(q);
q := expr;

Here, forget has to automatically synthesize an uncomputation for q. This is possible in main because the value of q is known. However, it is impossible in func. It may even be the case that there is not any way to uncompute the parameter q.

However, your use case is of course a reasonable thing to want to do.

The underlying issue is that there is information that is tracked by the type system that currently does not have syntax to cross function boundaries. We should therefore add some additional annotations, e.g.:

def func(const p:𝔹, forgettable q:uint[n]){
    if p {
        q = 3:uint[n];
    }
    return q;
}
n := 3;

def main(){
    q := 1 :uint[n];
    p := H(0:𝔹);
    q := func(p,q); // checks that q can be uncomputed
    measure(p);
    return q;
}

Ideally, this should be able to pass around all information that is currently tracked by the type checker so that Silq programs regain full modularity.

[marco-lewis]

Thanks for the information around this. I was thinking shortly after I posted and I think you are right that the issue is that q is known in main, but not in func. This would be a good enhancement to add considering that Silq code wants to be concise.