データ集合のあいだの関係（被リンク用）

「圏論やモナドが、どうして文書処理やXMLと関係するのですか？ - 檜山正幸のキマイラ飼育記 (はてなBlog)」にて：

1. T⊆Templ(A)⊆Nest(A)
2. A⊆B ならば、Templ(A)⊆Templ(B)、Nest(A)⊆Nest(B)
3. 0が空集合なら、Templ(0)＝T、Nest(0)＝T
4. Templ(T)＝TT、Nest(T)＝NT

これらを明白に示そう。まず、TとTTのnestLevelによる特徴付け。

• t∈T ⇔ nestLevel(t) = 0
• t∈TT ⇔ nestLevel(t) ≦ 1

BBC(t)を、t∈NTの末端ブロック内容（Bottom Block Content でBBC）をかき集めた集合とする。BBC(t)は、プログラミング課題4のプログラムから簡単に作れる集合値関数。BBCを使うと、次の特徴付けができる。

• t∈T ⇔ BBC(t) = 0
• t∈Nest(A) ⇔ BBC(t)⊆A

Templ(A)の特徴付けは（∧はandの意味）：

• t∈Templ(A) ⇔ (nestLevel(t)≦1 ∧ BBC(t)⊆A)

さて、問題の等式群を示そう。1番目と2番目は直感的にも分かりやすいから省略して、最初に、Templ(0)＝Tを示す； t∈Templ(0) は、上の特徴付けから、nestLevel(t)≦1 ∧ BBC(t)⊆0。ところが、BBC(t)⊆0から BBC(t) = 0、これからt∈T。t∈T ⇒ t∈Templ(0) も明らか（だって、T⊆Templ(A)だったもん）。これで示せた。

次、Nest(0)＝T； t∈Nest(0) ⇔ BBC(t)⊆0、これから t∈Nest(0) ⇔ BBC(t) = 0 だけど、BBC(t) = 0 は t∈T を意味する。

その次、Templ(T)＝TT； Templ(A)の特徴付けを使うと、t∈Templ(T) ⇔ (nestLevel(t)≦1 ∧ BBC(t)⊆T)。だけど、BBC(t)⊆Tは当たり前（常に成立）だから落として、t∈Templ(T) ⇔ nestLevel(t)≦1 。nestLevle(t)≦1 ってことは、t∈TTに他ならない。

最後に、Nest(T)＝NT； Nest(A)の特徴付けを使うと、t∈Nest(T) ⇔ BBC(t)⊆T。BBC(t)⊆T は当たり前だから、tには何の条件も付いてない。つまり、tは任意のネストしたテキスト。