One can compress data with straight-line grammars. An algorithm that employs this technique is called Sequitur. If I understood correctly, Sequitur basically starts with one rule representing the input and then does these three steps till the grammar does not change anymore:For each rule, try to find any sequences of symbols in any other rule that match the rule's right hand side and replace these sequences by the rules left hand side.For each pair of adjacent symbols in any right hand side, find all non-overlapping other pairs of adjacent symbols that are equal to the original pair. If there are any other pairs, add a new nonterminal, replace all occurrences of these pairs by the new nonterminal and add a new rule that defines the nonterminal.For each nonterminal that appears exactly once on all right-hand sides of all rules, replace its occurrence by its definition, remove the nonterminal and the rule that defines it.For each (non-empty) input, can one guarantee that the above algorithm terminates?
Will this algorithm terminate on any input?
algorithms;algorithm analysis;formal grammars;data compression;correctness proof