Re: P1788/D9.2 draft (10.5.5)
Frederic,
The relations X/Y = Z and X = ZY are not exactly equivalent.
The tuple (x=0, y=0, z=1) belongs to the second relation,
but it doesn't belong to the first relation.
Also it seems to me that
pow(X,Y,Z) == hull({z\in Z\mid \exists x\in X, \exists y\in Y: x^y = z})
powRev(Z,X,Y) == hull({x\in X\mid\exists y\in Y, \exists z\in Z: x^y = z})
powRev(Z,Y,X) == hull({y\in Y\mid\exists x\in X, \exists z\in Z: x^y = z})
are three different operations (in contrast to mul).
Please, explain if I miss something.
-Dima
----- Original Message -----
From: Frederic.Goualard@xxxxxxxxxxxxxx
To: mhack@xxxxxxx, stds-1788@xxxxxxxxxxxxxxxxx
Sent: Friday, May 16, 2014 9:15:31 PM GMT +04:00 Abu Dhabi / Muscat
Subject: Re: P1788/D9.2 draft (10.5.5)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Dear Michel,
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.
Best regards,
F.
- --
Frédéric Goualard LINA - UMR CNRS 6241
Tel.: +33 2 76 64 50 12 Univ. of Nantes - Ecole des Mines de Nantes
2, rue de la Houssinière - BP 92208
http://frederic.goualard.net/ F-44322 NANTES CEDEX 3
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.14 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
iQEcBAEBAgAGBQJTdkeKAAoJEIyjRWvAvCeCF/8IAJGbDI1+dGg4U7k6yBYx8FTm
ql0DbAIrp2prpLm5TsQofWhZT0b/lqMv2+dnfgmKA4MgkzniZKR/HaYleKrvH2tf
/ZH3SxWLbZEr+q85+daYxafgLPXZpMz28rT0aJtupcxw+lZulaIWt/gjYjJxcqPQ
oMh3PNQzCxLIniLvY2qQ9bVd6j9kXyJNgHk5quTWd1P11Un628cu9Uqt0lVlkrpc
QmZu2qMoxnZD1vxU2F4lOKYobKXnN/Ef0R6mrnl1pv8OGbDYHQe8PlBEmFMowOaf
msB+X5xTE/l5/9T8l4/cw6gC2P2DK95TpfrcgAhKOtA47zu6qeRR2EEwt/rCkto=
=8hGk
-----END PGP SIGNATURE-----