Henry Spece has solved Challenge 7:
Henry’s proof is below:
The set of Tree objects is countable.
The following already proven theorems are used:
- The set of all strees is countably infinite.
- the set of all finite sequences of natural numbers is countable.
- The cartesian product of two countable sets is also countable.
- The sub-set of a countable set is countable.
We prove that the set of all trees with natural number labels is countable by finding a total injective mapping between the set of all trees and a set which is known to be countably infinite.
The set to which we are mapping the trees is the cartesian product of the set of finite sequences of natural numbers and the set of all strees. We already know that the set of all strees is countable, as well as the set of all finite sequences of natural numbers. Because the cartesian product of two countable sets is also countable, the cartesian product of these two sets must be countable, and a total injective mapping between the trees and this set would prove the set of all trees to also be countably infinite.
It is possible to imagine a mapping that links a tree to a stree, representing its structure, and a list of its labels, “in-order.” This is effectively “breaking apart” the tree into its components, resulting in two more manageable data types, or one element of the set defined above.
The function is defined more rigorously below, in two parts:
Part 1 (helper function):
getStree := tree -> stree getStree(null) = null getStree(combine(t1,N,t2)) = combine(getStree(t1),getStree(t2))
Part 2 (helper function):
getSequence := tree -> sequence getSequence(null) = empty sequence getSequence(combine(t1,N,t2)) = concatenate(getSequence(t1),N,getSequence(t2))
Combined (the relation being defined for the proof):
splitTree := tree -> (stree, sequence) splitTree(t) = (getStree(t),getSequence(t))
This relation is defined for all trees, making it total, and produces a unique stree-sequence combination for each tree, making it injective.
Because we have defined a total injective relation between the trees and another set which is known to be countable, the set of all trees must be countable.