最初のやり方 - 菊やんの雑記帳

$T = 1 + T^2$
$T^7 = T^6\times T = T^6\times(1 + T^2) = T^6 + T^8$
$T^7 = T^5 + T^7 + T^8$
$T^7 = T^4 + T^6 + T^7 + T^8$
$T^7 = T + T^3 + T^4 + T^5 + T^6 + T^7 + T^8$
$T^7 = T + T^3\times(1 + T + T^2 + T^3 + T^5) + T^7$
$T~7 = T + T^4 + T^7$
$T^7 = (1 + T + T^2 + T^3 + T^5) + T^4 + T^7$
$T^7 = 1 + T + T^2 + T^3 + T^4 + T^5 + T^7 = T$

最初の場合わけ
$T^7 = T + T^3 + T^4 + T^5 + T^6 + T^7 + T^8$

match t1, t2, t3, t4, t5, t6, t7 with
| Leaf, Leaf, Leaf, Leaf, Leaf, Leaf, s1 => f_1 s1 (* T *)
| Leaf, Leaf, Leaf, Leaf, Leaf, (Node s1 s2), s3 => f_3 s1 s2 s3 (* T^3 *)
| Leaf, Leaf, Leaf, Leaf, (Node s1 s2), s3, s4 => f_4 s1 s2 s3 s4 (* T^4 *)
略
| (Node s1 s2), s3, s4, s5, s6, s7, s8 => f_8 s1 s2 s3 s4 s5 s6 s7 s8 (* T^8 *)
end

次の場合わけ
$T = 1 + T + T^2 + T^3 + T^5$

f_1 s1 :=
match s1 with
| Leaf => f_1_0 (* 1 *)
| Node u1 Leaf => f_1_1 u1 (* T *)
| Node u1 (Node u2 Leaf) => f_1_2 u1 u2 (* T^2 *)
略
| Node u1 (Node u2 (Node u3 (Node u4 u5))) => f_1_5 u1 u2 u3 u4 u5 (* T^5 *)
end.

構築

f_1_0 := Leaf  (* 長さ0 *)
f_1_1 u1 := Node u1 Leaf  (* 長さ1 *)
f_1_2 u1 u2 := Node u1 (Node u2 Leaf)  (* 長さ2 *)
f_1_3 u1 u2 u3 := Node u1 (Node u2 (Node u3 Leaf))  (* 長さ3 *)

f_3_x s1 s2 s3 s4 := Node s1 (Node s2 (Node s3 (Node s4 Leaf)))  (* 長さ4 *)
f_3 s1 s2 s3 := f_3_x s1 s2 s3 Leaf  (* 長さ4の長さ0 *)
f_4 s1 s2 s3 s4 := f_3_x s1 s2 s3 (Node s4 Leaf)  (* 長さ4の長さ1 *)
f_5 s1 s2 s3 s4 s5 := f_3_x s1 s2 s3 (Node s4 (Node s5 Leaf))  (* 長さ4の長さ2 *)
f_6 s1 s2 s3 s4 s5 s6 := f_3_x s1 s2 s3 (Node s4 (Node s5 (Node s6 Leaf)))  (* 長さ4の長さ3 *)
f_8 s1 s2 s3 s4 s5 s6 s7 s8 := f_3_x s1 s2 s3 (Node s4 (Node s5 (Node s6 (Node s7 s8))))  (* 長さ4の長さ4以上 *)

f_1_5 u1 u2 u3 u4 u5 := Node u1 (Node u2 (Node u3 (Node u4 (Node u5 Leaf))))  (* 長さ5 *)
f_7 s1 s2 s3 s4 s5 s6 s7 := Node u1 (Node u2 (Node u3 (Node u4 (Node u5 (Node s6 s7)))))  (* 長さ6以上 *)

この場合わけを圧縮すると８通りぐらいにはなる。

やってみるとわかるが、 $T = 1 + T + T^2 + T^3 + T^5$ の向きの場合わけはかなり圧縮が効く。

しかし、 $T^7 = T + T^3 + T^4 + T^5 + T^6 + T^7 + T^8$ の向きの場合わけはさっぱり圧縮できない。