Rose tree

From Wikipedia, the free encyclopedia
For the species of rhododendron, see Rhododendron maximum.

In computing, a rose tree is a term for the value of a tree data structure with a variable and unbounded number of branches per node.[1] The term is mostly used in the functional programming community, e.g., in the context of the Bird–Meertens formalism.[2] Apart from the multi-branching property, the most essential characteristic of rose trees is the coincidence of bisimilarity with identity: two distinct rose trees are never bisimilar.

Naming[]

The name "rose tree" was coined by Lambert Meertens to evoke the similarly-named, and similarly-structured, common rhododendron.[3]

We shall call such trees rose trees, a literal translation of rhododendron (Greek ῥόδον = rose, δένδρον = tree), because of resemblance to the habitus of this shrub, except that the latter does not grow upside-down on the Northern hemisphere.

Recursive definition[]

Well-founded rose trees can be defined by a recursive construction of entities of the following types:

  1. A base entity is an element of a predefined ground set V of values (the "tip"-values[3]).
  2. A branching entity (alternatively, a forking entity or a forest entity) is either of the following sub-types:
    1. A set of entities.
    2. A sequence of entities.
    3. A partial map from a predefined set Σ of names to entities.

    Any of (a)(b)(c) can be empty. Note that (b) can be seen as a special case of (c) – a sequence is just a map from an initial segment of the set ℕ of natural numbers.

  3. A pairing entity is an ordered pair (F, x) such that F is a branching entity and x is an element of a predefined set L of "label" values. Since a pairing entity can only contain a branching entity as its component, there is an induced division into sub-types (3a), (3b) or (3c) corresponding to sub-types of branching entities.

Typically, only some combinations of entity types are used for the construction. The original paper[3] only considers 1+2b ("sequence-forking" rose trees) and 1+2a ("set-forking" rose trees). In later literature, the 1+2b variant is usually introduced by the following definition: 

data Tree a = Leaf a | Node [Tree a]

A rose tree [...] is either a leaf containing a value, or a node that can have an arbitrary list of subtrees.[4]

The most common definition used in functional programming (particularly in Haskell) combines 3+2b: 

data Rose α = Node α [Rose α]

An element of Rose α consists of a labelled node together with a list of subtrees.[1] That is, a rose tree is a pairing entity (type 3) whose branching entity is a sequence (thus of type 2b) of rose trees.

Sometimes even the combination 1+3b is considered.[5][6] The following table provides a summary of the most established combinations of entities.

Terminology Entities used
Well-founded set (2a)
Well-founded nested list value (2b)(1)
Well-founded nested dictionary value (2c)(1)
Well-founded nested data value (2b)(2c)(1)
An L-name as known from forcing (2a)(3)[w 1]
Well-founded rose tree in the most common sense (3)(2b)[w 1]

Notes:

  1. ^ a b For the (2a)(3) and (3)(2b) combinations, the second stated entity type is only intermediate - it is just used for the definition of the "final" entity which is of the first type stated. Moreover, the types are strictly alternating, i.e. a branching entity can only contain a pairing entity as its member.

General definition[]

General rose trees can be defined via bisimilarity of accessible pointed multidigraphs with appropriate labelling of nodes and arrows. These structures are generalization of the notion of accessible pointed graph (abbreviated as apg) from non-well-founded set theory. We will use the apq acronym for the below described multidigraph structures. This is meant as an abbreviation of "accessible pointed quiver" where quiver is an established synonym for "multidigraph".

In a correspondence to the types of entities used in the recursive definition, each node of an apq is assigned a type (1), (2a), (2b), (2c) or (3). The apqs are subject to conditions that mimic the properties of recursively constructed entities.

    1. A node of type (1) is an element of the predefined set V of ground values.
    2. A node of type (1) does not appear as the source of an arrow.
    1. A node of type (3) appears as the source of exactly one arrow.
    2. The target of the arrow mentioned in (a) is a node of type (2).
  3. Two distinct arrows with the same source node of type (2a) have distinct targets.
  4. A node is labelled iff it is of type (3). The label belongs to the predefined set L.
    1. An arrow is labelled by an index from ℕ if its source node is of type (2b).
    2. An arrow is labelled by a name from a predefined set Σ if its source node is of type (2c).
    3. Otherwise an arrow is unlabelled.
  6. Labels of arrows with the same source node are distinct.
  7. Labels of arrows with the same source node of type (2b) form an initial segment of ℕ.

A bisimilarity between apqs