RFC: Boolean Semiring

Stream: mathlib4

[Rudy Peterson]

Hello,

In my research it would be helpful to have a boolean Semiring, where addition is or instead of xor.

Would it make sense to add this, or would such a new Add instance conflict with the existing Boolean Ring instances, where addition is xor?

Thanks!

[Aaron Liu]

sounds similar to docs#IdemSemiring

[Kenny Lau]

if you want a different instance, you should probably use a type synonym, i.e. do something like
def Bool' := Bool
and then construct the instance on Bool'

[Aaron Liu]

I think they're talking about docs#BooleanRing

[Aaron Liu]

not putting a different semiring instance on Bool

[Yaël Dillies]

Hey, can you clarify what exactly is a boolean semiring? Is it a specific (family of) ring(s) or is it any semiring satisfying some axioms? If so, do those axioms happen to be captured by docs#IdemSemiring ?

[Yaël Dillies]

nLab claims there are at least five different definitions of "boolean semirings" in the literature

[Rudy Peterson]

Thanks for all of the replies!

Basically, I need a Semiring instance for Bool where Add is or ||. I don't mean a type or family of ring(s).

For my general work, I believe that docs#IdemSemiring is too restrictive, since I also care about Semirings in general, not just a Semiring instance for Bool.

I am worked on weighted formal language theory, where automata and regular expressions also produce a weight, and the type of the weights need to satisfy the Semiring axioms.

Currently, I am working on showing that one may construct an unweighted/standard NFA given a weighted NFA with boolean weights, and for this case I believe I need the Add operation to be boolean or.

[Rudy Peterson]

Perhaps for this general construction (weighted to unweighted NFA) I do not need the boolean semiring specifically, but I believe it would be the most elegant

[Rudy Peterson]

I performed a similar construction to produce an unweighted/normal docs#DFA from a boolean weighted DFA, and this case the Semiring addition operator did not matter since for weighted DFAs only semiring multiplication matters (i think, or at least in this case)

[Kenny Lau]

see my answer

[Rudy Peterson]

Kenny Lau said:

if you want a different instance, you should probably use a type synonym, i.e. do something like
def Bool' := Bool
and then construct the instance on Bool'

is this the standard way to get around something like this in Mathlib or Lean when there are instances with different implementations for the same typeclass and data type?

[Kenny Lau]

yes

[Edward van de Meent]

(see for examples docs#Additive and docs#Opposite)

[Rudy Peterson]

Is there a way to suppress instances from imports and then define my own version of the instance? Or maybethe boolean ring file is not that pervasively imported across Matlib, and for my work I could just avoid importing modules that export that?

[Aaron Liu]

You could disable the instances locally

[Aaron Liu]

in Counterexamples.CharPZeroNeCharZero there's a semiring addmonoidwithone that's sort of like what you want (the addition and multiplication line up) that they use WithZero Unit

[Aaron Liu]

oh it actually has a semiring instance

import Mathlib

#synth Semiring (WithZero Unit)

[Damiano Testa]

Depending on which commit of mathlib you use, WithZero Unit may be Fin 2.

[Rudy Peterson]

Aaron Liu said:

You could disable the instances locally

do you mean like this? It doesn't get rid of the prior instance entirely...?

section boolean

attribute [-instance] instAddBool_mathlib

-- CommRing.toNonUnitalCommRing.toNonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.toDistrib.toAdd
#synth Add Bool

instance myAddBool : Add Bool where add := Bool.or

-- myAddBool
#synth Add Bool

...

end boolean

[Aaron Liu]

yeah you really need to disable a lot of instances

[Rudy Peterson]

I guess for my use-case it would be easier for me to define my own local Semiring Bool instance...

[Aaron Liu]

just use WithZero Unit instead it will save you a lot of trouble

[Rudy Peterson]

Would a Semiring Bool instance (with Add as or) be good for Mathlib in general

Aaron Liu said:

just use WithZero Unit instead it will save you a lot of trouble

what does this do?

[Aaron Liu]

Rudy Peterson said:

Would a Semiring Bool instance (with Add as or) be good for Mathlib in general

No it would not since Bool already has a different semiring instance

[Aaron Liu]

Rudy Peterson said:

Aaron Liu said:

just use WithZero Unit instead it will save you a lot of trouble

what does this do?

Gives you a way to refer to the semiring you want without fighting typeclass