By the Curry-Howard Isomorphism, constructive proofs correspond to functions (from correlates of assumptions to correlates of conclusions) - and an alternate proof often corresponds to an alternate function.
The Schroeder-Bernstein construction works for sets in general. But sets of concrete things such as emails are always at most countably infinite. So there's an alternative proof. You can compose the two bijections - quoted emails to integers and then from integers to unquoted emails. This is nonconstructive because I haven't pinned down what those (Godel numbering) bijections actually are, but it might look like a complete mess.
The 103...496th possible email not containing a specific byte sequence ("\nFrom" or whatever) might not have much superficial visual similarity to the 103...496th possible email when that byte sequence is allowed.
Indeed, there's no shortage of ways to show that two countably infinite sets are bijectable to one another. What strikes me as interesting (apart from the match of surnames) is that one reasonably natural way for a mathematician to do it (applying a theorem which happens to be more general than needed) also gives rise to a method of quoting which is not merely plausible for practical use but actually in use.
Of course, there's no need in general for the transformation from a string to its quoted form to be bijective, or even to be a function (by which I mean 'single-valued'). There are plenty of practical reasons why you might want to have some strings not be legal in the quoting syntax even though they aren't among the set of strings you really needed to avoid, or why you might want to provide multiple equivalent ways to quote the same thing (e.g. \042 vs \x22 vs \" in C string literals). Bijectivity is desirable only because it correlates with space-efficiency, and only as long as it doesn't introduce any other inconveniences. For instance, the qmail-style mbox quoting transform could have been replaced by simply prefixing every non-separator line with a > sign, but that wastes more space for a reason not totally unconnected to its non-bijectivity.
So the Gödel-numbering approach probably would be too inconvenient to be worth the space saving, if it didn't turn out to reduce to anything more easily stated!
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
The Schroeder-Bernstein construction works for sets in general. But sets of concrete things such as emails are always at most countably infinite. So there's an alternative proof. You can compose the two bijections - quoted emails to integers and then from integers to unquoted emails. This is nonconstructive because I haven't pinned down what those (Godel numbering) bijections actually are, but it might look like a complete mess.
The 103...496th possible email not containing a specific byte sequence ("\nFrom" or whatever) might not have much superficial visual similarity to the 103...496th possible email when that byte sequence is allowed.
Of course, there's no need in general for the transformation from a string to its quoted form to be bijective, or even to be a function (by which I mean 'single-valued'). There are plenty of practical reasons why you might want to have some strings not be legal in the quoting syntax even though they aren't among the set of strings you really needed to avoid, or why you might want to provide multiple equivalent ways to quote the same thing (e.g.
\042vs\x22vs\"in C string literals). Bijectivity is desirable only because it correlates with space-efficiency, and only as long as it doesn't introduce any other inconveniences. For instance, the qmail-style mbox quoting transform could have been replaced by simply prefixing every non-separator line with a > sign, but that wastes more space for a reason not totally unconnected to its non-bijectivity.So the Gödel-numbering approach probably would be too inconvenient to be worth the space saving, if it didn't turn out to reduce to anything more easily stated!