# How to prove a function is a bijection (name mangling)?

I'm writing a compiler for a subset of Java, which does not permit overloading (but it does permit overriding). Static functions outside of main are not allowed.

We're guaranteed class names are unique and method names within each class are unique.

I want to mangle the names in such a way that there will never be overlap when I map them to procedures at a lower level:

Here's my proposal:

_(ClassNameLength)ClassName(MethodNameLength)MethodName


I believe this works, and it allows me to define auxilary functions so long as they do not start with _.

How can I prove it works and is a bijection in all cases?

• 1. Why would you care for surjectivity? 2. Injectivity shouldn't be hard to prove. Take two classname/methodname pairs that are different. Case 1: the classnames are different. Then your mangled names have different prefixes. Case 2: the classnames are the same but the methodnames differ. Then the suffixes of the mangled names are different.
– Kai
Commented Apr 28 at 2:50
• You could make that same argument for a mangling scheme like _ClassName_MethodName but that mangling scheme doesn't work @Kai Commented Apr 28 at 3:21
• No, the same argument would not work. You'd fail to prove that ("a_b", "c") and ("a", "b_c") have different prefixes because they both mangle to "_a_b_c".
– Kai
Commented Apr 28 at 6:09
• And btw, you can simplify the mangling scheme to (c,m) $\to$ _(|c|)cm because |m|, the length of the method name, is not needed for the properties you listed.
– Kai
Commented Apr 28 at 6:20
• @Kai could you give the proof? I’m simply interested to see how it’s done. Commented Apr 28 at 16:53

Let $$\Sigma$$ be an alphabet including underscore, decimal digits, letters, and parentheses (e.g. the printable ASCII characters). Define a mangling function $$f:(\Sigma^* \times \Sigma^*) \to \Sigma^*$$ by $$f(a,b) = \mathtt{\_(}|a|\mathtt{)}a\mathtt{(}|b|\mathtt{)}b$$, where $$|.|$$ maps a string to the decimal representation of its length.

Claim: $$f$$ is injective.

Proof: Let $$c, d, m, n \in \Sigma^*$$ such that $$(c,m) \neq (d,n)$$. We proceed by case analysis on the cause of that inequality.

1. Case $$c\neq d$$
1. Case $$c$$ and $$d$$ have different lengths: Then the prefix of $$f(c,m)$$ matching the regular expression _([0-9]+) is different to that of $$f(d,n)$$. Neither is a prefix of the other.
2. Case $$c$$ and $$d$$ have the same length: Then $$\mathtt{\_(}|c|\mathtt{)}c$$ and $$\mathtt{\_(}|d|\mathtt{)}d$$ have the same length (and agree on the prefix matched in the previous case) but are still different because $$c\neq d$$.

In both sub-cases, we obtain different prefixes of the mangling function results that aren't prefixes of each other. Nothing can be appended to them to create identical strings.

1. Case $$c = d$$ and $$m \neq n$$: Then $$\mathtt{\_(}|m|\mathtt{)}m \neq \mathtt{\_(}|n|\mathtt{)}n$$. The two results of applying the mangling function agree on the first part but the second parts are different.

We conclude that $$f(c,m) \neq f(d,n)$$.

PS: This proof also works for the simpler mangling function I suggested in the comment above.

PPS: For the bogus mangling scheme $$f'(a,b) = \mathtt{\_}a\mathtt{\_}b$$ only Case 1.1. fails because it is impossible to establish the crucial property that "Neither [of $$\mathtt{\_}c$$ and $$\mathtt{\_}d$$] is a prefix of the other".

• How exactly would this proof fail for _<class>_<method>? I know the counterexamples, but I don't see how the proof would fail. Case 1: different prefixes Case 2: same prefixes, different endings Commented May 4 at 20:02