Why do we call them "diamonds" anyway?

Stream: general

[Anne Baanen]

I was just thinking that I don't know why we use the word 'diamond' for defeq issues like nat smul diamond in set actions.

Is it just a case of a surprising generalization of the term "diamond inheritance"?

[Johan Commelin]

They should have been called "non-commuting diagrams" from the get go... but of course "diamond" is catchy :stuck_out_tongue_wink:

[Anne Baanen]

@Eric Taucher mentioned the diamond property in the context of confluent rewriting, which would explain the term quite well.

[Eric Taucher]

For those seeking more beyond the Wikipedia article on confluence, a classic book on the subject is "Term Rewriting and All That" by Franz Baader and Tobias Nipkow (WorldCat)

[Anne Baanen]

So the diamond would be e.g. n • S →infers as→ {set.has_scalar_set.smul, set.add_comm_monoid.nsmul} n S →unfolds to→ (some implementation of scalar multiplication)?

[Eric Wieser]

I guess you're right, there's not always a diamond at all, sometimes the graph is just a wedge, and we're making up the "implementation" node at the bottom to make our terminology work

[Filippo A. E. Nuccio]

I thought it was because of https://arxiv.org/abs/1709.07343 ... :grinning_face_with_smiling_eyes:

[Patrick Stevens]

I guess I thought it was natural because "diamond dependency" is a standard phrase from software denoting Bad Things, so "diamond" already has discordant overtones