[Agda] algebra hierarchy in library
Sergei Meshveliani
mechvel at botik.ru
Sat Mar 9 19:28:07 CET 2019
On Sat, 2019-03-09 at 19:08 +0300, Sergei Meshveliani wrote:
> On Sat, 2019-03-09 at 17:08 +0300, Sergei Meshveliani wrote:
> > 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).
>
>
> No, again an error.
>
> A monoid in _this library_ is on the same carrier C as its inherited
> semigroup. So that to implement a monoid on a given semigroup means to
> choose any e in C which satisfy the law \forall x (e*x == x*e == x)
> and to prove this law.
> And it is proved above that such e is unique.
>
> So, I think that similarly, all the points (1) -- (7) are true
> -- if I am not missing something.
We need one more step towards truth :-)
Having a Monoid instance, how many different group instances can be
defined on this monoid (hence, on the same carrier C) ? Possible
inversion map on C is unique, as shown in one of previous letters. But
it can be implemented by different algorithms, and this can be used by
programmers. Algorithms matter in the library. And according to Agda,
different algorithms for inversion give different groups.
So that there remain the above statements (1), (3), (7), and may be (2).
--
SM
>
>
> > >
> > > >
> > > > 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