agda
`IntegralSemiring` proposal
Matthew Daggitt wrote on lib-2.2-rc1 on January 4, 2025
product≢0 : All NonZero ns → NonZero (product ns) while I agree that it would be good to develop the theory in terms of an appropriate algebraic structure, unfortunately the library is not currently set up to do so. We would need someone to be motivated to make those contributions, but regardless those changes would also not make it into v2.2.
The --attached archive-- contains the .agda files that set up lib-2.2 to do so, which makes it lib-2.2-next. It is set in the standard library style. It consists of the following files.
Algebra-Definitions.agda
to be merged to Algebra/Definitions.agda of lib-2.2.
It defines the property NoZeroDivisor
zero _∙_ = {x y : A} → (x ∙ y) ≈ zero → x ≈ zero ⊎ y ≈ zero
Algebra-Properties-Monoid.agda to be set as Algebra/Properties/Monoid.agda. It defines
Π₁ : C → List C → C -- product of a nonempty list of elements,
Π : List C → C -- product of a list of elements.
It proves
Π[x] : ∀ x → Π (x ∷ []) ≈ x
Algebra-Structures.agda to be merged to Algebra/Structures.agda. It defines
record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
isSemiring : IsSemiring + * 0# 1#
0≉1 : ¬ 0# ≈ 1#
noZeroDivisor : NoZeroDivisor 0# *
open IsSemiring isSemiring public
Algebra-Bundles.agda to merge to Algebra/Bundles.agda. It defines
record IntegralSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
...
isIntegralSemiring : IsIntegralSemiring _≈_ _+_ _*_ 0# 1#
Algebra-Properties-Semiring-Integral.agda to set as Algebra/Properties/Semiring/Integral.agda. It proves
nonzero*nonzero : ∀ {x y} → x ≉ 0# → y ≉ 0# → (x * y) ≉ 0#
nonzero*nonzero {x} {y} x≉0 y≉0 xy≈0 with noZeroDivisor xy≈0
... | inj₁ x≈0 = x≉0 x≈0
... | inj₂ y≈0 = y≉0 y≈0
Π≉0 : {xs : List Carrier} → All (_≉ 0#) xs → Π xs ≉ 0#
Π≉0 {_} [] = 1≉0
Π≉0 {x ∷ xs} (x≉0 ∷ xs≉0) = nonzero*nonzero x≉0 (Π≉0 xs≉0)
Data-Nat-Properties.agda to be merged to Data/Nat/Properties.agda. It proves
+-*-isIntegralSemiring : IsIntegralSemiring _+_ _*_ 0 1
+-*-isIntegralSemiring = record
{ isSemiring = +-*-isSemiring
; 0≉1 = λ()
; noZeroDivisor = λ m {n} → m*n≡0⇒m≡0∨n≡0 m {n}
}
But this latter instance is not type-checked, I do not know why, so far. After it is fixed, it will be added there
integralSemiring : IntegralSemiring _ _
for ℕ.
If all this is accepted and merged, it will be easy to add
- IntegralRing, IntegralDomain to Algebra.Bundles,
- the instance of IntegralDomain to Integer.Properties,
- several more proofs for the fnction
Π.
I wrote a certain erroneous message and have deleted it. Please, read this new one.
I think now that the notice by James@jamesmckinna is important.
I have missed the following point.
Consider the example with Field: "CommutativeRing in which each nonzero element is invertible".
The classical definition has the second axiom ∀ {x} → x ≉ 0# → x ∣ 1#.
And the Agda library would probably need to change this to
∀ x → x ≈ 0# ⊎ x ∣ 1#.
And IsField can be expressed as
record IsField 0# 1# + * ... where
field
isCommutativeRing : IsCommutativeRing ...
inversion : ∀ x → x ≈ 0# ⊎ x ∣ 1# --
-- x equals zero or x divides unity
Probably @jamesmckinna and @JacquesCarette meant this approach and call it "positive".
Right?
For the two definitions, we have F = (¬ A → B) vs G = A ⊎ B.
Then, G → F is derived in Agda:
G→F (y→Ay⊎By) x ¬Ax with (y→Ay⊎By) x
... | inj₂ Bx = Bx
... | inj₁ Ax = contradiction Ax ¬Ax
And F → G cannot be derived in Agda. So, classical is weaker.
Do I mistake?
If A is decidable, then F → G is derived too.
So, the traditional classical definition is not equivalent to the one desirable for Agda.
Right?
If so, how to name it in the Agda library?
I suggest to use the same name.
On practice, this notion difference will not show great.
Because in computational symbolic algebra almost all sensible methods are based on a decidable equality and even on decidable divisibility.
Now consider the definition of IsIntegralSemiring.
The classical definition in mathematics will be this:
-- recall:
NoZeroDivisor = {x y : A} → (x * y) ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
(I)
record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set _ where
field
isSemiring : IsSemiring + * 0# 1#
0≉1 : 0# ≉ 1#
noZeroDivisor : NoZeroDivisor 0# *
Here 0≉1 is equivalent to "not all elements equal zero".
The definition for Agda is proposed as
(II)
record IsIntegralSemiring (+ * : Op₂ A) (0# 1# : A) : Set _ where
field
isSemiring : IsSemiring + * 0# 1#
0≈1∨NoZeroDivisor : 0# ≈ 1# ⊎ NoZeroDivisor 0# *
I expect this is what was meant by James@jamesmckinna.
Is this?
Then (I) ⇒ (II) is derived constructively:
Suppose that R : IntegralSemiring-I.
Then, it holds NoZeroDivisor 0# *, and 0≈1∨NoZeroDivisor holds as the second member of disjunction,
and R : IntegralSemiring-II.
Try to derive (II) ⇒ (I) when all the involved relations are decidable.
Suppose that R : IntegralSemiring-II.
case (0 ≟ 1 , NoZeroDivisor?)
of
(no 0≉1, yes noZeroDiv) → 0≉1 , noZeroDiv -- (I) proved
(no 0≉1, no ¬noZeroDiv) → Impossible case, because the second disjunction member holds.
(yes 0≈1, no ¬noZeroDiv) → Impossible case, because zero semiring contradicts to existence of zero divisor.
(yes 0≈1, yes noZeroDiv) → This case is possible, (II) cannot be proved in this case.
So (I) and (II) are equivalent for all nonzero semirings.
Right?
If so, then I suggest the version (II) of the definition and expect that it is actually what James@jamesmckinna suggested
(is it?).
But may be I have missed something. So, please, comment.
Sergei, thanks very much for the careful consideration of my earlier comments, and for taking the trouble to check that, at least in the presence of decidability, that there is only a difference of presentation between the two approaches, but that the 'positive' formulation is more general. (Incidentally, while I no longer really remember the source(s), I guess that the terminology of 'positive' comes from substructural logics/proof theory, or first-order model theory?, to refer to theories whose axiomatisation involves no negated atoms/formulae... just as 'geometric' refers to that fragment involving ∃ and ∨ occurring positively, and thus are preserved by geometric morphisms between toposes... and the role of category theorists/categorical logic in championing non-classical/substructural logics as the internal logics of various categories is a significant influence on 'constructivism' generally, as well as individuals such as myself...)
The emphasis on 'positive' formulations, as a design style, I take originally from Mines, Richman and Ruitenberg, "A Course in Constructive Algebra", and perhaps more so from other writings of Fred Richman (whose website, like that of Gabriel Stolzenberg, another early influence on my thinking, seems inaccessible at the moment, alas).
I think that, following Richman (and of course, Bishop and others before that), working in a constructive meta-language such as the type theory of Agda is to be taken as an opportunity to work a bit harder in exploring mathematical concepts, while keeping a firm eye on their classical/orthodox definitions. Richman's pons asinorum example of a positive/constructive resolution of the problem of finding "two irrationals a, b such that a ̂ b is rational" is another, rather simpler, instance of the phenomenon.
James, thank you for your comments.
I an surprised with that I have forgotten light-headedly of the difference between ¬ A → B and A ⊎ B.
Now I revisit the definitions of Field and IntegralSemiring and try to accommodate them to constructive algebra in a better way.
My last letter in this issue have several places with the questions like "Right?", "is it?".
The comments are welcome from people.
I think that the above "positive" approach to definitions of Field and IntegralSemiring accommodates them better to the needs of constructive algebra, because sometimes the equality is not decidable. On the other hand we need to keep in mind that the case of a non-decidable equality is esoteric in computational algebra. Most essential methods there require decidable equality and many of them also require decidable divisibility relation.
Please, find attached the improved version archive of the proposal. First see there Readme.lagda.
#2563 resolves most of this proposal into the 'right' places in stdlib, but leaves unfinished the general product construction, and its NonZero properties to subsequent PRs, for reasons of complexity, together with a wider need to refactor things fo v3.0 before proceeding.
The fresh version (version 3) of the proposal had been lost somewhere in pull requests.
For any occasion I upload it here: