= Solution
Maintain a cursor to the first unread marker. A fork consumes its own marker and then two complete encodings, in left-to-right order.
``
PROCEDURE Decode(VAR code: ARRAY OF INTEGER;
VAR pos: INTEGER): Tree;
VAR marker: INTEGER; left, right: Tree;
BEGIN
marker := code[pos]; INC(pos);
IF marker = 0 THEN RETURN 0 END;
ASSERT(marker = 1);
left := Decode(code, pos);
right := Decode(code, pos);
RETURN NewFork(left, right)
END Decode;
``
Start with `pos := 0; t := Decode(code, pos)`, with sufficient unused arena space. The valid-input <precondition> ensures that every read exists and every fork has two encoded <subtrees>. Evaluating the two recursive calls in separate statements fixes their order.
<Structural induction> shows that decoding $P(t)$ reconstructs the same <binary tree> shape and leaves the cursor just after its encoding. The <tree> handles need not coincide with the original handles: the abstract <tree> does. The result is
$$
\boxed{\operatorname{Decode}(P(t))\cong t,\quad\mathrm{pos}=|P(t)|.}
$$
The <time complexity> is linear in the encoding length, with <call stack> space bounded by the <height of a binary tree>.
Back to article page
