[Agda] algebra hierarchy in library
Sergei Meshveliani
mechvel at botik.ru
Sat Mar 9 12:35:52 CET 2019
On Fri, 2019-03-08 at 22:09 +0000, Matthew Daggitt wrote:
> 1. Why `Raw' structures?
>
>
> Sometimes you only need the raw operators without assuming any
> properties over them. See for example the coefficient ring for
> the ring solver. You could of course change this to require the full
> ring axioms but this is a) more work for the user and b) unnecessary.
> The raw versions aren't widely used but they don't affect the
> hierarchy in anyway so there's no harm in having them.
>
Yes, it looks like they can be useful for solvers
(I wonder, why people, - and standard library, - call provers solvers).
> 2. Why putting `Is' structures into a different file?
>
>
>
> This was an inherited design decision. I know it differs from the way
> the library is laid out in `Relation.Binary`. The advantage of having
> them separately is that the module can be parameterised by the
> equality. See `Data.Nat.Properties` for a use of this. I agree it's a
> little irritating having to open both `Algebra` and
> `Algebra.Structures`. It may be that `Algebra` should re-export
> `Algebra.Structures`. I'm unsure of how to standardise this with
> `Relation.Binary`.
>
This re-export looks desirable.
>
> 3. Why Magma declares the fields Carrier and _≈_ by new?
>
>
>
> You've answered your own question here with your magma product
> example. It's exactly as you describe.
If this is the only reason, then it occurs that `Is' structure is needed
only in few cases.
For example,
(1) There does not exist different semigroups that inherit ("are over")
the same Magma. The difference can be in a _proof_ for associativity,
but I doubt of whether this feature can be taken here in account.
Let people correct me if I mistake in the following statements.
(2) There does not exist different monoids over the same Semigroup.
(3) There does not exist different commutative monoids over the same
Monoid.
(4) There does not exist different groups over the same Monoid.
(5) There does not exist different Abelian groups over the same Group.
(6) There does not exist different rings over the same Semiring.
(7) There does not exist different commutative rings over the same
Ring.
Here are the two proofs sketches.
(2) If a semigroup H is extended to monoids with unities e and e', then
e * e' == e == e' by the two unity laws ...
(4) If a monoid is extended to two groups with inversion operations i
and i', then it holds
i x == (i x) * e == (i x) * (x * (i' x)) ==
((i x) * x) * (i' x) == e * (i' x) == i' x.
Am I missing something?
`Is' structures are needed for the cases of the steps of
Setoid -- Poset, Setoid -- Magma, CommutativeMonoid -- Semiring.
It may be also Ring -- LeftModule (over a ring), if such is added to
standard.
> If you have two structures of the type `IsX` and you want to combine
> them, you can specify exactly how the parameters of the two interact
> to form the 3rd `IsX` type. This wouldn't be possible (or much harder
> anyway) using Version II. Version I requires a little more boiler
> plate code (written by the library maintainers) but it makes the
> hierarchy much easier to use in practice (on the user end).
>
Version II looks more natural to me. But I may be missing something.
To make sure, I could rewrite a part of the library for Version II and
demonstrate. And what if it occurs better? It will be late to consider
for standard.
Regards,
------
Sergei
>
> On Fri, Mar 8, 2019 at 3:00 PM Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>
> Dear standard library developers and supporters,
>
> can you please answer in (simple words) several questions
> about the
> representation of the algebraic hierarchy in standard library?
>
>
> 1. Why `Raw' structures?
>
> There are classical generic algebraic structures (call them
> GAS):
> Magma, Semigroup, Monoid, and so on.
>
> Those of them having some new field respectively to previous
> structures
> are accompanied with the corresponding `Raw' record. For
> example, Magma
> is preceded with RawMagma, Monoid with RawMonoid. Each `Raw'
> structure
> expresses only the signature of the corresponding GAS.
>
> What the `Raw' structures serve for?
>
>
> 2. Why putting `Is' structures into a different file?
>
> For example, the reader looks into Algebra.agda to find what
> is
> Semigroup:
>
> -------------------------------------------------------
> record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
> ...
> field Carrier : Set c
> _≈_ : Rel Carrier ℓ
> _∙_ : Op₂ Carrier
> isSemigroup : IsSemigroup _≈_ _∙_
>
> open IsSemigroup isSemigroup public
> ...
> magma = record { isMagma = isMagma }
> ...
>
> Now, one needs to find a declaration for IsSemigroup.
> And it resides in a different file of
> Algebra/Structures.agda :
>
> record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
> field
> isMagma : IsMagma ∙
> assoc : Associative ∙
>
> open IsMagma isMagma public
> ---------------------------------------------------------
>
> And all this implements the meaning of a small sentence:
> ``Semigroup is Magma in which multiplication _∙_ is
> associative''.
>
> Why not put ``record IsSemigroup'' before ``record Semigroup''
> in the
> same file Algebra.agda ?
>
> Similarly other `Is' GAS decls can join. So that Algebra.agda
> and
> Algebra/Structures.agda will merge into Algebra.agda in
> which each
> GAS will be defined in one place.
> For example, to see what is a group will need to look into one
> file, not
> in two files.
> ?
>
>
> 3. Why Magma declares the fields Carrier and _≈_ by new?
>
> Similarly, why other GAS re-declare many fields?
>
> In theory, we have
> ``Magma is a setoid with an operation _∙_ congruent with
> respect to the
> equality _≈_''.
>
> So, Magma inherits Setoid. And it is natural for its
> representation in
> Agda to have setoid somewhere inside it. So, it opens this
> setoid and
> uses its fields in further definitions. For example, like
> this:
>
> -- Version II
> ---------------------------------------------------------
>
> record IsMagma {α α=} (S : Setoid α α=) (_∙_ : Op₂
> (Setoid.Carrier S)) :
> Set
> (α ⊔ α=)
> where
> open Setoid S using (_≈_; Carrier)
> field
> ∙cong : _∙_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
>
> record Magma α α= : Set (suc (α ⊔ α=))
> where
> field setoid : Setoid α α=
>
> open Setoid setoid public
> infixl 7 _∙_
>
> field _∙_ : Op₂ Carrier
> isMagma : IsMagma setoid _∙_
> ------------------------------------------------------------------------
>
> And let us call Version I the approach of Standard library
> lib-0.17.
>
> Both versions use an `Is' structure, but II does not
> re-declare fields.
> Is not II more natural?
>
>
> Another question may be:
> ``why splitting each GAS into proper structure and `Is'
> structure?''.
>
> My guess is that this approach allows us to express two GAS-s
> that are
> over the same inherited GAS. For example, a programmer can
> express a
> product of two Magmae over the same Setoid:
> ------------------------------------------------------------
> module _ {α α=} (S : Setoid α α=)
> where
> open Setoid S using (Carrier; _≈_)
> SS = ×-setoid S S
> open Setoid SS using () renaming (Carrier to CC; _≈_ to
> _=p_)
>
> magmaProduct' :
> (_*₁_ _*₂_ : Op₂ Carrier) → IsMagma _≈_ _*₁_ →
> IsMagma _≈_ _*₂_ → Magma α α=
> magmaProduct' _*₁_ _*₂_ insM₁ isM₂ =
> <define coordinate-wise multiplcation
> on CC;
> prove ...; return the Magma record
> >
> ------------------------------------------------------------
>
> (is there any other purpose to introduce `Is' -structures?).
>
> This is equally easy to set both in Version I and Version II.
>
> But note that both approaches still deviate, a bit, from the
> theory.
> Because in theory, it is
> \ (mg1 : Magma_ _) (mg2 : Magma _ _) (HaveCommonSetoid mg1
> mg2) →
> product-magma,
> while magmaProduct' takes certain parts of the two magmae.
>
> So, there remain somewhat three and a half questions.
>
> Thank you in advance for your possible explanation.
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list