Suponha que tenhamos uma especificação gramatical simples. Existe uma maneira de enumerar os termos dessa gramática que garante que qualquer termo finito terá uma posição finita,iterando-o na diagonal. Por exemplo, para a seguinte gramática:

S      ::= add
add    ::= mul | add + mul
mul    ::= term | mul * term
term   ::= number | ( S )
number ::= digit | digit number
digit  ::= 0 | 1 | ... | 9

Você pode enumerar termos assim:

0
1
0+0
0*0
0+1
(0)
1+0
0*1
0+0*0
00
... etc

Minha pergunta é: existe uma maneira de fazer o oposto? Ou seja, para usar um termo válido dessa gramática, digamos,0+0*0e encontra sua posição sobre essa enumeração - nesse caso, 9?