Permutation

ここ二三日、順列と格闘してました。Agda の定義は Bijection がどうとかで高尚でなぁ。

やりたいのは数え上げなので

　　 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
　　 1 ∷ 0 ∷ 2 ∷ 3 ∷ []
　　 1 ∷ 2 ∷ 0 ∷ 3 ∷ []
　　 1 ∷ 2 ∷ 3 ∷ 0 ∷ []

ってな置換パターンを生成して、再帰的に組み合せてやればよい。

いきなり作ると Data.Fin とか Bijection で死んでしまうので、

refl : ∀ {xs} → xs ↭ xs
prep : ∀ {xs ys} x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
swap : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
trans : ∀ {xs ys zs} → xs ↭ ys → ys ↭ zs → xs ↭ zs

で inductive に作ってやると良いらしい。prep と swap は直接書けたので。ところが、

　Agda のプログラムの引数がまったく合わない

誰だよ、関数型言語はバグがないとか言ったのは... まぁ、できてしまえば、どうってことない。

これで、順列の交換子を数え上げれば終わりなはずです。