ref: http://d.hatena.ne.jp/ku-ma-me/20081023/p1
ref: http://d.hatena.ne.jp/m-hiyama/20081031/1225416719
ポイントは檜山さんが書かれているように、T = 1 + T^2 を使って T から T^7 への式変形を構成するところです。
その式変形は以下。各行は T^0 〜 T^8 までの係数を並べて書いています (T なら 0 1 0 0 0 0 0 0 0 、1 + T^2 なら 1 0 1 0 0 0 0 0 0 、という感じ) 。
0 1 0 0 0 0 0 0 0
/ \
1 0 1 0 0 0 0 0 0
/ \
1 1 0 1 0 0 0 0 0
/ \
1 1 1 0 1 0 0 0 0
/ \
1 1 1 1 0 1 0 0 0
/ \
1 1 1 1 1 0 1 0 0
/ \
1 1 1 1 1 1 0 1 0
/ \
1 1 1 1 1 1 1 0 1
/ \
1 1 1 1 1 2 0 1 1
/ \
1 1 1 1 2 1 1 1 1
\ /
1 1 0 2 1 1 1 1 1
\ /
1 0 1 1 1 1 1 1 1
\ /
0 1 0 1 1 1 1 1 1
\ /
0 0 1 0 1 1 1 1 1
\ /
0 0 0 1 0 1 1 1 1
\ /
0 0 0 0 1 0 1 1 1
\ /
0 0 0 0 0 1 0 1 1
\ /
0 0 0 0 0 0 1 0 1
\ /
0 0 0 0 0 0 0 1 0ちょうど 18 ステップでした。美しいですね。
面白かったのはここまでで、後は苦行。馬鹿正直に実装にするには、各行ごとに対応する型をバリアントとして定義していきます。
-- 0 1 0 0 0 0 0 0 0 の型 data Step0 = Step0_1 Tree -- 1 0 1 0 0 0 0 0 0 の型 data Step1 = Step1_0 | Step1_2 Tree Tree -- 1 1 0 1 0 0 0 0 0 の型 data Step2 = Step2_0 | Step2_1 Tree | Step2_3 Tree Tree Tree -- 1 1 1 0 1 0 0 0 0 の型 data Step3 = Step3_0 | Step3_1 Tree | Step3_2 Tree Tree | Step3_4 Tree Tree Tree Tree ... -- 1 1 1 1 2 1 1 1 1 の型 data Step9 = Step9_0 | Step9_1 Tree | Step9_2 Tree Tree | Step9_3 Tree Tree Tree | Step9_4_a Tree Tree Tree Tree | Step9_4_b Tree Tree Tree Tree | Step9_5 Tree Tree Tree Tree Tree | Step9_6 Tree Tree Tree Tree Tree Tree | Step9_7 Tree Tree Tree Tree Tree Tree Tree | Step9_8 Tree Tree Tree Tree Tree Tree Tree Tree ... -- 0 0 0 0 0 0 0 1 0 の型 data Step18 = Step18_7 Tree Tree Tree Tree Tree Tree Tree
係数が 2 のところはバリアントも 2 つ書かないといけないところに注意。
そして Step
step0_to_step1 :: Step0 -> Step1 step0_to_step1 (Step0_1 Leaf) = Step1_0 step0_to_step1 (Step0_1 (Node tl tr)) = Step1_2 tl tr step1_to_step2 :: Step1 -> Step2 step1_to_step2 Step1_0 = Step2_0 step1_to_step2 (Step1_2 t0 Leaf) = Step2_1 t0 step1_to_step2 (Step1_2 t0 (Node tl tr)) = Step2_3 t0 tl tr step2_to_step3 :: Step2 -> Step3 step2_to_step3 Step2_0 = Step3_0 step2_to_step3 (Step2_1 t0) = Step3_1 t0 step2_to_step3 (Step2_3 t0 t1 Leaf) = Step3_2 t0 t1 step2_to_step3 (Step2_3 t0 t1 (Node tl tr)) = Step3_4 t0 t1 tl tr ... step1_to_step0 :: Step1 -> Step0 step1_to_step0 Step1_0 = Step0_1 Leaf step1_to_step0 (Step1_2 tl tr) = Step0_1 (Node tl tr) step2_to_step1 :: Step2 -> Step1 step2_to_step1 Step2_0 = Step1_0 step2_to_step1 Step2_1 t0 = Step1_2 t0 Leaf step2_to_step1 (Step2_3 t0 tl tr) = Step1_2 t0 (Node tl tr) step3_to_step2 :: Step3 -> Step2 step3_to_step2 Step3_0 = Step2_0 step3_to_step2 Step3_1 t0 = Step2_1 t0 step3_to_step2 Step3_2 t0 t1 = Step2_3 t0 t1 Leaf step3_to_step2 (Step3_4 t0 t1 tl tr) = Step2_3 t0 t1 (Node tl tr) ...
あとはこれらをつなげて f と g を書きます。
f :: Tree7 -> Tree f (t0, t1, t2, t3, t4, t5, t6) = (\ (Step0_1 t) -> t) $ step1_to_step0 $ step2_to_step1 $ ... step17_to_step16 $ step18_to_step17 $ Step18_7 t0 t1 t2 t3 t4 t5 t6 t7 g :: Tree -> Tree7 g t = (\ (Step18_7 t0 t1 t2 t3 t4 t5 t6) -> (t0, t1, t2, t3, t4, t5, t6)) $ step17_to_step18 $ step16_to_step17 $ ... step1_to_step2 $ step0_to_step1 $ Step0_1 t
これで終わり。ふう。
ぼくが実際に書いたプログラムは、以下のようにステップを短くして、
0 1 0 0 0 0 0 0 0
/ \
1 0 1 0 0 0 0 0 0
/ \
1 1 0 1 0 0 0 0 0
/ \
1 1 1 0 1 0 0 0 0
/ \
1 1 1 1 0 1 0 0 0
/ \
1 1 1 1 1 0 1 0 0
\ / / \
1 1 0 2 0 1 0 1 0
\ / / \
1 0 1 1 0 1 1 0 1
\ / / \
0 1 0 1 0 2 0 1 1
\ / / \
0 0 1 0 1 1 1 1 1
\ /
0 0 0 1 0 1 1 1 1
\ /
0 0 0 0 1 0 1 1 1
\ /
0 0 0 0 0 1 0 1 1
\ /
0 0 0 0 0 0 1 0 1
\ /
0 0 0 0 0 0 0 1 0バリアントを使いまわしたものです。
module Main where import Control.Monad import Test.QuickCheck data Tree = Leaf | Node Tree Tree deriving (Eq, Show) type Tree7 = (Tree, Tree, Tree, Tree, Tree, Tree, Tree) instance Arbitrary Tree where arbitrary = oneof [ return Leaf, liftM2 Node arbitrary arbitrary ] instance (Arbitrary a, Arbitrary b, Arbitrary c, Arbitrary d, Arbitrary e, Arbitrary f, Arbitrary g) => Arbitrary (a, b, c, d, e, f, g) where arbitrary = return (,,,,,,) `ap` arbitrary `ap` arbitrary `ap` arbitrary `ap` arbitrary `ap` arbitrary `ap` arbitrary `ap` arbitrary data Value = T0 | T1 Tree | T2 Tree Tree | T3a Tree Tree Tree | T3b Tree Tree Tree | T4 Tree Tree Tree Tree | T5a Tree Tree Tree Tree Tree | T5b Tree Tree Tree Tree Tree | T6 Tree Tree Tree Tree Tree Tree | T7 Tree Tree Tree Tree Tree Tree Tree | T8 Tree Tree Tree Tree Tree Tree Tree Tree deriving (Eq, Show) f :: Tree7 -> Tree f (it0, it1, it2, it3, it4, it5, it6) = ot where v1 = T7 it0 it1 it2 it3 it4 it5 it6 v2 = case v1 of T7 t0 t1 t2 t3 t4 t5 Leaf -> T6 t0 t1 t2 t3 t4 t5 T7 t0 t1 t2 t3 t4 t5 (Node tl tr) -> T8 t0 t1 t2 t3 t4 t5 tl tr v -> v v3 = case v2 of T6 t0 t1 t2 t3 t4 Leaf -> T5a t0 t1 t2 t3 t4 T6 t0 t1 t2 t3 t4 (Node tl tr) -> T7 t0 t1 t2 t3 t4 tl tr v -> v v4 = case v3 of T5a t0 t1 t2 t3 Leaf -> T4 t0 t1 t2 t3 T5a t0 t1 t2 t3 (Node tl tr) -> T6 t0 t1 t2 t3 tl tr v -> v v5 = case v4 of T4 t0 t1 t2 Leaf -> T3a t0 t1 t2 T4 t0 t1 t2 (Node tl tr) -> T5a t0 t1 t2 tl tr v -> v v6 = case v5 of T3a t0 t1 Leaf -> T2 t0 t1 T3a t0 t1 (Node tl tr) -> T4 t0 t1 tl tr v -> v v7 = case v6 of T2 t0 Leaf -> T1 t0 T2 t0 (Node tl tr) -> T3a t0 tl tr T4 t0 t1 t2 t3 -> T5b t0 t1 t2 t3 Leaf T6 t0 t1 t2 t3 tl tr -> T5b t0 t1 t2 t3 (Node tl tr) v -> v v8 = case v7 of T1 Leaf -> T0 T1 (Node tl tr) -> T2 tl tr T5b t0 t1 t2 t3 t4 -> T6 t0 t1 t2 t3 t4 Leaf T7 t0 t1 t2 t3 t4 tl tr -> T6 t0 t1 t2 t3 t4 (Node tl tr) v -> v v9 = case v8 of T2 t0 Leaf -> T1 t0 T2 t0 (Node tl tr) -> T3b t0 tl tr T6 t0 t1 t2 t3 t4 t5 -> T7 t0 t1 t2 t3 t4 t5 Leaf T8 t0 t1 t2 t3 t4 t5 tl tr -> T7 t0 t1 t2 t3 t4 t5 (Node tl tr) v -> v vA = case v9 of T3b t0 t1 Leaf -> T2 t0 t1 T3b t0 t1 (Node tl tr) -> T4 t0 t1 tl tr T5a t0 t1 t2 t3 t4 -> T6 t0 t1 t2 t3 t4 Leaf T7 t0 t1 t2 t3 t4 tl tr -> T6 t0 t1 t2 t3 t4 (Node tl tr) v -> v vB = case vA of T4 t0 t1 t2 t3 -> T5a t0 t1 t2 t3 Leaf T6 t0 t1 t2 t3 tl tr -> T5a t0 t1 t2 t3 (Node tl tr) v -> v vC = case vB of T3a t0 t1 t2 -> T4 t0 t1 t2 Leaf T5a t0 t1 t2 tl tr -> T4 t0 t1 t2 (Node tl tr) v -> v vD = case vC of T2 t0 t1 -> T3a t0 t1 Leaf T4 t0 t1 tl tr -> T3a t0 t1 (Node tl tr) v -> v vE = case vD of T1 t0 -> T2 t0 Leaf T3a t0 tl tr -> T2 t0 (Node tl tr) v -> v vF = case vE of T0 -> T1 Leaf T2 tl tr -> T1 (Node tl tr) v -> v (T1 ot) = vF g :: Tree -> Tree7 g it = (ot0, ot1, ot2, ot3, ot4, ot5, ot6) where v1 = T1 it v2 = case v1 of T1 Leaf -> T0 T1 (Node tl tr) -> T2 tl tr v -> v v3 = case v2 of T2 t0 Leaf -> T1 t0 T2 t0 (Node tl tr) -> T3a t0 tl tr v -> v v4 = case v3 of T3a t0 t1 Leaf -> T2 t0 t1 T3a t0 t1 (Node tl tr) -> T4 t0 t1 tl tr v -> v v5 = case v4 of T4 t0 t1 t2 Leaf -> T3a t0 t1 t2 T4 t0 t1 t2 (Node tl tr) -> T5a t0 t1 t2 tl tr v -> v v6 = case v5 of T5a t0 t1 t2 t3 Leaf -> T4 t0 t1 t2 t3 T5a t0 t1 t2 t3 (Node tl tr) -> T6 t0 t1 t2 t3 tl tr v -> v v7 = case v6 of T2 t0 t1 -> T3b t0 t1 Leaf T4 t0 t1 tl tr -> T3b t0 t1 (Node tl tr) T6 t0 t1 t2 t3 t4 Leaf -> T5a t0 t1 t2 t3 t4 T6 t0 t1 t2 t3 t4 (Node tl tr) -> T7 t0 t1 t2 t3 t4 tl tr v -> v v8 = case v7 of T1 t0 -> T2 t0 Leaf T3b t0 tl tr -> T2 t0 (Node tl tr) T7 t0 t1 t2 t3 t4 t5 Leaf -> T6 t0 t1 t2 t3 t4 t5 T7 t0 t1 t2 t3 t4 t5 (Node tl tr) -> T8 t0 t1 t2 t3 t4 t5 tl tr v -> v v9 = case v8 of T0 -> T1 Leaf T2 tl tr -> T1 (Node tl tr) T6 t0 t1 t2 t3 t4 Leaf -> T5b t0 t1 t2 t3 t4 T6 t0 t1 t2 t3 t4 (Node tl tr) -> T7 t0 t1 t2 t3 t4 tl tr v -> v vA = case v9 of T1 t0 -> T2 t0 Leaf T3a t0 tl tr -> T2 t0 (Node tl tr) T5b t0 t1 t2 t3 Leaf -> T4 t0 t1 t2 t3 T5b t0 t1 t2 t3 (Node tl tr) -> T6 t0 t1 t2 t3 tl tr v -> v vB = case vA of T2 t0 t1 -> T3a t0 t1 Leaf T4 t0 t1 tl tr -> T3a t0 t1 (Node tl tr) v -> v vC = case vB of T3a t0 t1 t2 -> T4 t0 t1 t2 Leaf T5a t0 t1 t2 tl tr -> T4 t0 t1 t2 (Node tl tr) v -> v vD = case vC of T4 t0 t1 t2 t3 -> T5a t0 t1 t2 t3 Leaf T6 t0 t1 t2 t3 tl tr -> T5a t0 t1 t2 t3 (Node tl tr) v -> v vE = case vD of T5a t0 t1 t2 t3 t4 -> T6 t0 t1 t2 t3 t4 Leaf T7 t0 t1 t2 t3 t4 tl tr -> T6 t0 t1 t2 t3 t4 (Node tl tr) v -> v vF = case vE of T6 t0 t1 t2 t3 t4 t5 -> T7 t0 t1 t2 t3 t4 t5 Leaf T8 t0 t1 t2 t3 t4 t5 tl tr -> T7 t0 t1 t2 t3 t4 t5 (Node tl tr) v -> v (T7 ot0 ot1 ot2 ot3 ot4 ot5 ot6) = vF main :: IO () main = do quickCheck $ \x -> x == f (g x) quickCheck $ \x -> x == g (f x)
ながー。5 分岐とかは全然考えてないです。
