一般存在定理からの帰結 - 白のカピバラの逆極限 S.144-3

F を三引数をとる curry化された関数としよう。

G x y z = F z y x

の G を G = XXXXX の形で lambda を使わずに定義したい。これは flip だけでは出来ない気がする。curry uncurry も助けにはならない。

さて、BG公理系では反転公理というものがあって、
$<x,y,z>=<x,<y,z>>$
$<x_0, \cdots x_n >=<x_0,<x_1,\cdots x_n>>$
順序対に対して
$B=\{<y,x>| <x,y> \in A\}$
$C=\{<y,z,x>| <x,y,z> \in A\}$
$D=\{<x,z,y>| <x,y,z> \in A\}$

これにならって、flip1 flip2 flip3 を定義する。

flip1 f = (\(x,y) -> f (y,x) )
flip2 f = (\((x,y),z) -> f ((z,x),y))
flip3 f = (\((x,y),z) -> f ((y,x),z))

curry化の都合で変数の順番は逆になっている。

test a b c d = (a,b,c,d)

> test 1 2 3 4
(1,2,3,4)
> (curry . curry . curry . flip2 . flip3. uncurry . uncurry . uncurry) test 1 2 3 4
(1,2,4,3)
> (curry . curry . flip2 . flip3 . uncurry . uncurry) test 1 2 3 4
(1,3,2,4)
> (curry . flip1 . uncurry) test  1 2 3 4
(2,1,3,4)
> (curry . curry . curry . flip2 . flip2 . flip1 . flip3 . flip1 . flip2 . uncurry . uncurry . uncurry) test  1 2 3 4
(2,1,3,4)

これで生成できるから、4変数の任意の互換が存在。
やあ。群論とBG公理系エライ。
はじめ、curry . curry . curry . XXXXX . uncurry . uncurry . uncurry という形にしないといけないと思っていて、互換が作れないから「一般存在定理の反証か?」とあせったのは秘密。

curry . flip1 . uncurry == flip

だから、

curry . curry . flip2 . uncurry . uncurry
curry . curry . flip3 . uncurry . uncurry

を用意しておけば幸せということが分かる。

curry . curry . flip2 . flip2 . uncurry . uncurry

のほうが使い勝手がいいかもしれない。