[Agda] algebra hierarchy in library

Matthew Daggitt matthewdaggitt at gmail.com
Sat Mar 16 11:16:03 CET 2019


Hi Sergei,

(I wonder, why people, - and standard library, - call provers solvers).
>

Unsure.

If this is the only reason, then it occurs that `Is' structure is needed
> only in few cases.
>

I think your examples miss the point. For example take any binary operator.
That binary operator may form many different Semigroups/Monoids/Groups etc.
depending on what the underlying equality is. The `Is` structures allow you
to expose which equality you're using at a particular point, whereas your
suggestion would hide it.

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

As I mentioned to you in an issue on Github, non-backwards compatible
changes will only be considered where either i) the implementation is
incorrect (clearly not the case here) or ii) there's a compelling reason
why the current version isn't good enough. "Looking more natural"
unfortunately isn't such a reason and as mentioned above Version II doesn't
allow you to expose the underlying equality.
Best,
Matthew

On Sat, Mar 9, 2019 at 6:28 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> 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
> > >
> > >
> > >
> >
> >
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190316/b7208579/attachment.html>


More information about the Agda mailing list