interval arithmetic

[Ralf Hemmecke]

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.

Discussion open.

Ralf

[Waldek Hebisch]

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

[Martin Baker]

Is there any link from this topic to the topological spaces over finite
sets that I am looking at? Especially homotopy theory.

In programs that implement cubical type theory (CTT) the interval [0,1]
has to be specially built into the type system, it behaves like a type
in some ways but technically it is not a type. For instance, you can
have maps out of the interval but not maps into it.

For instance see:
https://arend-lang.github.io/documentation/tutorial/PartII/hits
See the section 'Types as spaces'.

Martin

[Dima Pasechnik]

On 4 March 2025 11:18:09 GMT-06:00, Martin Baker <ax8...@martinb.com> wrote:
>Is there any link from this topic to the topological spaces over finite
>sets that I am looking at? Especially homotopy theory.

There is no direct link, no more than, say, a link from the topic of machine-precision floating point computations and associated to it types. (it's well-known that floating point numbers don't
satisfy the axioms of a field, just like it is for interval numbers). Not much to do with type theory here, it's just basic numerical analysis.