You have a classical string P. We like to cooperate across worldviews or whatever, so we provide sprinkleNegations to sprinkle double negations on classical strings and decorateWithBox to decorate provability on intuitionistic strings.
The definition of inverse would be cool, but you see that decorateWithBox(sprinkleNegations(P)) = P isn’t really there, because now you have all these annoying symbols (which cancel out if we implemented translations correctly, but how would we know that?). Luckily, we know we can automate cancelation with an evaluator / normalization--- normalize(decorateWithBox(sprinkleNegations(P))) = P is a trivial syntactic string equality, which is close enough to the definition of inverse.
I think Alice and Bob, socially, care a lot simply about the costs of normalizing to the input after the translations are applied. If it’s an expensive application, they’re going to struggle to connect. If not, they’ll enjoy the benefits of invertable translations.
I’ve seen a lot of attempts to provide “translations” from one domain-specific computer language to another, and they almost always have at least one of these properties:
They aren’t invertible, nor “almost invertible” via normalization
They rely on an extension mechanism intentionally allowing the embedding of arbitrary data into the target language
They use hacks (structured comments, or even uglier encodings if there aren’t any comments) to embed arbitrary data
They require the source of the translation to be normalized before (and sometimes also after, but always before) translation
(2) and (3) I don’t think are super great here. If there are blobs of data in the translated version that I can’t understand, but that are necessary for the original sender to interpret the statement, it isn’t clear how I can manipulate the translated version while keeping all the blobs correct. Plus, as the recipient, I don’t really want to be responsible for safely maintaining and manipulating these blobs.
(1) is clearly unworkable (if there’s no way to translate back into the original language, there can’t be a conversation). That leaves 4. 4 requires stripping anything that can’t be represented in an invertible way before translating. E.g., if I have lists but you can only understand sets, and assuming no nesting, I may need to sort my list and remove duplicates from it as part of normalization. This deletes real information! It’s information that the other language isn’t prepared to handle, so it needs to be removed before sending. This is better than sending the information in a way that the other party won’t preserve even when performing only operations they consider valid.
I think this applies to the example from the post, too—how would I know whether certain instances of double negation or provability were artifacts that normalization is supposed to strip, or just places where someone wanted to make a statement about double negation or provability?
My summary translation:
You have a classical string
P. We like to cooperate across worldviews or whatever, so we providesprinkleNegationsto sprinkle double negations on classical strings anddecorateWithBoxto decorate provability on intuitionistic strings.The definition of inverse would be cool, but you see that
decorateWithBox(sprinkleNegations(P)) = Pisn’t really there, because now you have all these annoying symbols (which cancel out if we implemented translations correctly, but how would we know that?). Luckily, we know we can automate cancelation with an evaluator / normalization---normalize(decorateWithBox(sprinkleNegations(P))) = Pis a trivial syntactic string equality, which is close enough to the definition of inverse.I think Alice and Bob, socially, care a lot simply about the costs of normalizing to the input after the translations are applied. If it’s an expensive application, they’re going to struggle to connect. If not, they’ll enjoy the benefits of invertable translations.
I’ve seen a lot of attempts to provide “translations” from one domain-specific computer language to another, and they almost always have at least one of these properties:
They aren’t invertible, nor “almost invertible” via normalization
They rely on an extension mechanism intentionally allowing the embedding of arbitrary data into the target language
They use hacks (structured comments, or even uglier encodings if there aren’t any comments) to embed arbitrary data
They require the source of the translation to be normalized before (and sometimes also after, but always before) translation
(2) and (3) I don’t think are super great here. If there are blobs of data in the translated version that I can’t understand, but that are necessary for the original sender to interpret the statement, it isn’t clear how I can manipulate the translated version while keeping all the blobs correct. Plus, as the recipient, I don’t really want to be responsible for safely maintaining and manipulating these blobs.
(1) is clearly unworkable (if there’s no way to translate back into the original language, there can’t be a conversation). That leaves 4. 4 requires stripping anything that can’t be represented in an invertible way before translating. E.g., if I have lists but you can only understand sets, and assuming no nesting, I may need to sort my list and remove duplicates from it as part of normalization. This deletes real information! It’s information that the other language isn’t prepared to handle, so it needs to be removed before sending. This is better than sending the information in a way that the other party won’t preserve even when performing only operations they consider valid.
I think this applies to the example from the post, too—how would I know whether certain instances of double negation or provability were artifacts that normalization is supposed to strip, or just places where someone wanted to make a statement about double negation or provability?