Define a relation $\rhd$ by the deduction rules of figure \ref{trans}. By inspection, it is obvious that $(x\rhd y \wedge x \rhd z)\Rightarrow y=z$, so we are able to make the following definition.
\begin{definition}
Define a functional $\mathcal{F}: (INT \rightarrow INT)\rightarrow(INT \rightarrow INT)$:
$$
\mathcal{F}(f)(i) =
\begin{cases}
f(j)&\text{if $\exists j / i\rhd j$}\\
i&\text{else}
\end{cases}
$$
\end{definition}
Now, let $F: INT \rightarrow INT$ be the least fixed point of $\mathcal{F}$. $F$ is the \emph{Factor evaluator function}. It takes an interpreter and maps it to another
interpreter. If the resulting interpreter's call frame is $\bot$, evaluation completed
successfully; otherwise, at some stage of the computation, there was no applicable
inference rule (for example, a \texttt{drop} was attempted with an empty stack), in which case it is an error condition. In the case that the final call frame is non-empty, we abuse notation and say that $F(\delta,\rho,\chi)=\bot$.
Note that $F$ is a partial function, and it might not terminate; in this case, lets say $F(i)=\bot$.
\end{definition}
Now, I will give the first lemma. Intuitively, it states that if a quotation consumes $n$ elements from the stack, it does not ``see'' anything below. This forms the basis for the work in the next section.
\begin{lemma}\label{dipping}
Let $q\in QUOT$ be such that there exists $\delta\in STACK$ with $F(\delta,\bot,q)=(\delta\prime,\bot,\bot)$. Then for any $\delta_0\in STACK$,
Since $F(\delta,\bot,q)\ne\bot$ by assumption, each step of its transition chain has the
property that the data stack is either $\bot$ and no attempt is made to access its top
element, or the data stack is not $\bot$. Now notice that the same transition chain will
occur with $F(\delta\circ\delta_0,\bot,q)$; the only difference being that when the data stack would become $\bot$ in the former, it would become $\delta_0$ in the latter. But since no attempt is made to access the top stack element, both transition chains are equivalent up to the appending of $\delta_0$. Therefore $F(\delta\circ\delta_0,\bot,q)=(\delta\prime\circ\delta_0,\bot,\bot)$.
\end{proof}
\section{Stack effects}
Now, I will study the effect of evaluation on the data stack in detail. The primary motivation, and
eventual goal, is to be able to statically deduce the number of input and output parameters
of a quotation on the stack.
\begin{definition} Let $q \in QUOT$ be a program fragment. The \emph{stack effect} of $q$, denoted $[q]$, is $(m,n)\in\mathbb{Z}^+\times\mathbb{Z}^+$ iff the following conditions hold:
\begin{enumerate}
\item If $\leng(\delta)=m$, $(F(\delta,\bot,q)=(\delta\prime,\bot,\bot))\Rightarrow(\leng(\delta\prime)=n)$.
\item If $l<m$, there exists a data stack $\delta$ with $\leng(\delta)=l$ such that $F(\delta,\bot,q)=\bot$.
\end{enumerate}
Note that if for all data stacks $\delta$, we have $F(\delta,\bot,q)=\bot$, the stack effect can be stated to be any pair $(m,n)$. This does not cause a problem in practice.
\end{definition}
The following result is intuitively obvious; the stack effect of a literal object is to increase the number of elements on the stack by one.
\begin{lemma}
For $o \in LIT$, $[o]=(0,1)$.
\end{lemma}
\begin{proof}
By the transition rule \{Literal\}, we have:
$$F(\bot,\bot,(o))=((o),\bot,\bot)$$
By definition if the length function, it follows that:
$$\leng((o))=1+\leng(\bot)=1$$
Since 0 is the smallest possible choice of $n$, the second condition on the definition of a
stack effect is automatically satisfied.
\end{proof}
\begin{definition} The \emph{composition of stack effects}$(a,b), (c,d)\in\mathbb{Z}^+\times\mathbb{Z}^+$ is defined and denoted as follows:
The reason we define the above operation becomes clear with the following theorem.
It actually does represent composition of stack effects.
\begin{theorem}\label{iso}
For $p,q \in QUOT$, $[p\circ q]=[p]\otimes[q]$.
\end{theorem}
\begin{proof}
Let $[p]=(a,b)$, $[q]=(c,d)$.
If for all $\delta$, $F(\delta,\bot,p\circ q)=\bot$, then the stack effect of $p\circ q$ is vacuously $(a,b)\otimes(c,d)$. So assume that there exists a stack $\delta$ such that $F(\delta,\bot,p\circ q)=(\delta\prime,\bot,\bot)$ for some $\delta\prime$.
Now, consider two cases.
\begin{enumerate}
\item$c<b$. Let $\delta$ be such that $\leng(\delta)=a$ and $F(\delta,\bot,p)=(\delta\prime,\bot,\bot)$. Then $\leng(\delta\prime)=b$.
By assumption, $F(\delta\prime,\bot,q)\ne\bot$. So by \ref{dipping},
$F(\delta\prime,\bot,q)=(\delta\prime\prime,\bot,\bot)$ where $\leng(\delta\prime\prime)=\leng(\delta\prime)+b-c$.
\item$c\geq b$. p takes a, leaves b, q takes c-b more then and leaves c-b+d by \ref{dipping}.
\end{enumerate}
In both cases, we have that $[p\circ q]=(a +\max(0,c-b),d +\max(0,b-c))$.
\end{proof}
\begin{lemma}
Stack effect composition has an equal left and right identity, and is associative:
\begin{enumerate}
\item For all $(a,b)\in\mathbb{Z}^+\times\mathbb{Z}^+$, $(a,b)\otimes(0,0)=(0,0)\otimes(a,b)=(a,b)$.
\item For all $x,y,z \in\mathbb{Z}^+\times\mathbb{Z}^+$, $x\otimes(y\otimes z)=(x\otimes y)\otimes z$.
The second follows from the associativity of the concatenation operator $\circ$. Given stack effects $x,y,z$, let $X,Y,Z \in QUOT$ be quotations whose stack effects are $x,y,z$, respectively. Then by the previous theorem we have:
