Add new `Bool` action on a `RawMonoid` plus properties #2450

jamesmckinna · 2024-07-31T14:33:36Z

Prompted by @JacquesCarette 's desire to further systematise the refactoring in #2407 , this adds two operations which appear ad hoc in the normal form semantics for IdempotentCommutativeMonoids, but are yet more instances of a (Raw)MonoidAction cf. #2348 / #2350 by analogy with the corresponding actions in the normal form semantics for CommutativeMonoids.

NB

Nat-action arises because (Nat, +, 0) is the free commutative monoid on one generator...
similarly, (Bool, /, true) is, I think, the free idempotent commutative monoid on one generator?

Could be left as DRAFT, pending further work cf. #2351 , but worth inviting review now, I think.

NB. possible issues:

names of things: current notation is terrible, unfortunately, so suggestions welcome!
left-/right- symmetric versions, ie. x + n × y as well as n × x + y etc.
possible refactoring of the existing definitions as instances of these generalised 'affine' ones?
refactoring not yet applied to Algebra.Solver.*Monoid etc.
... further systematisation of existing Algebra.Definitions.RawMonoid._×_ operation etc. possible as well?
Fairbairn threshhold?

jamesmckinna · 2024-08-02T05:20:54Z

Ooops (mistake to try to abstract immediately over MonoidAction... the Nat case is a MagmaAction, but not a MonoidAction... the 0/1 cases don't match up right). Moving to DRAFT while I rethink this.

gallais · 2024-08-06T14:01:00Z

Conor's disembodied voice tells me we should use a non-symmetric infix symbol for this non-symmetric action.

jamesmckinna · 2024-08-13T07:38:45Z

Conor's disembodied voice tells me we should use a non-symmetric infix symbol for this non-symmetric action.

I'm genuinely torn over this. I understand, appreciate, and even largely agree with, the doctrine (prevalent in WG2.1) that non-symmetric/commutative operations should be given non-symmetric notation. Nevertheless, we don't insist that that a Group operation be given a non-symmetric symbol... even if we do distinguish it as _+_ (or something else 'obviously connoting commutativity') in the AbelianGroup case.

Nevertheless, I think we do ourselves (or else: type theory as a principled metalanguage for the prosecution of such doctrine) a disservice by taking the 'old-fashioned' CFG view of notation not coming a priori with a type attached.

The case here, as more generally in the draft PR on Algebra.Action, is that the point of an action is that it is extending the domain of applicability of a given operation (however symbolised) to the structure on which it acts... and the generalised associativity property of a MagmaAction is precisely where the extended notation bites, visually/mnemonically at least.

You might object that the Bool action defined here, or Algebra.Definitions.RawMonoid. _×_ aren't in and of themselves 'commutative'... but that obscures the fact that their flipped counterparts are in fact extensionally equal to these definitions.

So perhaps the way out of the bottle is to tag the symbol with ˡ and ʳ annotations, and use infix symbol positions to record where the tail-recursive accumulator argument should go in the extended notation, yielding four compound symbols in all?

I guess I could live with that... modulo leaving _×_ unchanged as 'legacy' (yuk)?

src/Algebra/Properties/Monoid/Mult.agda

MatthewDaggitt

Otherwise looks good.

JacquesCarette · 2024-08-15T13:31:58Z

src/Algebra/Definitions/RawMonoid.agda

+infixr 8 _∧_
+
+_∧_ : Bool → Carrier → Carrier
+b ∧ x = if b then x else 0#


Strictly speaking, this could be defined for any Pointed structure with an apartness relation, as an action on a Pointed structure.

How is the above 'conjuction'?

OK, I think that's fair... I was being pretty ad hoc in wanting to add this by analogy with the Nat action already defined there, as then these two instances of a phenomenon (eventually: wreath product) are the relevant ones for the Algebra.Solver.*CommutativeMonoid refactorings #2407 #2457 ... and I'm still unhappy about the general picture for Pointed things in the library, so don't (yet) want to reopen that can of worms...

As for it being 'conjunction', well it clearly generalises it: for Carrier being that of the Monoid structure on Bool given by _∨_ with unit false,

b ∧ x = if b then x else false

is a definition of 'conjunction'... yes!?

Yes, that is the operational definition of 'conjunction' on Bool.

I guess that I was thinking along the lines of "if b is the least element then x else some-distinguished-point" as the general meaning. It feels more action-y. 'conjunction' feels like it's a coincidence when Carrier is Bool.

Revisiting: maybe better thought as a 'guarded' value?

Yes, I guess that this is a classic instance of (idealised) haskell's MonadZero.guard (if I've got this right; hackage seems to suggest that's not quite the case...)

b ∧ x is essentially the pattern x <$ guard b which AFAIK does not have a name
but is very useful.

JacquesCarette · 2024-08-15T13:32:39Z

src/Algebra/Definitions/RawMonoid.agda

+_∧_ : Bool → Carrier → Carrier
+b ∧ x = if b then x else 0#
+
+-- tail-recursive optimisation


optimisation of what? It doesn't seem like an optimisation of the above? What am I missing?

As with the TCOptimised forms of (monoid) sum and multiplication, the 'optimisation' lies in avoiding having to explicitly track terms of the form x + 0# when these can be computed away instead to x... But I admit I haven't quite got my story straight yet... ;-)

As witnessed by b∧x∙y≈b∧x+y...

It still feels like a stretch. I do like the optimization of an action not doing a (statically known) null operation, a lot. I'm still worried that this particular case is a coincidence rather than fundamental!

Well I think it extends to the Nat cases as well (but obscured in the current presentation, which doesn't introduce the tail-recursive forms... but see #2475 )

src/Algebra/Properties/Monoid/Mult.agda

JacquesCarette · 2025-07-30T20:34:22Z

What prevents this from losing its DRAFT status?

jamesmckinna · 2025-07-31T09:16:37Z

What prevents this from losing its DRAFT status?

Off the top of my head:

no bandwidth to think about the problem... incl revisiting
does it solve the problem I wanted it to?
does it help with Refactor Algebra.Solver.*Monoid (further!) #2457 as I had hoped?

All of the above are slightly beyond my capacity to think right now, so DRAFT seemed to safest way to mark "I'll come back to this (at some point)"

jamesmckinna · 2025-11-25T03:43:49Z

Notes to self (and any other interested parties here):

[ refactor/design ] left- and right- actions of normal subgroups on their ambient group #2892 provides more primitive infrastructure for definitions such as those given here?
wreath product constructions cf. Add Algebra.Construct.WreathProduct and/or Algebra.Construct.SemiDirectProduct #2351
... 'actions induced by homomorphisms' more generally

It may well be that this all needs reorganisation down the road, at which point it may be clearer (than it is to me now) what would be necessary/useful to isolate 'sensible' common abstractions.

JacquesCarette · 2025-12-24T17:02:28Z

src/Algebra/Properties/Monoid/Mult.agda

 ×-homo-+ x 0       n = sym (+-identityˡ (n × x))
 ×-homo-+ x (suc m) n = begin
-  x + (m ℕ.+ n) × x    ≈⟨ +-cong refl (×-homo-+ x m n) ⟩
+  x + (m ℕ.+ n) × x    ≈⟨ +-congˡ (×-homo-+ x m n) ⟩


cong followed by sym-assoc is what some of those combinators for Semigroup does in one go.

JacquesCarette · 2025-12-24T17:04:27Z

CHANGELOG.md


+* In `Algebra.Definitions.RawMonoid` action of a Boolean on a RawMonoid:
+  ```agda
+  _∧_    : Bool → Carrier → Carrier


I'm with @gallais here (and Conor too): I find this symmetric symbol quite misleading.

Yes, I wonder if these things could be (appropriately) re-notated in terms of #2894 , for all its faults?

Could be something like ?> by analogy to $>.

JacquesCarette · 2025-12-24T17:06:28Z

src/Algebra/Definitions/RawMonoid.agda

+infixr 8 _∧_
+
+_∧_ : Bool → Carrier → Carrier
+b ∧ x = if b then x else 0#


Revisiting: maybe better thought as a 'guarded' value?

Add new Bool action on a RawMonoid plus properties

d666858

jamesmckinna added the addition label Jul 31, 2024

jamesmckinna requested a review from JacquesCarette July 31, 2024 14:49

jamesmckinna marked this pull request as draft August 2, 2024 05:21

MatthewDaggitt reviewed Aug 14, 2024

View reviewed changes

src/Algebra/Properties/Monoid/Mult.agda Outdated Show resolved Hide resolved

MatthewDaggitt reviewed Aug 14, 2024

View reviewed changes

src/Algebra/Properties/Monoid/Mult.agda Outdated Show resolved Hide resolved

MatthewDaggitt reviewed Aug 14, 2024

View reviewed changes

JacquesCarette requested changes Aug 15, 2024

View reviewed changes

jamesmckinna and others added 2 commits August 16, 2024 07:53

response to review comments on draft

7d4d3a0

Merge branch 'master' into Bool-action

1caa018

jamesmckinna mentioned this pull request Aug 25, 2024

Refactor Algebra.Solver.*Monoid (further!) #2457

Draft

jamesmckinna mentioned this pull request Sep 5, 2024

[DRY?] Direct definition vs. generic combinators, ctd. in Algebra.Definitions.RawMonoid #2475

Open

JacquesCarette requested changes Dec 24, 2025

View reviewed changes

Add new Bool action on a RawMonoid plus properties #2450

Are you sure you want to change the base?

Add new Bool action on a RawMonoid plus properties #2450

Uh oh!

Conversation

jamesmckinna commented Jul 31, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna commented Aug 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gallais commented Aug 6, 2024

Uh oh!

jamesmckinna commented Aug 13, 2024

Uh oh!

Uh oh!

Uh oh!

MatthewDaggitt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Aug 27, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

JacquesCarette commented Jul 30, 2025

Uh oh!

jamesmckinna commented Jul 31, 2025

Uh oh!

jamesmckinna commented Nov 25, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Jan 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Add new `Bool` action on a `RawMonoid` plus properties #2450

Add new `Bool` action on a `RawMonoid` plus properties #2450

jamesmckinna commented Jul 31, 2024 •

edited

Loading

jamesmckinna commented Aug 2, 2024 •

edited

Loading

jamesmckinna Aug 27, 2024 •

edited

Loading

jamesmckinna Jan 8, 2026 •

edited

Loading