Stream: Beginner Questions

Topic: Good Style Suggestion for Locales

Ata Keskin (Sep 02 2023 at 16:19):

Hi, in my project I have introduced a lot of locales, which are generalizations of oneanother. Specifically i have the hierarchy:
stochastic_process $\supseteq$ adapted_process $\supseteq$ progressive_process $\supseteq$ predictable_process

For each of these locales, I have two additional "instantiations":
nat_stochastic_process = stochastic_process ........
nat_adapted_process = adapted_process ........
.....
and

real_stochastic_process = stochastic_process ........
real_adapted_process = adapted_process ........

Furthermore, I have two other conditions, one: the underlying filtrations can be sigma finite, two: the codomain of the processes can be ordered banach spaces. Therefore currently I have introduced all possible combinations of locales, ranging from "stochastic_process_order" to "real_sigma_finite_predictable_process_order".

In total, I have around 40-50 locales and 10-20 sublocale relations covering all possible combinations.

Today, I noticed that I also need to consider the case where the measure space is finite, so I need to add at least 40 other locales to cover all possible combinations and also prove all sublocale relations (something like nat_adapted_process $\subseteq$ nat_stochastic_process is not generated automatically).

From a style perspective, would it make more sense to include all possibilities, or should I only introduce the locales that I will actually use, and leave the rest to others (or me in the future) who will (hopefully) use my formalization for their purposes. I only really need sigma_finite_adapted_process, nat_sigma_finite_predictable_process and a couple more for example.

TLDR; Should I introduce locales for all combinations of type classes, or should I only introduce the locales that I will actually use?

Ata Keskin (Sep 02 2023 at 16:53):

I have decided to take the second path and introduce only those locales that I will directly need. I have deleted all other locale statements to avoid clutter. But please provide me with suggestions if you have any experience with (or opinion on) an issue similar to this.

Mathias Fleury (Sep 03 2023 at 10:32):

I think that it mostly depend on your usage.:

1. Make sure to instantiate all locales at least once (it is very stupid to accidentally contradicting assumptions! Happened to me once, but I found out early enough)
2. More locales and more relations actually help catching mistakes…
3. … but you need to maintain and adapt the proofs

Mathias Fleury (Sep 03 2023 at 10:33):

I would say that: don't add too many locales as long as you might still be changing them (aka when you follow a math book, this is not too important) and then, add the ones that feel important, but not everything you can

Last updated: Apr 27 2024 at 16:16 UTC