今、コンビネータ代数を学ぼうと思い、以下の論文を読んでいる。
1989年にCategories in computer science and logic誌に載っていたが、2017年に書き直したようだ。こういう点を考えると数学というのは、あまり焦って結果を出すというよりも結果が出たら発表するというもので、まるで文学作品のようなものなのかもしれない。
Combinators;or, a semantic argument for the extensional principle
Peter Freyd
外延原理
ある集合の要素において等価性(equality)を定義するために外延等価性が必要である。外延等価性とは以下の通り：
全て$x$に対して$x$を含まない$\psi, \psi'$が$$\psi x=\psi' x$$を満たすならば、$$\psi = \psi'$$となる。
例えば、
コンビネータ$I$は$SKK$と置き換えられるが、同様に$SKS$も$I$となるので、$SKK=SKS$となる。
$SKKt\rightarrow Kt(Kt)\rightarrow t=It$
外延定理より、$SKKt=It$ならば、$SKK=I$
$SKSt\rightarrow Kt(St)\rightarrow t=It$
外延定理より$SKSt=It$ならば、$SKS=I$
もう一つの例は、右射影二項演算子$K'\equiv\lambda xy.y$である。
$K'xy\rightarrow \lambda xy.y(xy)\rightarrow y$
$KIxy\rightarrow Iy\rightarrow y$
外延原理より、$K'xy=KIxy$ならば、$K'=KI$である。
ドット積
コンビネータ代数$A$が与えられた時、別のコンビネータ代数$\bullet A$を定義してみる。原始二項操作$$x\cdot y\equiv Sxy$$（ドット積）で定義する。
ドット$K$を$$\dot K\equiv KK$$と、ドット$S$を$$\dot S\equiv KS$$と定義する。
EP1, EP2
$EP1\bullet)\quad \dot K\cdot x\cdot y=x$
$EP2\bullet)\quad \dot S\cdot x\cdot y\cdot z=
x\cdot z\cdot (y\cdot z)$
ドットなしの式は：
$EP1)\quad S(S(KK)x)y=x$
$EP2)\quad S(S(S(KS)x)y)z=S(Sxz)(Syz)$
EP1, EP2の検証
$EP1)$
$S(S(KK)x)yt\rightarrow S(KK)xt(yt)
\rightarrow (KK)t(xt)(yt)
\rightarrow K(xt)(yt)
\rightarrow xt$
$EP2)$
$S(S(S(KS)x)y)zt$
$\rightarrow S(S(KS)x)yt(zt)
\rightarrow S(KS)xt(yt)(zt)$
$\rightarrow KSt(xt)(yt)(zt)
\rightarrow S(xt)(yt)(zt)$
$\rightarrow (xt)(zt)((yt)(zt))
\equiv Sxzt(Syzt)
\equiv S(Sxz)(Syz)t$
K写像
$K$写像とは、$a\in A$を$Ka\in\bullet A$に送る関数である。
コンビネータ代数の同型性(homomorphism)に言及するために次の式が必要となる。
$EP3\bullet)\quad K(xy)\equiv (Kx)\cdot(Ky)$
ドットなしの式は：
$EP3)\quad K(xy)\equiv S(Kx)(Ky)$
K写像の検証
$S(Kx)(Ky)t\rightarrow Kxt(Kyt)
\rightarrow xy$
$K(xy)t\rightarrow xy$
EP4 I
$EP4\bullet)\quad (Kx)\cdot I\equiv x$
ドットなしの式は：
$EP4)\quad S(Kx)I\equiv x$
検証は、
$S(Kx)It\rightarrow Kxt(It)\rightarrow xt$