On Tue, Mar 04, 2025 at 11:37:16AM +0100, 'Ralf Hemmecke' via FriCAS - computer
algebra system wrote:
> Maybe I do not know much about interval arithmetic, but Interval
> https://fricas.github.io/api/Interval.html
> claims to be a Ring and so should fulfil the ring axioms.
>
>
> %%% (1) -> ii:=interval(-2.0,7.0)$Interval(Float)
>
> (1) [- 2.0, 7.0]
> Type: Interval(Float)
> %%% (2) -> ii*ii*ii
>
> (2) [- 98.0000000000_00000003, 343.0000000000_0000001]
> Type: Interval(Float)
> %%% (3) -> ii^3
>
> (3) [- 8.0000000000_000000002, 343.0000000000_0000001]
> Type: Interval(Float)
>
> Of course,
>
> %%% (5) -> ii^2
>
> (5) [0.0, 49.0000000000_00000001]
> Type: Interval(Float)
>
> makes sense in terms of interval arithmetic, but we shouldn't export
> GcdDomain. I have nothing against exporting functions with the same name (^
> in this case), but they shouldn't come in the context of being inherited
> from Ring if they do not fulfil the axioms.
Yes, Interval violates ring axioms.
Trouble is that exports perform double duty. We want to be able
to pass intervals to functions accepting rings. IIRC I tried to
trim unsound exports, but in case of Interval it would break
some things.
In the long run more exports should be conditional. And we need
better proving machinery. Part of proving is inside Spad compiler
and we should improve it. At some moment in the future we
probably should get external proving tool. Simply, many
needed reasonings are too complicated to do as part of type
checking. One possible approach could be to have analog of
'pretend', that would assert certain things. Some assertions
can be checked at runtime. But there is also possibility of
trusting validity od assertions at compile time, but having
separate proof checker to prove that they are always valid.
Anyway, having full soundness and proofs is future dream.
--
Waldek Hebisch
--
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 fricas-devel+unsubscr...@googlegroups.com.
To view this discussion visit
https://groups.google.com/d/msgid/fricas-devel/Z8cI7OGDIDgYFREo%40fricas.org.
