Add new 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]

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

[jamesmckinna]

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

[JacquesCarette]

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.

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