ProblemInProgramAlgebra.tex

\chapter{Problem In Programming Algebra}
Algebraic structures show variations in syntax and semantics depending on the
system or language in which they are defined. Each system discussed in Chapter 3
have their own style of defining structures in the standard libraries. For
example, in Idris, the ring is defined without a multiplicative identity
(\MYhref{https://github.com/idris-lang/Idris2/blob/78ff2059f39cb65ad9ed09dec1416621b6e662a5/libs/contrib/Control/Algebra.idr#L85}{Ring}).
However, in Agda, the ring has a multiplicative identity
(\MYhref{https://github.com/agda/agda-stdlib/blob/42d13fdea1b1861e545c5a0799d605edfa0acc31/src/Algebra/Structures.agda#L459}{IsRing})
and rng is defined as ringWithoutOne that has no multiplicative identity
(\MYhref{https://github.com/agda/agda-stdlib/blob/f7bfeba6cfc03b9488e6d91ea0b011831f53be8a/src/Algebra/Structures.agda#L626}{IsRingWithoutOne}).
This ambiguity in naming is also seen in literature. For example,
\cite{anh1987morita}, \cite{jacobson1956structure},
\cite{persson1999application} define ring without the multiplicative identity
and \cite{lehmann1977algebraic}, \cite{geuvers2002constructive} define ring with
multiplicative identity. Another example is the same structure having multiple
definitions like Quasigroups. Quasigroups can be defined as a type(2) algebra
with Latin square property or as a type(2,2,2) with left and right division
operators. Both definitions are equivalent \cite{shcherbacov2003elements}, but
they are structurally different. This chapter identifies and classifies five
important problems that arise when defining types of algebraic structures in
proof assistant systems.

\section{Ambiguity In Naming}
Ambiguity arises when something can be interpreted in more than one way. The
example of a quasigroup having more than one definition can give rise to a
scenario of making an incorrect interpretation of the algebraic structure when
it is not clearly stated. In abstract algebra and algebraic structure, these
scenarios can be more common and this can be attributed to the lack of naming
convention that is followed in naming algebraic structures and their properties.
For example, consider algebraic structures ring and rng. Some mathematicians
define a ring as an algebraic structure that is an Abelian group under addition,
a monoid under multiplication, multiplication distributes over addition and has
an annihilating zero. This definition is also named explicitly as ring with unit
or ring with identity. Rng is defined as an algebraic structure that is an
Abelian group under addition and a semigroup under multiplication. The same
structure is also defined as ring without identity or ring without unit.
However, these definitions are often interchanged i.e., some mathematicians
define ring as ring without identity that is multiplication has no identity or
is a semigroup. This ambiguity may be attributed to the language of origin of
the algebraic structures. In this case, rng is used in French whereas ring is in
English. These confusions can be seen in literature and in online blogs where it
is difficult to imply the definition of intent when they are not explicitly
defined. 

In Agda, a ring structure is defined as an algebraic structure with two binary
operations $+$ and $*$, one unary operator $^{-1}$, and two elements $0$ and $1$
on setoid $A$. $(A,+,^{-1},0)$ is an Abelian group and $(A,*,1)$ forms a monoid.
The binary operation $*$ distributes over $+$, and it has annihilating zero.

\begin{minted}[breaklines,samepage]{Agda}
record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
  +-isAbelianGroup : IsAbelianGroup + 0# -_
  *-cong           : Congruent₂ *
  *-assoc          : Associative *
  *-identity       : Identity 1# *
  distrib          : * DistributesOver +
  zero             : Zero 0# *

open IsAbelianGroup +-isAbelianGroup public
\end{minted} 

\inline{Rng} is defined as \inline{IsRingWithoutOne} that is a ring structure without
multiplicative identity.

\begin{minted}[breaklines,samepage]{Agda}
record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where
field
  +-isAbelianGroup : IsAbelianGroup + 0# -_
  *-cong           : Congruent₂ *
  *-assoc          : Associative *
  distrib          : * DistributesOver +
  zero             : Zero 0# *

open IsAbelianGroup +-isAbelianGroup public
\end{minted}

Lam in \cite{lam1991first} discusses the confusion between "Ring" and "Rng" and
how the term "Rng" refers to rings without unity, leading to potential
misunderstandings in the literature. The issue is also seen in
\cite{bosma1997magma}, \cite{jacobson1956structure},
\cite{persson1999application}, \cite{lehmann1977algebraic}, and
\cite{geuvers2002constructive}.

Another example of ambiguity arises when defining structure nearring. Nearring
is defined as a structure for which addition is a group and multiplication is a
monoid, and multiplication distributes over addition. However, some
mathematicians use the definition where multiplication is a semigroup. The same
confusion also arises in defining semiring and rig structures.
\cite{rasuli2022anti} states that the term rig originated as a joke that it is
similar to rng and is missing the alphabet "n" and "i" to represent that the
identity does not exist for these structures. In Agda, the algebraic structure
rig is defined as \inline{SemiringWithoutOne} where one represents the
multiplicative identity.

For axioms of structures, the names are usually invented when defining the
structure. As an example when defining Kleene Algebra in Chapter 7,
\inline{starExpansive} and \inline{starDestructive} names were invented
(inspired from what is used in literature). Due to the lack of standardized
names, many names can be coined for the same axiom. 

\section{Equivalent But Structurally Different}
Quasigroup structure is an example that can be defined in two ways that are
equivalent but structurally different. A type (2) Quasigroup can be defined as a
set Q and binary operation ∙ that forms a magma and satisfies the Latin square
property. Latin square property states that for each a, b in set Q there exists
unique elements x, y in Q such that the following property is satisfied:
\begin{equation}
a ∙ x = b
\end{equation}
\begin{equation}
y ∙ a = b
\end{equation}
Another definition of quasigroup is given as type a (2,2,2). In Chapter 5, we
defined quasigroup with three binary operations ($∙, \backslash, /$) that
satisfy the identities below.

\begin{equation} \label{eq_L-leftdivides1}
  x\ ∙\ (x\ \backslash\ y) \ = \ y
\end{equation}
\begin{equation} \label{eq_L-rightdivides1}
  x\ \backslash\ (x\ ∙\ y)\ = \ y
\end{equation}
\begin{equation} \label{eq_R-leftdivides1}
  (y\ /\ x)\ ∙\ x \ =\ y
\end{equation}
\begin{equation} \label{eq_Rirightdivides1}
  (y\ ∙\ x)\ /\ x \ =\ y
\end{equation}

A quasigroup that is a type (2) algebra and a quasigroup that is a type (2,2,2)
algebra are equivalent but are structurally different. We can show that both the
definitions of quasigroup are isomorphic to each other. The proof is adapted
from \cite{shcherbacov2003elements}.

\begin{enumerate}
  \item 
  Let $(Q, ∙)$ be a quasigroup (satisfies Latin square property). Since $ a ∙ x =
  b$, we can associate this with an operation such that $a ∙ x = b \mapsto a
  \backslash b = x$. We can substitute this in equation $a ∙ x = b$ to get $a ∙ (a
  \backslash b) = b \forall a,b \in Q$ which is \ref{eq_L-leftdivides1}.

  Similarly, $y ∙ a = b \mapsto a / b = y$. Substituting this we get $ (a / b) ∙ a
  = y$ which is \ref{eq_R-leftdivides1}.

  Equation \ref{eq_L-rightdivides1} and \ref{eq_Rirightdivides1}, follows from the
  definition of operation $\backslash$ and $/$. That is $x \backslash (x ∙ y) = y \mapsto x
  ∙ y = x ∙ y$ and $(y ∙ x) /x \mapsto y ∙ x = y ∙ x$.

\item 
  Let $(Q,∙, \backslash, /)$ be a quasigroup (satisfies division). We need to show
  the existence of a unique solution of equation $ a ∙ x = b$ and $y ∙ a = b$.

  To prove the existence of a solution, let $x = a\backslash b$ and $y = b / a$.
  Substituting $x$ and $y$ in above equation, we get $a ∙ x = a ∙ (a \backslash b)
  = b$ from equation \ref{eq_L-leftdivides1} and $ y ∙ a = (b / a) ∙ a = b$ from
  equation \ref{eq_R-leftdivides1}.

  To prove the uniqueness of the solution, we can assume there exist two solutions
  $x_1$ and $x_2$ that is $a ∙ x_1 = b$ and $a ∙ x_2 = b$. Then $x_1 = a
  \backslash b$. Therefore we get $x_1 = a \backslash b = a \backslash (a ∙ x_2) =
  x_2$ from equation \ref{eq_R-leftdivides1}

  Similarly, if $y_1$ and $y_2$ two solutions that is $y_1 ∙ a = b$ and $y_2 ∙ a = b$, we get 
  $y_1 = b / a = (y_2 ∙ a) / a = y_2$ from equation \ref{eq_Rirightdivides1}.

\end{enumerate}

In the algebra hierarchy, a Loop is an algebraic structure that is a quasigroup
with identity. It can be observed the same problem persists in the hierarchy. If
a loop is defined with a quasigroup that is a type (2,2,2) algebra then, a loop
structure of type (2) will be forced to be defined with a suboptimal name. One
possible solution to this problem is to define the structures in different
modules and import restrict them when used. This problem of not being able to
overload names for structures also affects when defining types of quasigroup or
loops such as bol loop and moufang loop. Since quasigroup is defined in terms of
division operation, the loop is also defined as a type (2,2,2) algebra in the Agda
standard library.

\section{Redundant Field In Structural Inheritance}
Redundancy arises when there is duplication of the same field. In programming
redundant code is considered a bad practice and is usually avoided by
modularizing and creating functions that perform similar tasks. In algebraic
structures, redundant fields can be introduced in structures that are defined in
terms of two or more structures. For example, semiring can be defined with
commutative monoid under addition and a monoid under multiplication. In Agda,
both monoid and commutative monoid have an instance of equivalence relation.
Hence, if semiring is defined in terms of commutative monoid and monoid then
this definition of the semiring will have a redundant equivalence field. This
redundancy can also be seen in other structures like ring, lattice, module, and
other algebraic structures. To remove this redundant field in Agda, the
structure except the first is opened and expressed in terms of independent
axioms that they satisfy. For example, semiring without identity or rig
structure in Agda is defined as:

\begin{minted}[breaklines,samepage]{Agda}
record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
field
  +-isCommutativeMonoid : IsCommutativeMonoid + 0#
  *-cong                : Congruent₂ *
  *-assoc               : Associative *
  distrib               : * DistributesOver +
  zero                  : Zero 0# *

open IsCommutativeMonoid +-isCommutativeMonoid public
\end{minted}

From the above definition, we can observe that the operation $*$ is a semigroup
expressed with axioms congruent and associative. But, there is no field to
say that $*$ is a semigroup. To overcome this problem an instance is created in
the definition as follows along with near semiring structure.

\begin{minted}[breaklines,samepage]{Agda}
*-isMagma : IsMagma *
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = *-cong
  }

*-isSemigroup : IsSemigroup *
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc   = *-assoc
  }

isNearSemiring : IsNearSemiring + * 0#
isNearSemiring = record
  { +-isMonoid    = +-isMonoid
  ; *-cong        = *-cong
  ; *-assoc       = *-assoc
  ; distribʳ      = proj₂ distrib
  ; zeroˡ         = zeroˡ
  }
\end{minted}

The above technique will remove the redundant equivalence relation. However, it
fails to express the structure in terms of two or more structures that are
commonly used in literature and other systems. Agda 2.0 removed redundancy by
unfolding the structure. This solution should ensure that the structure exports
the unfolded structure whose properties can be imported when required.

\section{Identical Structures}
In abstract algebra when formalizing algebraic structures from the hierarchy,
the same algebraic structure can be derived from two or more structures. One
such example is Nearring. Nearring is a group under addition, a monoid under
multiplication, and multiplication right distributes over addition. In this
case, nearring is defined using two algebraic structures group and monoid.
Another definition of nearring can be derived using the structure quasiring.
Quasiring is an algebraic structure in which addition is a monoid,
multiplication is a monoid and multiplication distributes over addition. Using
this definition of quasiring, nearring can be defined as a quasiring that has an
additive inverse. In Agda nearring is defined in terms of quasiring with
additive inverse as: 

\begin{minted}[breaklines,samepage]{Agda}
record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
field
  isQuasiring : IsQuasiring + * 0# 1#
  +-inverse   : Inverse 0# _⁻¹ +
  ⁻¹-cong     : Congruent₁ _⁻¹

open IsQuasiring isQuasiring public

+-isGroup : IsGroup + 0# _⁻¹
+-isGroup = record 
  { isMonoid = +-isMonoid 
  ; inverse = +-inverse 
  ; ⁻¹-cong = ⁻¹-cong 
  }
\end{minted}

In some literature, a nearring is defined such that multiplication is a
semigroup. This can be attributed to the problem of ambiguity. It can be
analyzed that having two different definitions for the same structure is not a
good practice. If nearring is defined using quasiring then it should also give
an instance of an additive group without having to construct it when using the
above formalization. This solution might solve the problem at first but in
practice, this becomes tedious and may go to a point at which this can be
impractical especially when formalizing structures at higher levels in the
algebra hierarchy.

\section{Equivalent Structures}
Consider the example of idempotent commutative monoid and bounded semilattice.
Both idempotent commutative monoid and bounded semilattice are equivalent
structures that are also of the same type. It is redundant to define two different
structures from different hierarchies. Instead, in Agda, aliasing may be used to
say that the bounded semilattice is same as the idempotent commutative monoid.
Idempotent commutative monoid is defined and an aliasing for bounded semilattice
is given.

\begin{minted}[breaklines,samepage]{Agda}
record IsIdempotentCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeMonoid : IsCommutativeMonoid ∙ ε
    idem                : Idempotent ∙

  open IsCommutativeMonoid isCommutativeMonoid public

IsBoundedSemilattice = IsIdempotentCommutativeMonoid
module IsBoundedSemilattice {∙ ε} (L : IsBoundedSemilattice ∙ ε) where

  open IsIdempotentCommutativeMonoid L public
\end{minted}

Some mathematicians argue that bounded semilattice and idempotent
commutative monoid are not the same structures but are isomorphic to each other.
We do not consider this argument in the scope of this thesis.

\section{Summary}
The table below provides a summary of the issues classified and recommendations
to mitigate the issues.

\begin{longtable}{|p{4cm}|p{9cm}|}
  \caption{Problem in programming algebra} 
  \hline \multicolumn{1}{|c|}{\textbf{Issue}} & \multicolumn{1}{c|}{\textbf{Recommendation}}\\
  \hline
  Ambiguity in naming & \begin{itemize}[left=0pt,topsep=0pt]
      \item Encouraging standardization by adopting commonly accepted definitions
      and terminology.
      \item When defining terms in standard libraries or in literature, provide
      contextual clarification when introducing potentially ambiguous terms.
    \end{itemize}\nointerlineskip\\
  \hline
  Equivalent but structurally different & \begin{itemize}[left=0pt,topsep=0pt]
    \item Provide proofs for equivalence in algebraic structures.
    \item Make the system capable of overloading names.
    \item Provide commonly used definitions in different modules to avoid conflict.
  \end{itemize}\nointerlineskip\\
  \hline
  Redundant field in structural inheritance & \begin{itemize}[left=0pt,topsep=0pt]
    \item Unfold structure to remove redundant fields.
    \item Provide all instances of structure that were available before unfolding. 
  \end{itemize}\nointerlineskip\\
  \hline
  Identical structures & \begin{itemize}[left=0pt,topsep=0pt]
    \item Make a note of diamonds in the hierarchy when defining structures.
    \item Provide the instance of structure that was not defined with the field.
  \end{itemize}\nointerlineskip\\
  \hline
  Equivalent structures &\begin{itemize}[left=0pt,topsep=0pt]
    \item Give aliasing instead of defining the structure again.
    \item Provide proof if the structures are isomorphic to each other.
  \end{itemize}\nointerlineskip\\
  \hline
  \end{longtable}