Plane trees

Content created by Egbert Rijke.

Created on 2024-04-13.
Last modified on 2024-04-13.

module trees.plane-trees where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.maybe
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

open import lists.lists

open import trees.full-binary-trees
open import trees.w-types

open import univalent-combinatorics.standard-finite-types

Idea

A plane tree is a finite directed tree that can be drawn on a plane with the root at the bottom, and all branches directed upwards. More precisely, a plane tree consists of a root and a family of plane trees indexed by a standard finite type. Plane trees are also known as ordered trees.

The type of plane trees can be defined in several equivalent ways:

  • The type of plane trees is the inductive type with constructor

      (n : ℕ) → (Fin n → plane-tree) → plane-tree.

  • The type of plane trees is the W-type

      𝕎 ℕ Fin.

  • The type of plane trees is the inductive type with constructor

      list plane-tree → plane-tree.

The type of plane trees is therefore the least fixed point of the list functor X ↦ list X. In particular, plane-tree is the least fixed point of the functor

  X ↦ 1 + plane-tree × X.

The least fixed point for this functor coincides with the least fixed point of the functor

  X ↦ 1 + X².

Thus we obtain an equivalence

  plane-tree ≃ full-binary-tree

from the type of plane trees to the type of full binary trees.

Definitions

Plane trees

data plane-tree : UU lzero where
  make-plane-tree : {n : ℕ} → (Fin n → plane-tree) → plane-tree

Plane trees as W-types

plane-tree-𝕎 : UU lzero
plane-tree-𝕎 = 𝕎 ℕ Fin

Plane trees defined using lists

data listed-plane-tree : UU lzero where
  make-listed-plane-tree : list listed-plane-tree → listed-plane-tree

Operations on plane trees

The type of nodes, including leaves, of a plane tree

node-plane-tree : plane-tree → UU lzero
node-plane-tree (make-plane-tree {n} T) =
  Maybe (Σ (Fin n) (λ i → node-plane-tree (T i)))

The root of a plane tree

root-plane-tree : (T : plane-tree) → node-plane-tree T
root-plane-tree (make-plane-tree T) = exception-Maybe

Properties

The type of listed plane trees is equivalent to the type of lists of listed plane trees

unpack-listed-plane-tree : listed-plane-tree → list listed-plane-tree
unpack-listed-plane-tree (make-listed-plane-tree t) = t

is-section-unpack-listed-plane-tree :
  is-section make-listed-plane-tree unpack-listed-plane-tree
is-section-unpack-listed-plane-tree (make-listed-plane-tree t) = refl

is-retraction-unpack-listed-plane-tree :
  is-retraction make-listed-plane-tree unpack-listed-plane-tree
is-retraction-unpack-listed-plane-tree l = refl

is-equiv-make-listed-plane-tree :
  is-equiv make-listed-plane-tree
is-equiv-make-listed-plane-tree =
  is-equiv-is-invertible
    ( unpack-listed-plane-tree)
    ( is-section-unpack-listed-plane-tree)
    ( is-retraction-unpack-listed-plane-tree)

equiv-make-listed-plane-tree : list listed-plane-tree ≃ listed-plane-tree
pr1 equiv-make-listed-plane-tree = make-listed-plane-tree
pr2 equiv-make-listed-plane-tree = is-equiv-make-listed-plane-tree

The type of listed plane trees is equivalent to the type of full binary trees

Since plane-tree is inductively generated by a constructor list plane-tree → plane-tree, we have an equivalence

  list plane-tree ≃ plane-tree.

This description allows us to obtain an equivalence plane-tree ≃ full-binary-tree from the type of plane trees to the type of full binary trees. Indeed, by the above equivalence we can compute

  plane-tree ≃ list plane-tree
             ≃ 1 + plane-tree × list plane-tree
             ≃ 1 + plane-tree²

On the other hand, the type full-binary-tree is a fixed point for the polynomial endofunctor X ↦ 1 + full-binary-tree × X, since we have equivalences.

  full-binary-tree ≃ 1 + full-binary-tree²
                   ≃ 1 + full-binary-tree × full-binary-tree

Since full-binary-tree is the least fixed point of the polynomial endofunctor X ↦ 1 + X², we obtain a (1 + X²)-structure preserving map

  full-binary-tree → plane-tree.

Likewise, since plane-tree is the least fixed point of the endofunctor list, we obtain a list-structure preserving map

  plane-tree → full-binary-tree.

Initiality of both full-binary-tree and plane-tree can then be used to show that these two maps are inverse to each other, i.e., that we obtain an equivalence

  plane-tree ≃ full-binary-tree.

full-binary-tree-listed-plane-tree : listed-plane-tree → full-binary-tree
full-binary-tree-listed-plane-tree (make-listed-plane-tree nil) =
  leaf-full-binary-tree
full-binary-tree-listed-plane-tree (make-listed-plane-tree (cons T l)) =
  join-full-binary-tree
    ( full-binary-tree-listed-plane-tree T)
    ( full-binary-tree-listed-plane-tree (make-listed-plane-tree l))

listed-plane-tree-full-binary-tree : full-binary-tree → listed-plane-tree
listed-plane-tree-full-binary-tree leaf-full-binary-tree =
  make-listed-plane-tree nil
listed-plane-tree-full-binary-tree (join-full-binary-tree S T) =
  make-listed-plane-tree
    ( cons
      ( listed-plane-tree-full-binary-tree S)
      ( unpack-listed-plane-tree (listed-plane-tree-full-binary-tree T)))

is-section-listed-plane-tree-full-binary-tree :
  is-section
    ( full-binary-tree-listed-plane-tree)
    ( listed-plane-tree-full-binary-tree)
is-section-listed-plane-tree-full-binary-tree leaf-full-binary-tree =
  refl
is-section-listed-plane-tree-full-binary-tree
  ( join-full-binary-tree S T) =
  ap-binary
    ( join-full-binary-tree)
    ( is-section-listed-plane-tree-full-binary-tree S)
    ( ( ap
        ( full-binary-tree-listed-plane-tree)
        ( is-section-unpack-listed-plane-tree _)) ∙
      ( is-section-listed-plane-tree-full-binary-tree T))

is-retraction-listed-plane-tree-full-binary-tree :
  is-retraction
    ( full-binary-tree-listed-plane-tree)
    ( listed-plane-tree-full-binary-tree)
is-retraction-listed-plane-tree-full-binary-tree (make-listed-plane-tree nil) =
  refl
is-retraction-listed-plane-tree-full-binary-tree
  ( make-listed-plane-tree (cons T l)) =
  ( ap
    ( make-listed-plane-tree)
    ( ap-binary
      ( cons)
      ( is-retraction-listed-plane-tree-full-binary-tree T)
      ( ap
        ( unpack-listed-plane-tree)
        ( is-retraction-listed-plane-tree-full-binary-tree
          ( make-listed-plane-tree l)))))

is-equiv-full-binary-tree-listed-plane-tree :
  is-equiv full-binary-tree-listed-plane-tree
is-equiv-full-binary-tree-listed-plane-tree =
  is-equiv-is-invertible
    ( listed-plane-tree-full-binary-tree)
    ( is-section-listed-plane-tree-full-binary-tree)
    ( is-retraction-listed-plane-tree-full-binary-tree)

equiv-full-binary-tree-listed-plane-tree :
  listed-plane-tree ≃ full-binary-tree
pr1 equiv-full-binary-tree-listed-plane-tree =
  full-binary-tree-listed-plane-tree
pr2 equiv-full-binary-tree-listed-plane-tree =
  is-equiv-full-binary-tree-listed-plane-tree

Recent changes