I am new to this site and this question is certainly not research level - but oh well. I have a little background in software engineering and almost none in CSTheory, but I find it attractive. To make a long story short, I would like a more detailed answer to the following if this question is acceptable on this site.
So, I know that every recursive program has an iterative analog and I kind of understand the popular explanation that is offered for it by maintaining something similar to the "system stack" and pushing environment settings like return address etc. I find this kind of handwavy.
Being a little more concrete, I would like to (formally) see how does one prove this statement in cases where you have a function invoking chain $F_0 \rightarrow F_1 \ldots F_i \rightarrow F_{i+1} \ldots F_n \rightarrow F_0$. Further, what if there are some conditional statements which might lead an $F_i$ make a call to some $F_j$? That is, the potential function call graph has some strongly connected components.
I would like to know how can these situations be handled by let us say some recursive to iterative converter. And is the handwavy description I referred to earlier, really enough for this problem? I mean then why is it that I find removing recursion in some cases easy. In particular removing recursion from pre-order traversal of a Binary tree is really easy - its a standard interview question but removing recursion in case of post order has always been a nightmare for me.
What I am really asking is $2$ questions
(1) Is there really a more formal (convincing?) proof that recursion can be converted to iteration?
(2) If this theory is really out there, then why is it that I find, for eg, iteratizing preorder easier and postorder so hard? (other than my limited intelligence)