「7つのツリー」と「1つのツリー」の全単射

元ネタ
arxiv.org

ツリーを「『リーフ』または『2つのツリーを持つノード』」と定義する。ラベルは無く、ノードの左右は区別する。本記事ではリーフをL、ノードを [x, y] と略記する。Coqによる定義は以下のようになる。
Leaf と Node が T (ツリー) の2つのコンストラクタで、意味は「Leaf はツリーである」と「Node は 2つのツリーから作られるツリーである」。

Inductive T : Set :=
| Leaf: T
| Node: T -> T -> T.

Notation L := Leaf.
Notation "[ x , y ]" := (Node x y) (at level 60, x at next level, y at next level).

2つのツリーの場合

「2つのツリー」と「1つのツリー」の全単射があれば3でも4でも7でも何でもできる。しかし2つのツリー x, y から単純に [x, y] を作っても、L への写像がないので全射ではない。
そこで、ツリーと非負整数の全単射を使って { 2つのツリー ⇔ 2つの非負整数 ⇔ 1つの非負整数 ⇔ 1つのツリー } のように全単射を構築する。eval と build が互いに逆関数になっている。

eval(t) {
  ツリーを非負整数に写す。特に Leaf を 0 に写す
  if t = L {
    return 0
  } else {
    [x, y] <- t
    merge は2つの非負整数を1つに写す。例えば1桁ずつ並べる
    return 1 + merge(eval(x), eval(y))
  }
}

build(n) {
  非負整数からツリーを作る
  if n = 0 {
    return L
  } else {
    merge されいる n-1 を2つの非負整数a, bに分ける
    return [build(a), build(b)]
  }
}

7つのツリーの場合

驚くことに7の場合はツリー全体を見る必要はなく定数個のノードをリンクするだけでできる、新しくノードを追加するので元データを破壊しない。それがこれだ（唯一解ではない）。

Definition T7 := (T*T*T*T*T*T*T)%type.

Definition f71: T7 -> T := fun x =>
  match x with
  | (L, L, L, L, [e1, e2], f, g) => [[[[L, g], f], e1], e2]
  | (L, L, L, L, L, [f1, f2], g) => [[[[[[f1, f2], g], L], L], L], L]
  | (L, L, L, L, L, L, [[[[g1, g2], g3], g4], g5]) => [[[[[L, g1], g2], g3], g4], g5]
  | (L, L, L, L, L, L, g) => g
  | (a, b, c, d, e, f, g) => [[[[[[g, f], e], d], c], b], a]
  end.

Definition f17: T -> T7 := fun x =>
  match x with
  | [[[[L, g], f], e1], e2] => (L, L, L, L, [e1, e2], f, g)
  | [[[[[[f1, f2], g], L], L], L], L] => (L, L, L, L, L, [f1, f2], g)
  | [[[[[L, g1], g2], g3], g4], g5] => (L, L, L, L, L, L, [[[[g1, g2], g3], g4], g5])
  | [[[[[[g, f], e], d], c], b], a] => (a, b, c, d, e, f, g)
  | g => (L, L, L, L, L, L, g)
  end.

パターンマッチの優先のために元論文から順番を変えている。またf71とf17でもパターンの順番が変わっている。元論文ではこのアルゴリズムを非負整数に写すものに比べて "very explicit" と表現している。
T7 は L が前4つ・5つ・6つで大きく場合分けしている、T はツリーのルートから最左のノードをたどる辺数が3以下・4・5・6以上で場合分けしている。

なぜ7なのか

ツリーTは代数的データ型である。Leaf は1通りなのでその濃度は $1$ 。Node は2つのツリーの直積なのでその濃度は $T^2$ 。

$T = 1 + T^2$

この解は $\frac{1}{2} \pm i \frac{\sqrt {3} }{2}$ だが適切な式変形で

$T = T^7$

が導かれる。よって7つのツリーは定数回の場合分けでツリーに変形できる。
例えば1行目のパターン

(L, L, L, L, [e1, e2], f, g) => [[[[L, g], f], e1], e2]

これは $T^7$ の濃度の入力のうち $T^4$ にマッチする。2行目以降は残りの $T^7 - T^4$ に対してパターンマッチする。

コード

パターンマッチなので証明が数行でできる。

Inductive T : Set :=
| Leaf: T
| Node: T -> T -> T.

Notation L := Leaf.
Notation "[ x , y ]" := (Node x y) (at level 60, x at next level, y at next level).

Definition T7 := (T*T*T*T*T*T*T)%type.

Definition f71: T7 -> T := fun x =>
  match x with
  | (L, L, L, L, [e1, e2], f, g) => [[[[L, g], f], e1], e2]
  | (L, L, L, L, L, [f1, f2], g) => [[[[[[f1, f2], g], L], L], L], L]
  | (L, L, L, L, L, L, [[[[g1, g2], g3], g4], g5]) => [[[[[L, g1], g2], g3], g4], g5]
  | (L, L, L, L, L, L, g) => g
  | (a, b, c, d, e, f, g) => [[[[[[g, f], e], d], c], b], a]
  end.

Definition f17: T -> T7 := fun x =>
  match x with
  | [[[[L, g], f], e1], e2] => (L, L, L, L, [e1, e2], f, g)
  | [[[[[[f1, f2], g], L], L], L], L] => (L, L, L, L, L, [f1, f2], g)
  | [[[[[L, g1], g2], g3], g4], g5] => (L, L, L, L, L, L, [[[[g1, g2], g3], g4], g5])
  | [[[[[[g, f], e], d], c], b], a] => (a, b, c, d, e, f, g)
  | g => (L, L, L, L, L, L, g)
  end.

Theorem f171_id: forall x, f71 (f17 x) = x.
Proof.
  intros [| [| [| [| [| [| g f] e] []] []] []] []]; try reflexivity.
Qed.

Theorem f717_id: forall x, f17 (f71 x) = x.
Proof.
  intros [[[[[[[] []] []] []] []] []] g]; try reflexivity.
  destruct g as [|[|[|[| g1 g2] g3] g4] g5]; try reflexivity.
Qed.

終わりに

Anarchy Proof で出題されたので興味を持った