On Fri, 24 Apr 2020 18:50:11 -0700, Mario Carneiro <[email protected]> wrote: > I like the idea of using ++ for concatenation, particularly in ascii > notation, since I don't want to try to reproduce a frown symbol in ascii. I > think the most common symbol for this is adjacency though.
I also have (mild) prefererence for "++" to represent concatenation. In particular, I'd prefer "++" as the ASCII representation, with a Unicode display of ⧺ (U+29FA) and \doubleplus in LaTeX (package unicode-math). This is somewhat common in Computer Science; Haskell uses "++" for concatenation, and many other programming languages use "+" for concatenation (but they can use types to figure out what overloaded operation was meant). I think ++ would make the ASCII display a little simpler, and many people think of "add" and "concatenate" as related... so having intentionally similar symbols has some mild advantages. Frown looks a little like intersection, even though there's no relationship, and that could be considered a negative for it. That said, frown has significant use, it's not terribly ambiguous, and it just works, so I'm not unhappy with it. Bottom line: I have a minor preference for ++, but it's not a big deal to me. I agree that "no displayed symbol, just adjacency" is common. However, generally in Metamath we try to be very explicit, so I think we shouldn't have "no displayed symbol" in Metamath (at least in set.mm) for concatenation. Notation is hard. There's a brief related discussion here: https://math.stackexchange.com/questions/298648/is-there-a-common-symbol-for-concatenating-two-finite-sequences I don't like the other options discussed there (the other symbols already have other conflicting meanings), so I think frown and doubleplus are the contenders. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jSB1O-00047l-Mh%40rmmprod06.runbox.
