組み合わせ論理とは、Mosese Ilych Schönfinkelとhaslekll Curryが記号論理における変数を消去するために導入した手法だ。
ここまで、Haskellを勉強してきたが、ここでHaskellの名前が出てきた。感無量!
参考は下記の書籍:
J. Roger Hindley & Jonathan P. Seldin, Lambda-Caulculus and Combinators: An Introduction
2A 組み合わせ論理への導入
いくつかのコンビネータを導入する。
$\textbf{C}$:変数を交換する:$(\textbf{C}(f))(x,y)=f(y,x)$
$\textbf{B}$:二つの関数を合成する:$(\textbf{B}(f,g))(x)=f(g(x))$
$\textbf{B'}$:二つの関数を逆順で合成する:$(\textbf{B'}(f,g))(x)=g(f(x))$
$\textbf{I}$:恒等関数:$\textbf{I}(f)=f$
$\textbf{K}$:定数を生成する関数:($\textbf{K}(a))(x)=a$
定義2.9(弱redex)
$\textbf{I}X, \textbf{K}XY, \textbf{S}XYZ$を弱redexと呼ぶ。
$\textbf{I}X\rightarrow X$
$\textbf{K}XY\rightarrow X$
$\textbf{S}XYZ\rightarrow XZ(YZ)$
定義2.10
弱標準形式とは、弱redexを含まない項のことを言う。
例2.11
$\textbf{B}\equiv\textbf{S}(\textbf{KS})\textbf{K}$と定義すると、全ての$X,Y,Z$に対し$\textbf{B}XYZ\triangleright_w X(YZ)$
なぜならば、
$\textbf{B}XYZ\equiv\textbf{S}(\textbf{KS})\textbf{K}XYZ$
$\rightarrow\textbf{KS}X(\textbf{K}X)YZ$、ここで$\textbf{S}(\textbf{KS})\textbf{K}X\rightarrow\textbf{KS}X(\textbf{K}X)$によって
$\rightarrow\textbf{S}(\textbf{K}X)YZ$、ここで$\textbf{KS}X\rightarrow\textbf{S}$によって
$\rightarrow\textbf{K}XZ(YZ)$
$\rightarrow X(YZ)$、ここで$\textbf{K}XZ\rightarrow X$によって
従って
$$\textbf{B}XYZ\triangleright_w X(YZ)$$
例2.12
$\textbf{C}\equiv\textbf{S}(\textbf{BBS})(\textbf{KK})$と定義すると、全ての$X,Y,Z$に対し$\textbf{C}XYZ\triangleright_w XZY$
これを示す。
$\textbf{C}XYZ\equiv\textbf{S}(\textbf{BBS})(\textbf{KK})XYZ$
$\rightarrow\textbf{BBS}X(\textbf{KK}X)YZ$
$\rightarrow\textbf{BBS}X(\textbf{K})YZ$、ここで$\textbf{KK}X\rightarrow\textbf{K}$によって
$\rightarrow\textbf{BBS}X\textbf{K}YZ$
$\rightarrow\textbf{B}(\textbf{S}X)\textbf{K}YZ$、ここでは例2.11によって
$\rightarrow\textbf{S}X(\textbf{K}Y)Z$、ここでは例2.11によって
$\rightarrow XZ((\textbf{K}Y)Z)$
$\rightarrow XZ(Y)$、ここでは$\textbf{K}YZ\rightarrow Y$によって
$\rightarrow XZY$
従って
$$\textbf{C}XYZ\triangleright_w XZY$$
練習問題2.13
(i) $\textbf{SIK}x\rightarrow\textbf{I}x(\textbf{K}x)
\rightarrow x(\textbf{K}x)
\rightarrow x\textbf{K}x$
(ii) $\textbf{SSK}xy
\rightarrow\textbf{S}x(\textbf{K}x)y
\rightarrow xy(\textbf{K}xy)
\rightarrow xyx$
(iii) $\textbf{S}(\textbf{SK})xy
\rightarrow\textbf{SK}y(xy)
\rightarrow\textbf{K}xy(yxy)
\rightarrow x(yxy)
\rightarrow xyxy$
(iv) $\textbf{S}(\textbf{KS})\textbf{S}xyz
\rightarrow\textbf{KS}x(\textbf{S}x)yz
\rightarrow\textbf{S}(\textbf{S}x)yz
\rightarrow\textbf{S}xz(yz)$
$\rightarrow xyz(zyz)
\rightarrow xyzzyz$
(v) $\textbf{SBBI}xy\rightarrow\textbf{BI}(\textbf{BI})xy
\rightarrow\textbf{I}x(\textbf{BI}x)y
\rightarrow x(\textbf{BI}xy)$
$\rightarrow x(\textbf{I}y(xy))
\rightarrow x(y(xy))
\rightarrow xyxy$