[ add ] Bool action on a RawMonoid plus properties

[jamesmckinna]

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]

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]

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

[jamesmckinna]

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)?

[MatthewDaggitt]

Otherwise looks good.

[JacquesCarette]

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

[jamesmckinna]

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... ;-)

[jamesmckinna]

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

[JacquesCarette]

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!

[jamesmckinna]

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 )

[JacquesCarette]

What prevents this from losing its DRAFT status?

[jamesmckinna]

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]

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.

[jamesmckinna]

Converting back from DRAFT:

• fixed proofs (incl. @JacquesCarette 's suggestions)
• fixed notation to be (more like) @gallais 's suggestion (subscript-0 for the 'common' case; I don't really like the use of primes in the names for the accumulator generalisations in Algebra.Definitions.RawMonoid...)
• fixed merge conflicts to resolve CHANGELOG problems etc.

I never quite got as far as finding a common generalisation between the Nat- and Bool-actions, I think that will need to wait until #2350 eventually (!?) lands, so for now, I think this should just stand as-is, modulo nitpicking about names, which I'd be happy to engage with!

[JacquesCarette]

Thanks @gallais for this nice notation suggestions. I'm now happy with this PR.

[JacquesCarette]

Still needs a second approver...