HackerPapers

arXiv:math/9405205math.LO

Seven Trees in One

Andreas Blass

Abstract

Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set T of finite binary trees and the set T^7 of seven-tuples of such trees. "Particularly elementary" means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to X=1+X^2. Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.

arXiv comments
Version 2 has the same content as version 1 but improved formatting. The last line or two of each page will no longer be deleted
Journal reference
Journal of Pure and Applied Algebra 103 (1995) 1-21
DOI
Subjects
math.LOLogic

On Hacker News

Linked by 5 identifiable commenters in 5 comments across 5 threads, from Jun 2015 to May 2024.

Comments linking this paper, per year.

Discussed in comments5 threads

  1. Grothendieck’s use of equality 1 comment

    • The connection between type isomorphisms and algebraic equalities is known and explored in a variety of interesting ways. I don't know the precise history of the development of the notation and vocabulary, but there's a reason types like A+B are notated with a plus symbol and…

      cvossView on HNParent context

  2. The Derivative of a Regular Type is its Type of One-Hole Contexts (2001) [pdf] 1 comment

    • 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.…

      enricozbView on HNParent context

  3. Calculus with types 1 comment

    • A very nice fact that I coincidentally learned just yesterday, which is not in the linked answer but is touched on in one of the comments and in an edit on the accepted answer: there is an explicit bijection that maps a binary tree to seven binary trees (and vice-versa, by the…

      svatView on HNParent context

  4. Representing Graphs by Knuth Trees (1974) [pdf] 1 comment

    • If you like that then you are going to love this: "Seven Trees in One" by Andreas Blass. https://arxiv.org/abs/math/9405205

      mathgeniusView on HNParent context

  5. The Algebra of Algebraic data types 1 comment

    • A few remarks on this stuff. 1. Very closely related is the pure-mathematical technique of generating functions, where you take a sequence (let's say the Fibonacci sequence 0,1,1,2,3,5,8,13,...) and use its elements as coefficients in a power series…

      gjm11View on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.