On 4 March 2025 11:18:09 GMT-06:00, Martin Baker <ax87...@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.
>
>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/ED5B6F9C-E69D-4AB4-BE3C-5CDFC67B02DA%40gmail.com.
