Re: P1788/D9.2 draft (10.5.5)
Frédéric
On 16 May 2014, at 18:14, Frédéric Goualard wrote:
> On 16/05/2014 16:42, Michel Hack wrote:
>>> that the mulRev1/mulRev2 and powRev1/powRev2 dichotomy is not
>>> present.
>>
>> There is only one mulRev, but there are divRev1 and divRev2. We
>> also need powRev1 and powRev2 because the pow(x,y) function is not
>> commutative.
>>
>> You would use divRev1 to narrow X in the relation X/Y = Z and
>> divRev2 to narrow Y.
>>
>> At least that's MY understanding.
>
> That is precisely my point. The *relation*
>
> X/Y = Z
>
> can be rewritten equivalently as
>
> X = ZY
>
> and then we are back to what I said in my previous mail.
I also wondered about this but it's not my area so I didn't say anything. AFAICS this comes from Arnold Neumaier's Vienna Proposal where §3.10 says
> 3.10. Table: Binary arithmetic operations
>
> Notation is as in Section 3.8.
> plus x+y tightest
> minus x-y tightest
> times x*y tightest reverse
> divide x/y tightest reverse
> min min(x,y) tightest
> max max(x,y) tightest
> pow x^y (see 3.12) accurate reverse
> atan2 atan2(x,y) accurate reverse
Since Arnold had done a lot of work in constraint satisfaction, I reckoned that reverse forms of "divide" & "pow" must be useful. If you convince us this is not the case, I'll be very happy to simplify things by removing them.
Jürgen, you have traditionally been our operations tsar. What do you think?
John