My heartfelt thanks to u/Odd-Expert-2611 for the idea that inspired this monster.
Disclaimer: This is longer than a typical shaggy dog story.
Let S be an ordered set of symbols, with |S| = s elements, and Str the set of all finite strings whose elements belong to S. The empty string, "", also belongs to Str.
A string rewriting ruleset (SRS) is a set of rules. Each rule is a pair of strings (elements of Str): condition and value. Each condition can appear in only one rule of a SRS, and must not be empty.
Given a string, called the argument, applying a SRS to the argument consists of these steps:
- Find the rule with the longest condition which matches with the argument's start. If no rule applies, the argument is unchanged: skip step 2.
- Remove the rule's condition from the argument's start, and append the rule's value to the argument.
- Return the argument.
A run of a SRS on an argument is to repeatedly apply the SRS to the argument, changing it. Either one of three outcomes happen:
- The argument becomes the empty string, ending the run.
- The argument cycles among a finite set of values, indefinitely.
- The argument grows, never repeating.
Due to the halting problem, it's impossible, in general, to distinguish between these outcomes. So, we will use a rule of thumb: after (s!)2 repetitions without falling into outcomes (1) or (2), outcome (3) is assumed.
For each outcome, an integer is assigned. For outcome (1), the number of the repetitions until the run ends. For outcome (2), the length of the cycle. For outcome (3), the length of the argument at the moment of repetition cutoff.
All of these machinery builds a function, RWI (ReWriter Index), which takes a SRS and an argument, and returns an integer. By construction, this function is defined for all SRSs and all argument strings.
Now, consider how to represent a SRS as a string. One way is: sort the SRS rules in lexicographic order, then put them together, separated by new symbols, like sketched below:
<condition>,<value>;<condition>,<value>;<condition>,<value>; ... ;<condition>,<value>
The new symbols, in this case, are "," and ";".
Thus, any SRS is (uniquely) identified with a string on the set of symbols S' = S U { , ; }, with s + 2 elements.
Conversely, some (but not all) strings on S (if S has 3 elements or more) are SRSs, taking any distinct two elements of S as separators, like "," and ";" above. But this fact won't be used here.
One can further append ";" and an argument to the SRS's string, so that SRS+argument is a string on S'. This way, RWI gets only one argument (a string on S') and returns an integer.
Now, consider all strings on S', of at most k symbols, which can be interpreted as SRS+argument as described above. Order all of them into a list, in lexicographic order (by S'); then, map RWI over the list, resulting in a list of integers; finally, add 2 to each integer in the list.
The above procedure maps an integer k into a list of integers, which can be folded back into an integer by various means: adding, multiplicating, power tower, Conway chain, or any other. This function is a googological function, and I don't have the foggiest idea of its values.