Zulip Chat Archive

Stream: general

Topic: Why do we call them "diamonds" anyway?

Anne Baanen (Dec 08 2021 at 11:35):

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 (Dec 08 2021 at 11:43):

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

Anne Baanen (Dec 08 2021 at 11:49):

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

Eric Taucher (Dec 08 2021 at 11:52):

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 (Dec 08 2021 at 11:52):

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 (Dec 08 2021 at 12:03):

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 (Dec 08 2021 at 13:44):

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

Patrick Stevens (Dec 08 2021 at 21:17):

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

Last updated: Dec 20 2023 at 11:08 UTC