Your conversion doesn't address determining the length of the output. Another conversion avoids that issue, by converting a polynomial time function f into the

Your conversion doesn't address determining the length of the output. Another conversion avoids that issue, by converting a polynomial time function f into the language L_f = { (x,y): f(x) < y}, where < compares strings lexicographically "" < "0" < "1" < "00" ... Given a decider for L_f and an input x it's easy to determine |f(x)| and next f(x) by binary search.