[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