On 06/30/2014 01:35 PM, Waldek Hebisch wrote: > Ralf Hemmecke wrote: >> >> On 06/30/2014 04:05 AM, Waldek Hebisch wrote: >>> The following look very fishy: >>> >>> (13) -> i1 := interval(1,2)$Interval(Float) + interval(1,2)$Interval(Float) >>> >>> (13) [2.0,4.0000000000_000000001] >>> Type: >>> Interval(Float) >>> (14) -> i1 - interval(1,2)$Interval(Float) - interval(1,2)$Interval(Float) >>> >>> (14) [- 2.0000000000_000000001,2.0000000000_000000001] >>> Type: >>> Interval(Float) >>> (15) -> i1 - (interval(1,2)$Interval(Float) + interval(1,2)$Interval(Float)) >>> >>> (15) [0.0,0.0] >>> Type: >>> Interval(Float) >> >> Why? Float is not holding exact values, so how would the system know >> whether (when it sees) 2.0000 is not actually coming from 2.00004? (For >> simplicity I've reduced the precision to precision(18).) > > The point is that difference between (14) and (15) is way beyond > rounding error. In any ring 'a - (b + b)' and 'a - b -b' should > give the same result.
Yes, I understand. Another reason, why https://github.com/fricas/fricas/blob/master/src/algebra/interval.spad#L14 i.e. the export of "Ring" is wrong for domain Interval. > Well, Float is red herring here: the same problem would be present > if we allowed intervals with exact ends. In fact, I was not so much putting emphasis on Float (in fact, I thought you were concentrating on why we see 4.0000000000_000000001 instead of 4.0. You never mentioned the distribution law in your first mail. Anyway, neither Float nor Interval(R) should export Ring, because they do not meet the ring laws. Of course, we could still allow them to be Ring, but then our Ring category and the mathematical definition of ring do not match and just lead to confusion. Also Float: Join(Ring, Approximate) would not be an option for me, since it would still lead to Float has Ring resulting in "true" with all the bad consequences. > Coming back to Float: operation there are associative up > to rounding error. So, if you are prepared to ignore > rounding error (which typically is small), then usual > ring idetities work OK. But for intervals error are > not small... So? Then export something like ApproximateRing, but not Ring. But ApproximateRing is rather as useless as is our attribute Approximate, since the documentation is rather vague and doesn't clearly convey the semantics behind. >> The algebra library in Aldor solves that problem in a way that I find >> much more mathematically correct. It introduces AdditiveType. > Yes, that is possible direction. Concerning implementation, I > think it is quite doable. For me main problem is potential > loss of expressivness. Namely, currently various opertions > are applied only to types that have apropriate mathematical > properties. Decoupling math properties and signatures we > would be forced to perform operations in cases where only > signatures are available. Wait a minute. AdditiveType and Co represent an idea for me. I'm not saying that is perfect. Look at this. https://github.com/pippijn/aldor/blob/master/aldor/lib/aldor/src/arith/sal_arith.as#L46 \Signatures{ $-$: & \% $\to$ \%\\ $+,-$: & (\%, \%) $\to$ \%\\ } \Params{ {\em x,y} & \% & elements of the type\\ } \Retval{$x + y, x - y$ return respectively the sum and difference $x$ with $y$, while $-x$ returns the opposite of $x$.} It doesn't say anything about the connection of + and -. It's not even clear whether (x+(-y)) = x-y. Or whether -(-x)=x. It's really just exporting the signatures. Unfortunately, we cannot (yet) express in SPAD the respective mathematical laws. But what we can do is what we already do with the category CommutativeStar. We can introduce a category for every law that we find relevant. Yes, that may seem tedious, but it would make it clear what the exact properties of the various operations are. So we might have a category UnaryMinus: Category == with -: % -> % ++ -x returns the opposite of x with the property that -(-x)=x. Plus: Category == with +: (%, %) -> % ++ x+y returns the sum of x and y. +++ If a domain exports AssociateivePlus, it means that for all any +++ elements x,y,z it holds (x+y)+z=x+(y+z). AssociativePlus: Category == Plus etc. etc. > In other words alternatives are: > > - have strict applicability conditions, but lie from > time to time > - tell truth always, but have loose applicability conditions Lying is not an option for me. Ralf -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
