Stream: Hierarchy Builder devs & users

Topic: demo2

Marie Kerjean (Mar 22 2021 at 15:53):

In the demo2 file, what does Uniform_TAddAG_unjoined here means ? Is it the translation of a mc-analysis line I could look at ?

Enrico Tassi (Mar 22 2021 at 16:09):

There is a property which is nice to have (and sometimes required? @Cyril Cohen ) that is that for any set of mixins there is a structure defined by that set. I think the structure you point to has no interest per se (mathematically speaking), but is the only one with that set of mixins (and no more).

Cyril Cohen (Mar 22 2021 at 16:13):

Marie Kerjean said:

In the demo2 file, what does Uniform_TAddAG_unjoined here means ? Is it the translation of a mc-analysis line I could look at ?

No it's the translation of nothing we have so far in mc analysis, it would be too time/space/understanding costly to implement it by hand... This is an example on how to deal with the interpendency between topological space, uniform space and topological group, indeed, uniform spaces form a substructure of topological spaces, but when the topological space happens to be a (topological) group, then it is a uniform space. The problem that demo2 solves is how to do that, while still preserving forgetful inheritance...

Enrico Tassi (Mar 22 2021 at 16:15):

Is my reply off topic then? (just to clarify the thread)

Cyril Cohen (Mar 22 2021 at 16:17):

The reason why (as @Enrico Tassi said) it is usually a good idea to define intermediate structures which should not be used by the end user (because indeed they have no interest mathematically speaking) is to make sure that joins are unique, i.e. for any pairs of structures in the hierarchy, they have at most one sub-structure in common, otherwise, there is no unification rule we can give to coq that will solve all the constraints that must be solvable in practice.

Cyril Cohen (Mar 22 2021 at 16:19):

Since I look closer to the structure you point out @Marie Kerjean I am wondering if it is actually necessary to create it in this case... Maybe we could skip it.

Last updated: Apr 18 2024 at 04:02 UTC