Abstract machine

An abstract machine specifies a computational state and rules for advancing that state without requiring one particular physical implementation. A Turing machine and a stack machine give different ways to organize the state and its transitions.

A computational model with an internal state and transition rule, together with an initial state and optional observation and stopping functions. The state space need not be finite; a finite-state machine is the special case with finitely many states. A trace records observations along transitions. An interface providing only reset, update, stopping and observation operations does not by itself provide copying or rollback; a trace iterator can revisit saved observations without reversing machine effects.

A configuration of a system at one moment. In a transition system, a state is an element of its state space $S$, and a transition relation specifies permitted changes of state.

An execution model whose instructions obtain operands from a stack and put results back on that stack.

Code whose operand-producing instructions precede the instruction that consumes those operands. A stack machine can translate a binary program expression by producing its left operand, producing its right operand, and then applying the operation to the two top values.

Suppose each subtree of a binary expression tree is evaluated completely before its sibling, leaves one result on an operand stack, and is not spilled or interleaved. If the child depths are $p,q$, evaluating the first child needs $p$ slots and keeping its result while evaluating the second needs $1+q$. Reversing the order gives $\max (q,1+p)$. If either order preserves the expression's meaning, the minimum is $\max (p,q)$ when $p\ne q$ and $p+1$ when $p=q$. For example, if $p>q$, integrality gives $p\ge q+1$, so evaluating the deeper child first attains the lower bound $p$. If $p=q$, the second child needs its own $p$ slots plus one saved result regardless of order. Induction over the binary expression tree proves optimality in this evaluation model.

For a noncommutative operator, an instruction swapping the top two stack entries or a reverse-operand opcode permits the same ordering while preserving operand positions. Reordering still requires absence of order-sensitive side effects. Reassociation and interleaving are separate transformations and are not part of this optimality claim.