I recently added a semiring to Granule which has two grades (0 and 1), and has 1 + 1 = 0.
It turns out that this semiring can be used to track whether a hypothesis is discharged an even or odd number of times (see examples/ooz.gr).
Please share any thoughts you have on possible applications for this semiring! I'm imagining that this could have some interesting applications in binary trees (balanced or otherwise).
Examples welcome :)
I am fairly confident that this semiring can be generalised, to form a family of semirings P k for k in Nat>0. Then the operations in the semiring are mod k, thus (n + m)_{P k} = ((n + m) % k)_{Nat} (exploring this over on #149).
I recently added a semiring to Granule which has two grades (
0and1), and has1 + 1 = 0.It turns out that this semiring can be used to track whether a hypothesis is discharged an even or odd number of times (see
examples/ooz.gr).Please share any thoughts you have on possible applications for this semiring! I'm imagining that this could have some interesting applications in binary trees (balanced or otherwise).
Examples welcome :)
I am fairly confident that this semiring can be generalised, to form a family of semirings
P kfork in Nat>0. Then the operations in the semiring aremod k, thus(n + m)_{P k} = ((n + m) % k)_{Nat}(exploring this over on #149).