Comment by enricozb
4 years ago
Some related links (specifically that they perform "high school" algebra on types):
- Seven trees in one [0], a paper showing a bijection between binary trees and seven-tuples of binary trees.
- The algebra of algebraic data types [1] discusses Taylor expansions of data types.
- Differentiation of higher-order types [2] is commenting on OP's paper.
I used to be really interested in type theory, but haven't had as much time to explore it, but over the years I've saved these links (and the one posted).
[0]: https://arxiv.org/pdf/math/9405205.pdf
[1]: https://codewords.recurse.com/issues/three/algebra-and-calcu...
[2]: http://conal.net/blog/posts/differentiation-of-higher-order-...
Seven trees in one [0], a paper showing a bijection between binary trees and seven-tuples of binary trees.
Is this a surprising result? I am not quite interested enough to read through the paper in order to find out. Naively I would say, sounds maybe a bit fiddly, could have a clever trick to do elegantly, but does not sound too surprising or hard.
Build a complete binary tree with six nodes and attach the seven trees from the tuple as children. This is not a bijections as trees without the complete tree do not map back into any tuple of trees, so fiddle a bit with those six nodes to encode some special tuples or classes of tuples. Okay, now you have a new problem, two encodings for some tuples, so we have to also fiddle a bit with the trees before attaching them. Yeah, that could get fiddly...
It's definitely surprising, for a couple of reasons: 1. It isn't just the uninteresting result that the set of trees has the same cardinality as the set of 7-tuples of trees; the bijection here is given by a finite, non-looping program built out of `isEmpty : Tree -> Bool`, `getLeft : Tree -> Maybe Tree`, `getRight : Tree -> Maybe Tree`, and the constructors `empty : Tree` and `join : Tree x Tree -> Tree` 2. It isn't true for any number 1 < x < 7 3. In any case, why should it work out exactly? Why not "one tree can be encoded into seven trees, or one of these 13 remaining cases"?
The paper is quite good, but Dan Piponi has a great blog post that recasts the isomorphism as a game of "nuclear pennies", which is a fun puzzle to work out yourself: http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nu...
Nice puzzle. I found a 18 step solution but of course somebody posted one in the comments years ago.
Why not "one tree can be encoded into seven trees, or one of these 13 remaining cases"?
This direction is no problem, at least if we accept a graph with zero vertices as a tree which is probably non-standard as it should then have -1 edges. But if we allowed it, then a trivial mapping would be T -> (T,Ø,Ø,Ø,Ø,Ø,Ø). The other direction is much more problematic, one can easily map n trees into one, but then one gets stuck with either some trees that do not map back to any tuple or some tuples that have multiple representations. So now I am really curious what makes 7 special, so I will probably have to read the paper after all.
Why doesn't this work for x=2?
Let T denote the space of binary trees.
Any 2-tuple of trees (L, R) can be written as a binary tree with left node S and right node T, so we have an injection from T x T to T.
For the other direction we can embed a binary tree S as (S, {}) (with {} an empty binary tree).
By Schreuder-Bernstein there is a bijection between T and T x T.
1 reply →
Maybe Schroder-Bernstein could simplify. Easier to write 2 injections.
That theorem is not valid constructively, so no way to make a computer program out of it. I.e., there is no program that given types A, B and injections (f : A -> B) and (g : B -> A) produces a bijection A -> B.
1 reply →
But from reading the first bit of the paper I think they are talking about something stronger, not any bijection but one that only requires inspecting and manipulating a bounded number of layers of the trees.