AngleOp::adiv is ambiguous

[cqc-alec]

Angles are equivalence classes mod 2π; but division by an integer (in contrast to multiplication by an integer) is not invariant under that equivalence: e.g. 0 ≡ 2π but 0/2 ≢ (2π)/2.

I would rather like to get rid of this operation for this reason, but if we do keep it we should specify the semantics, probably by coercing the initial argument to be in [0, 2π) or [-π, π). (Note that if we chose [0, 2π) then dividing e.g. the angle -π/2 by 2 would give us 3π/4, which may be unexpected.)

[doug-q]

I agree we should remove for this reason.

The "law" adiv(afromrads(x),y) =~= afromrads(fdiv(x,y)) (where =~= means approximately equal) does not hold.

Also, adiv should return an option type for the case where the divisor is 0. I am not creating an issue for this on the assumption that the op will be removed.

[jake-arkinstall]

Possibly too picky but...

Angles are equivalence classes mod 2π

Not if you're a spin-1/2 fermion, a mobius strip, or a (2+1)D manifold with holes!

Ok, silly examples for this, but there's a more pressing one. The R gate (a.k.a. phased x) is defined as:

R(θ, ϕ) = (         cos(θ/2)              -i exp(-iϕ) sin(θ/2)  )
          (  -i exp(iϕ) sin(θ/2)                cos(θ/2)        )

In this case, R(π/2 + 2π, π) = -R(π/2, π). In this case, R is 4π periodic in θ, not 2π. It differs by a global phase at 2π, which might be something that one can ignore, but might not, depending on the scenario.

There are possibly some more useful examples, but this is the first one that springs to mind.

division by an integer (in contrast to multiplication by an integer) is not invariant under that equivalence

I think windings could be taken into account through a fixed point angle that doesn't have the 'point' before the MSB, but somewhere in the middle.

For example, if we have 64 bits of angle, the first byte could be an integer component:

00000010 (.) 10000000 00000000 .... => 2.5

This leaves us with up to 255 'windings' (that may be considered moot or not, depending on the scenario) and still allows the angle component to be represented to one part in 72 quadrillion. A finer balance may be struck, e.g. 16 bits of winding and 40 bits of angle.

However, one might argue that the intent of a division depends on the situation - and in this case we might want a 'pure' angle and a 'wound' (?) angle type, each with a well defined division. Would that be too confusing for users?

[cqc-alec]

Yes, in pytket we consider angle parameters to be defined mod 2π for some ops and mod 4π for others. The difference this makes is at most a global phase. But in all cases where it is 4π (such as your R example), it could (arguably should) equally have been defined in terms of a mod-2π angle (by halving/doubling the parameters in the definition). Alternatively there could be separate types (mod-2π angles and mod-4π angles) but I think that's overkill.

I think in the rare cases where it really matters, winding number and angle can be stored as separate variables (integer, angle) in the user's program, and we don't need a core type for this.

[doug-q]

Here is a use of adiv: https://github.com/CQCL/guppylang/blob/36c76e05185f027df6d6a38ce2e5806e38b9031c/examples/random_walk_qpe.py#L69

[cqc-alec]

Here is a use of adiv: https://github.com/CQCL/guppylang/blob/36c76e05185f027df6d6a38ce2e5806e38b9031c/examples/random_walk_qpe.py#L69

This particular one could easily be rewritten as

    a = angle(-0.25 * t)
    q2 = rz(q2, a)
    q1, q2 = cx(q1, q2)
    q2 = rz(q2, -a)
    return cx(q1, q2)

[acl-cqc]

Agree adiv should be removed. Integers modulo a prime $p$, there is a unique result of every division ($0\leq{}x\lt{}p$). This is simply not true of floats, there are multiple answers less than the modulus/within the range.

Storing the windings basically means, angles are no longer identified modulo 2pi. At that point it's a different choice of precision (/when does truncation happen), etc. Not saying whether it might be better or worse than float / nondyadic rational, but it's in the same space, so one should compare those different "number types" just in terms of when truncation happens, etc.