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?
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?