Revisit how __truediv__ works for QuantTensor

[nickfraser]

__truediv__ in QuantTensor currently does the inverse operation of multiplication, W.R.T. how the output bitwidths, scales are calculated based on the inputs.

For d = a / b, we currently do the following:

d_bitwidth = a_bitwidth - b_bitwidth
d_scale = a_scale / b_scale
d = a / b

This makes sense, when the numerator is the result of the previous multiplication, but perhaps doesn't generalise to a standalone division operation. This also diverges a little bit from what "traditional"* fixed-point arithmetic does. My suggestion is to generalise traditional fixed point arithmetic rules for floating point scales, and to be able to represent the extremes of the input and output range.

A convenient way to do this, would be do decompose division (a / b) into a * (1 / b), and have a simple rule for calculating to output bitwidth of 1 / b, then apply the regular rules to multiplication that we normally do. My suggestion is then as follows:

c = 1 / b
c_bitwidth = b_bitwidth
c_scale = 1 / b_threshold # where b_threshold = b_scale * 2^b_bitwidth (for unsigned) or b_scale * 2^(b_bitwidth-1) (signed)
c_scale = 1 / (b_scale * 2^(b_bitwidth - int(signed))

Adding the multiply, leads to:

d = a / b = a * c = a * (1 / b)
d_bitwidth = a_bitwidth + c_bitwidth = a_bitwidth + b_bitwidth
d_scale = a_scale * c_scale = a_scale / (b_scale * 2^(b_bitwidth - int(signed))

The resulting value would then be:

d = a * QuantInt(1 / b, c_bitwidth, c_scale) # Requantization required to ensure the output QuantTensor contains only valid values, which can be reconverted to integers

I believe this would match traditional fixed point arithmetic rules in the power-of-two case and do something not completely unreasonable in the floating point scaling case. However, the floating point scaling case should be studied further to understand the ramifications of making such a choice. I expect that the decomposition of division into inversion and multiplication is not unreasonable.

*traditional = power-of-two scaling

[nickfraser]

@preusser, I would appreciate feedback on my proposal here.

[preusser]

d = a / b = a * c = a * (1 / b)
d_bitwidth = a_bitwidth + c_bitwidth = a_bitwidth + b_bitwidth
d_scale = a_scale * c_scale = a_scale / (b_scale * 2^(b_bitwidth - int(signed))

In most of the cases, division is a lossy operation. So, I assume the goal would be to preserve the accuracy that can reasonably be expected in the operands?
These proposed bitwidths and scales are reasonable choices. I'd argue that they are even when representing values by a (fixed) floating-point scale (_scale) and a variable integer value (_val):

d = a / b
  = a_scale/b_scale * a_val/b_val
  = (a_scale/b_scale / 2^b_ws) * (a_val * 2^b_ws / b_val)    // b_ws = b_bitwidth - int(signed)
  = d_scale                    * d_val

The scaling performed for the value computation ensures that even the biggest b can fit into the smallest a preserving whatever accuracy a brought into the operation.
However, I would definitely go for this direct implementation rather than taking a detour through 1/b, which would introduce an avoidable accuracy bottleneck.

[nickfraser]

Thanks @preusser, I will adopt your suggestions into the proposal.