[Agda] algebra hierarchy in library

Sergei Meshveliani mechvel at botik.ru
Sat Mar 9 15:08:16 CET 2019


On Sat, 2019-03-09 at 14:35 +0300, Sergei Meshveliani wrote:

> 
> 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.
[..]


Sorry for a silly error. I discover a mistake in (2), (4) (6).

For example,  Nat1 = Nat\0  is a semigroup by _+_,  and zero can be
joined in different ways, so that (Nat1 U 0) and (Nat1 U 0') occur
different monoids. They are isomorphic, but they have different
carriers. 
A similar effect with carrier may be in (4) and (6).

So that there remain (1), (3) and (7).


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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda




More information about the Agda mailing list