Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
just so that there are (cross-)links to them, I have created brief stub entries on some linear connectives:
and we already talked about
Normally I would apply the word “conjunction” to binary operations, not to an unary operation like . Do other people say “exponential conjunction”?
I hyperlinked the term the way it appears in the nLab entry linear logic
“Exponential conjunction” also sounds wrong to me.
This was introduced by Toby in revision 14, December 2010.
I don't remember whether I made that term up or read it somewhere1. One could also say ‘conjunctive exponential’ or ‘conjunctive modality’, besides ad-hoc names like ‘of course’.
Normally I would apply the word “conjunction” to binary operations
I wouldn't; it's important that truth is the nullary conjunction (where linear logic has both additive and multiplicative truth), and there's also -ary conjunction for by induction.
The exponential conjunction is not as simple as this, but still it is (or may be) built out of other forms of conjunction, now in an infinitary combination.
It apparently existed by 2009 (a year earlier than my edit) on a web page with a novel application and in 2006 in a document discussing something even more complicated. But I never read either of those before. ↩
Thanks for the info.
I was so happy about seeing “exponential conjunction” in the entry, because it gave me an alternative to the inane “of course” and the more inane “bang”.
I suppose just “exponential” works and is standard when the context is clear, but is a bit problematic in a more global context here.
Maybe “exponential modality” would be best!?
Doesn’t ’why not’ ’?’ also get called an exponential connective? And it’s a modality.
Re #6, #7: thanks for looking into this, Toby. I suggest though that we stick to (what I think is) the more familiar terminology, ’exponential modality’.
Re #8: this is the first I’ve heard anyone call an exponential connective; were you suggesting someone also calls an exponential connective? Or did you mean to say ’exponential modality’?
By the way: am I right that people here have begun to settle on ’modality’ being reserved for comonad-type thingies, calling monad-type thingies ’comodalities’? I just want to say that I think we should go ahead and call them both modalities. After all, the classical examples and were both called modalities or moad operators, even though they are De Morgan dual to each other. It would be handy to have a term that covers both cases (otherwise, we could just use comonad and monad, when we want to maintain a distinction).
I say “modality” for both and “co-modality” for definiteness when I find I need to emphasize that it’s a co-monad.
Todd, I say “modality” for both, for the same reason that you specify. If necessary to clarify I say “monadic modality” or “comonadic modality”. I would also like to leave open the possibility of modalties which are neither monads nor comonads.
Re #9, try Googling “exponential connective”. Maybe it’s not so odd if you remember negation is often called a (unary) connective.
My point was that we can’t use unadorned “exponential modality” for ! as we might have done with “exponential conjunction”. But “the exponential comonadic modality” is such a mouthful. You’d think there would be a way to say “the X” for !.
David, that was precisely my last point in #9. We can use “exponential modality” for (and people do use this term after all) under the permission that modality doesn’t have to mean a monad but can mean other things. Or, one could follow Urs in #10 and say “exponential comodality”, although I like this not as much.
In print, I see nothing wrong with just writing “the modality ” (or just for that matter). If I were to pronounce it aloud, I think I’d tend to say “bang”.
Why “bang”? To me that seems weird. But I may be missing some context.
In linear logic, ‘exponential modality’ is simply redundant; you might as well just say ‘exponential’. Both exponential operators (! and ?) are modalities (although one is monadic and one is comonadic). Besides conjunction and disjunction, you could distinguish them that way: as the monadic and comonadic modalities.
BTW, I agree with Mike #11 about the use of ‘modality’.
I agree with what Toby said in #16.
Maybe “exponential conjunction” is fine if it comes with an explanation of why it’s a reasonable terminology.
Heck, I’d prefer “conjunctive exponential” to “exponential conjunction”!! The latter just sounds goofy to my ears; I’m sorry.
Well, the comparison to true as a nullary conjunction is not really completely analogous: it’s not as if we have a conjunction of exponentially many things. In fact the word exponential is motivated by its expression in terms of an infinite disjunction of finite conjunctions. More appropriate from that perspective, I think, would be ’positive exponential’, to indicate that the conjunctions and disjunctions in the exponential are the positive ones.
By “conjunctive exponential”, I meant the exponential modality (as many call it, redundantly or not) that relates the multiplicative conjunction to the additive conjunction , aka the cartesian product.
(This is for anyone listening, but possibly also in response to Mike #20 in case he was talking to me. (-: )
Ah, right, there is also that other way to justify the word “exponential”. I was thinking of the expression
which I thought Toby was referring to in #6 — but I was misremembering the “&”s in it as being s. So I withdraw #20. I can see arguments for both “conjunctive exponential” and “exponential conjunction”.
There are three expressions (or expression schemas) like that listed currently (near the bottom) at linear logic; they are indeed what I was thinking of when I wrote #6. Todd's explanation, that , is maybe better.
1 to 23 of 23