I'm looking for a partial function $f$ from binary strings to natural numbers such that the following holds ($x$ and $y$ always represent binary strings, $\epsilon$ is the empty string, $H(x)$ is the Hamming weight of $x$, i.e. the number of $1$s): $$f(\epsilon)=1$$ $$f(x)>0 \implies f(x+1)=f(x)-1$$ $$x \in Dom(f) = (\nexists y,z :x=y+z,f(y)=0,z \neq \epsilon)$$ $$x\neq y,f(x)=f(y)\implies H(x) \neq H(y)$$ $$\forall n, \exists x: H(x)=n,f(x)=0$$
This function represents a command in a programming language that normally takes a single digit (all represented by $1$ in this function), but $0$ is an extending digit that lets the command take more digits instead. Just letting each $0$ increase the number of desired digits leads to multiple ways to represent the same string of digits, though, like $0011$ and $0101$, which both have $2$ actual accepted digits, when I'd like one of them to accept a different number of digits.
Description of rules:
- The function is 1 at the empty string (default to accepting a single digit).
- Appending a 1 to a string decreases the function by 1 if not already 0 (represents accepting a single digit)
- Any string with a prefix that produces the value 0 shouldn't be in the domain of the function $f$ (this represents a string reaching the correct number of 1s, so it stops accepting more digits), but all other strings should.
- No two different strings should have the same number of ones and the same value of the function, since then we can add $1$s to the end until both reach zero, and we reach the aforementioned redundant case of two strings accepting the same number of digits.
- We need to be able to end up with any number we'd like of accepted digits.
Optional: It shouldn't take more zeros to accept fewer ones (i.e. no $f(0)=3, f(00)=2$)
I'm just having trouble coming up with a solution that would provably work, since I can't just blindly iterate through all strings with the same number of ones and assign values, since previous values can invalidate future strings.
It looks like the following function $f$ satisfies the five conditions: $$ f(x) = \begin{cases} 1& \text{ if $x = \varepsilon$}\\ 0& \text{ if $x = 0^k1^{k+1}$ for some $k \geq 0$}\\ \text{undefined}&\text{otherwise} \end{cases} $$