In executable Haskell, the algebraic data type declaration uses This is a preorder traversal of a full binary tree, including the leaves. Structural induction proves correctness: the leaf of a rooted tree case has precisely one output, and the fork case concatenates the correct preorder traversals of its two subtrees after its own marker.
data, rather than the printed type. A leaf of a rooted tree contributes False; a fork contributes True followed by its left and right subtrees in that order.data Tree = Leaf | Fork Tree Tree
preorder :: Tree -> [Bool]
preorder Leaf = [False]
preorder (Fork l r) = True : (preorder l ++ preorder r)An equivalent version avoids repeatedly copying the left list through list concatenation:Its strengthening is
preorder t = walk t []
where
walk Leaf rest = False : rest
walk (Fork l r) rest = True : walk l (walk r rest)walk t rest = preorder t ++ rest. Each vertex constructs one list cell, so this version has linear time complexity. The concise result isFor parts (b)–(e), use array indices as tree handles. This also makes the shared storage in part (d) type-correct: both pending handles and output markers occupy integer cells. Zero denotes a leaf of a rooted tree; a positive handle denotes a fork whose children are in Initialize
nodes[t-1]. Only finite acyclic structures are admitted. An allocated fork's children are themselves valid handles.CONST MaxForks = 100000;
TYPE Tree = INTEGER;
Node = RECORD left, right: Tree END;
Arena = ARRAY MaxForks OF Node;
VAR nodes: Arena;
used: INTEGER;
PROCEDURE NewFork(left, right: Tree): Tree;
BEGIN
ASSERT(used < MaxForks);
nodes[used].left := left; nodes[used].right := right;
INC(used);
RETURN used
END NewFork;
PROCEDURE Preorder(t: Tree; VAR out: ARRAY OF INTEGER;
VAR count: INTEGER);
PROCEDURE Visit(p: Tree);
BEGIN
IF p = 0 THEN
out[count] := 0; INC(count)
ELSE
out[count] := 1; INC(count);
Visit(nodes[p-1].left); Visit(nodes[p-1].right)
END
END Visit;
BEGIN
count := 0; Visit(t)
END Preorder;used := 0 before constructing any trees; NewFork allocates within this arena. The fixed capacity is an implementation parameter and may be replaced by a dynamically allocated arena. The returned prefix out[0..count) encodes Boolean values by and . This encoding is part of the chosen representation, not a conversion of a pointer into a Boolean value.The recursion invariant is that
Visit(p) appends exactly the preorder traversal of the subtree represented by p. If the full binary tree has forks, it has leaves; henceEach occurrence is visited once, using linear time complexity and a call stack bounded by the height of a binary tree. The arena is the input representation, not an extra copy made by the traversal.Use an explicit stack of handles. Push the right subtree first, so that the left subtree is removed first by the LIFO stack.The loop invariant says that the already written prefix, followed by the preorder traversals of the pending subtrees in top-to-bottom stack order, equals the entire required output. Popping a leaf of a rooted tree transfers one marker to the prefix. Popping a fork transfers its marker and replaces its remaining work by left then right subtree work. Both preserve the loop invariant. The number of as-yet-unwritten vertices decreases by one per iteration, proving termination.The time complexity is linear in the output length. The maximum stack size is at most one plus the height of a binary tree.
PROCEDURE PreorderIter(t: Tree; VAR out: ARRAY OF INTEGER;
VAR count: INTEGER;
VAR stack: ARRAY OF Tree);
VAR top: INTEGER; p: Tree;
BEGIN
count := 0; top := 1; stack[0] := t;
WHILE top > 0 DO
DEC(top); p := stack[top];
IF p = 0 THEN
out[count] := 0; INC(count)
ELSE
out[count] := 1; INC(count);
stack[top] := nodes[p-1].right; INC(top);
stack[top] := nodes[p-1].left; INC(top)
END
END
END PreorderIter;Let be the final output length, the number of emitted markers, and the number of pending handles. Each pending subtree contributes at least one future marker, soStore output from the low end and the stack from the high end of the same array. A pop frees one cell before the next write. For a fork, the two pushed children each account for at least one of the remaining markers. Thus the two regions never overlap.The loop invariant includes
PROCEDURE PreorderShared(t: Tree; VAR out: ARRAY OF INTEGER;
VAR count: INTEGER);
VAR top, cap: INTEGER; p: Tree;
BEGIN
cap := LEN(out); count := 0;
top := cap-1; out[top] := t;
WHILE top < cap DO
p := out[top]; INC(top);
IF p = 0 THEN
out[count] := 0; INC(count)
ELSE
out[count] := 1; INC(count);
DEC(top); out[top] := nodes[p-1].right;
DEC(top); out[top] := nodes[p-1].left
END
END
END PreorderShared;count <= top, with pending handles in out[top..cap) and final markers in out[0..count). The preceding accounting proves every intermediate write also respects array bounds. This uses the integer handle representation chosen in part (b). Simply putting a pointer into a genuinely Boolean-typed cell would not be valid Oberon.Maintain a cursor to the first unread marker. A fork consumes its own marker and then two complete encodings, in left-to-right order.Start with
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;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 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 isThe time complexity is linear in the encoding length, with call stack space bounded by the height of a binary tree.
Articles by others on the same topic
There are currently no matching articles.