I'm not sure actually! In hindsight I could have been using the term ‘later modality’ imprecisely… I *think* box and diamond can take on different meanings depending on your perspective? Far from an expert, alas.
Conversation
I usually ask for help when I over-extend myself in thinking about modal logic, and it's usually I'm speaking nonsense. I guess I was more thinking ‘later’ in the sense of ‘I have this modal operator for code that will be compiled later’, but that could be wrong.
1
2
My understanding is that there are many modal logics, each using ☐ and/or ◇ (and/or sometimes ◯) to mean different things. By social convention, in all of them ☐A -> A but not the converse, otherwise ☐ is a poor choice of name for whatever concept that logic models.
2
3
Modal logics like K, KD, KB, K4, don't have []A -> A (or the converse). One way to think of it: []A says that A is required. But not all kinds of requirements are always met!
1
2
In this diagram, a modal logic includes []A -> A iff it has a path from it to T
read image description
ALT
1
3
I tend to think of the box/diamond divide as more closely related to conjunction and disjunction: for a modal operator O, having O(A & B) <-> (OA & OB) is a box-like quality, and having O(A v B) <-> OA v OB is a diamond-like quality
1
2
I need to think about this more, and try to translate it into examples I know from programming, but this seems like a very useful way of thinking about it. Thanks so much!
1
2
Seems like Rust's references can't go in the opposite direction of the iff, as you'd need to return a reference to a temporary variable! :( play.rust-lang.org/?version=stabl
1
2
I'd I'm reading that right, you've got O(A & B) -> (OA & OB) and O(A v B) -> (OA v OB) both, but neither converse. Is that right?
1
Correct!
1
1
To elaborate on why the inverse breaks, Rust allows you to return references to data behind a reference you passed as an argument, but you can't:
- package some referenced data inside another reference without copying
- return reference to temporary memory
Hmm. Then I don't know of any modal logic that exhibits this kind of behaviour! Maybe or or or does?
1
4
It could also be that I'm looking in the wrong place for modal stuff in Rust though. Or that this approach is a wrong fit entirely. I'll have more of a think. Then there's also interesting stuff wrt. unique references and uniqueness that I still don't understand…
1
3
Show replies