James Hanson (Feb 02 2024 at 22:14): James Hanson (Feb 02 2024 at 22:14):I'm trying to learn some basics of Isabelle/HOL. My understanding is that the typical way of dealing with algebraic objects is with locales. Is it possible to work with infinite families of objects in such a framework? For instance, say I wanted to take the direct product of an infinite family of groups. Can this be done?
Christian Pardillo Laursen (Feb 04 2024 at 15:42):Infinite families are modelled as functions in Isabelle/HOL. As far as I know, group theory in Isabelle is done using typeclasses and combining those is trickier, but if we have some set G whose elements are groups then an infinite family of groups would be a function "I => G", and the semidirect product would be a function (I => G) => G. Have a look at HOL/Analysis/Finite_Product_Measure and Infinite_Product_Measure for a (rather involved) example of how this is done in measure theory.
James Hanson (Feb 04 2024 at 17:01):Thanks. I looked at Paulson's blog post about type classes vs. locales, but I still don't feel like I understand the practicalities of when to use one or the other.
Christian Pardillo Laursen (Feb 05 2024 at 00:53):Typeclasses are locales tied to types, and so work best when the concept you are trying to define has one correct interpretation for any given type. Locales are more flexible, and generally if you want to reason about carrier sets directly or need compositionality they will let you do a lot more, but without the automation that typeclasses bring.
Manuel Eberl (Feb 09 2024 at 11:23):As soon as you want to do proper abstract algebra you need to move away from type classes. Reasoning about e.g. subclasses is usually not possible with type classes. The canonical library for doing abstract algebra in Isabelle/HOL is HOL-Algebra. It's usable, albeit not in the best state I would say.
Manuel Eberl (Feb 09 2024 at 11:25):A student of mine formalised direct products of groups in the AFP a few years ago:
https://www.isa-afp.org/sessions/finitely_generated_abelian_groups/#IDirProds.html#IDirProds.IDirProds|const
https://www.isa-afp.org/sessions/finitely_generated_abelian_groups/#DirProds.html#DirProds.DirProds|const
Manuel Eberl (Feb 09 2024 at 11:25):This uses HOL-Algebra. If you have any questions about this, feel free to ask me.
James Hanson (Feb 09 2024 at 16:19):@Manuel Eberl As I mentioned in another question, I'd like to try to formalize some results about Henkin-Monk-Tarski cylindric algebras both as practice and because I think it might be a decent approach to eventually formalizing some intermediate model theory. Basically my uniformed guess is that Isabelle's automation is going to be a little bit better at handling abstract algebra than formulas defined in terms of syntax directly.
What would you recommend as the right way to structure that definition? Cylindric algebras are Boolean algebras with extra operators, but they typically have an infinite language (with infinitely many cylindrification operators). Ideally one might want to allow this to vary, but it should also be possible to get away with only having cylindrifications indexed by the natural numbers.
HOL-Algebra doesn't seem to have Boolean algebras. Would it make sense to try to formalize them in terms of Boolean rings?
Manuel Eberl (Feb 16 2024 at 11:32):Hm, that's hard to say.
Manuel Eberl (Feb 16 2024 at 11:33):My guess would be that you don't need a lot of ring theory when reasoning about Boolean algebras.
Manuel Eberl (Feb 16 2024 at 11:33):So it might make sense to just do it from scratch.
Manuel Eberl (Feb 16 2024 at 11:33):Maybe also without records. In HOL-Algebra, a ring is a record with a locale containing the ring axioms as assumptions.
Manuel Eberl (Feb 16 2024 at 11:35):Ballarin's approach does use locales but not records, which has some advantages. The main disadvantage is that there isn't an easy way to talk about a ring as a single object (i.e. a function that returns a ring). But if you don't need that then Ballarin's approach is probably nicer.
Manuel Eberl (Feb 16 2024 at 11:36):I.e. a locale that fixes a carrier set and operators 0, 1, +, *, ~ and then assumes that they all behave properly.
Manuel Eberl (Feb 16 2024 at 11:37):Note however that there is already some material on Boolean algebras in the AFP.
James Hanson (Feb 17 2024 at 20:09):@Manuel Eberl I realized that I'm not really understanding the role of schemes in the use of records. In the definition of the direct product of groups why is the output given as a monoid rather than a monoid_scheme?
definition DirProds :: "('a ⇒ ('b, 'c) monoid_scheme) ⇒ 'a set ⇒ ('a ⇒ 'b) monoid" where
"DirProds G I = ⦇ carrier = Pi⇩E I (carrier ∘ G),
monoid.mult = (λx y. restrict (λi. x i ⊗⇘G i⇙ y i) I),
one = restrict (λi. 𝟭⇘G i⇙) I ⦈"
Oh I think I understand now. The whole point of _schemes is that they're what allow methods of records to be inherited by extension. The reason that DirProds goes from a family of monoid_schemes to a monoid is that a record extending monoid could include arbitrary data that we don't know how to sensibly interpret in the direct product.
Am I understanding this correctly?
Manuel Eberl (Feb 20 2024 at 11:53):Yes, the scheme is just an artefact of how records inheritance work in Isabelle.
Manuel Eberl (Feb 20 2024 at 11:54):In particular you can use a ring as a group and a group as a monoid without having to do any sort of conversion (you then get the multiplicative group).
Manuel Eberl (Feb 20 2024 at 11:54):And it has nothing to do with the algebraic structure known as "scheme".
Last updated: Dec 21 2024 at 16:20 UTC