Tree is a type constructor, taking the element type parameter a to the algebraic data type Tree a. It is not a value and has no ordinary value-level function type; its kind of a type is * -> *. The other names are data constructors with polymorphic type signatures:
One :: a -> Tree a
Two :: Tree a -> Tree a -> Tree a
One constructs a leaf-labelled binary tree with one leaf; Two joins two such trees under a new internal node. Unlike a general binary tree representation with empty child slots, this representation has no empty tree.[ref]
Count each data constructor once, including each Two:
size :: Tree a -> Int
size (One _)   = 1
size (Two l r) = 1 + size l + size r
Structural induction verifies the count: a leaf contributes one; an internal node contributes itself and the disjoint occurrences in its two subtrees. Fully evaluating the result takes linear time in the number of nodes. This type signature uses machine Int as usual in the examination; Integer avoids overflow for arbitrarily large inputs.
The natural tree fold replaces each data constructor by the supplied operation:
fold :: (a -> b) -> (b -> b -> b) -> Tree a -> b
fold one two (One x)   = one x
fold one two (Two l r) = two (fold one two l) (fold one two r)
Its reconstruction identity is fold One Two = id. More generally a function h equals fold one two on finite trees exactly when h (One x) = one x and h (Two l r) = two (h l) (h r). These equations determine the result by structural induction, expressing why this is the natural structural recursion for this datatype.
Replace the leaf data constructor by the constant one and the internal data constructor by addition with one extra node:
size :: Tree a -> Int
size = fold (const 1) (\m n -> 1 + m + n)
The two defining equations of the tree fold become exactly the two equations for the recursive node count.
Emit the root subtree first, then the occurrences inside its children:
subs :: Tree a -> [Tree a]
subs t@(One _)   = [t]
subs t@(Two l r) = t : (subs l ++ subs r)
This is a preorder traversal of subtree occurrences. Equal-valued occurrences are retained: the answer is a list, not a deduplicated set. Every occurrence is either the root or lies in exactly one child, which proves completeness by structural induction.
The head of each recursively obtained list is the original child. Hence the tree fold has retained enough information to reconstruct the parent:
subs :: Tree a -> [Tree a]
subs = fold (\x -> [One x]) combine
  where
    combine ls rs = Two (head ls) (head rs) : (ls ++ rs)
The invariant is that every folded result is nonempty and begins with the subtree being folded. It holds at One; the displayed combining operation preserves it at Two. Thus neither use of head encounters an empty list, and the remaining entries agree with the recursive preorder traversal.
Include each child itself, followed by its proper subtrees, while excluding the current root:
proper :: Tree a -> [Tree a]
proper (One _)   = []
proper (Two l r) = (l : proper l) ++ (r : proper r)
Again, occurrences matter: a child with the same value as another child is not removed. The definition is a structural recursion, but its right-hand side uses the original children as well as their recursively computed results.
Suppose that a direct tree fold with result type [Tree a] implements proper, so proper = fold one two. Every leaf has result [], hence one x = [] for every label x. Consequently proper (Two (One x) (One y)) would always equal two [] [], independently of either label. Taking labels from Bool, the inputs Two (One False) (One False) and Two (One True) (One False) would therefore have equal results. Their correct results are [One False, One False] and [One True, One False], which differ. This is a contradiction.
There is no direct fold with only the proper-subtree list as its recursive summary. This is the direct tree-fold information obstruction: replacing both children by equal summaries prevents the parent operation from recovering their different labels. The claim must not be extended to every expression containing a tree fold. A fold retaining the original tree alongside its proper-subtree list, followed by projection, does work; alternatively tail . subs uses the richer fold from part (f).

Ancestors (10)

  1. Functional programming, design and analysis of algorithms
  2. 2018
  3. Past exam of the year 1 of the computer science course of the University of Oxford
  4. Year 1 of the computer science course of the University of Oxford
  5. Computer science course of the University of Oxford
  6. Undergraduate course of the University of Oxford
  7. Course of the University of Oxford
  8. University of Oxford
  9. List of universities
  10. Home

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version