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
On 04/03/2025 14:06, Waldek Hebisch wrote:
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.
--
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/bd16456c-cd56-400c-a490-688a2f5d0a73%40martinb.com.
