Lovelier than a poem

Stream: maths

[Alex Meiburg]

Just for fun!

I was curious if anyone has an inventory of the various things that have been meant by "tree", in math/cs literature. (This was prompted in part by needing a "tree" notion in Mathlib and finding that neither Tree nor IsTree were what I wanted :) ) To start the list off, I have definitely seen "tree" to mean:

• Acyclic, connected simple graph. (This is Mathlib's IsTree)
• Acyclic, connected, locally finite, simple graph. IsTree+LocallyFinite.
• Acyclic, connected, finite, simple graph. IsTree+Fintype.
• Acyclic, directed, weakly-connected graph with max in-degree 1. Note that the infinite path graph has two non-isomorphic versions under this definition, and trees do not necessarily have a root. I'll call this DirectedTree.
• Acyclic, directed, weakly-connected graph with max in-degree 1, and one vertex with in-degree 0. This is a "rooted tree" (with no ordering of children). Note that "acyclic, directed, weakly-connected with max in-degree 1" is equivalent to "a pointed undirected graph that IsTree", that is, an IsTree graph with a single designated "root". I will call this RootedTree.
• DirectedTree+LocallyFinite.
• DirectedTree+Fintype. The same as RootedGraph+Fintype.
• RootedGraph+LocallyFinite.
• IsTree+LocallyFinite + the condition that each vertex has degree 1 or degree _k_, and then this is called either a _k_-tree, or a (k-1)-tree, depending on context. I'll call this kEqTree. Especially common with k=2.
• Like kEqTree, but instead the requirement is just that degree is _at most_ k. We could call this a kLETree.
• kTree + Fintype.
• The permutations of DirectedTree and RootedGraph but with the k-regularity condition.
• All the versions of kEqTree and kLETree, but with an additional _ordering_ on the children. For instance with kEqTree with k=2, and then the children are the left- and right-children. For a kLETree with k=2, some nodes can have just one child, but it is not distinguished whether that's the "left" or "right" child -- it's just the only child.
• Versions of kLETree where, when the degree is more than 1 and less than k, there is a distinct notion of which neighbors are "missing". That is, the neighbors of every vertex can be described as Maybe (Fin k -> Maybe V). Mathlib's Tree then describes an kLETree 2, RootedGraph on a Fintype, with this additional "missing" info -- with the ability to store data on the vertices.
• All of the above are sometimes implicitly meant "up to isomorphism", which in Lean would of course be a distinct type from the trees itself. For instance, when people talk about counting unlabelled trees on n vertices.
• Last and _certainly_ least, I contend that "tree" is very often used by computer scientists to actually mean any DAG -- even ones that are weakly cyclic. For instance, the "git-tree", an "inheritance tree" (in any language with multiple inheritance, such as C++), or a "dependency tree" are all DAGs, not trees. But they are still colloquially referred to as trees, and often described in code by a class named Tree or similar.

I wonder if anyone can come up with some that I've missed! :) And while some might sound silly, I promise I've seen (nearly?) all of these used in practice... for instance, I've seen IsTree+LocallyFinite come up in condensed matter physics plenty of times, as well as DirectedTree+LocallyFinite (_without_ a root).

[Alex Meiburg]

Well would you know it, I sent this message and only afterwards noticed Daniel Weber 's message. Ha!