Haskellでラムダ計算:組み合わせ論理

組み合わせ論理とは、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)$$

BコンビネータのHaskellでの証明

-- K combinator
k :: a -> b -> a
k x _ = x

-- S combinator
s :: (a -> b -> c) -> (a -> b) -> a -> c
s x y z = x z (y z)

-- B combinaotr
b = s (k s) k

main = do
    let x = (*2)
    let y = (+3)
    let z = 4
    let lhs = b x y z
    let rhs = x (y z)
    putStrLn $ "B X Y Z =" ++ show lhs      -- B X Y Z = X (Y Z)
    putStrLn $ "X (Y Z) =" ++ show rhs

*Main> main
B X Y Z =14
X (Y Z) =14

例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$$

CコンビネータをHaskellで証明

-- C combinator
c = s (b b s)(k k)

main = do
    let x = \a b -> a - b
    let y = 1
    let z = 4
    let lhs = c x y z
    let rhs = x z y
    putStrLn $ "CXYZ =" ++ show lhs
    putStrLn $ "XZY  =" ++ show rhs

*Main> main
CXYZ =3
XZY  =3

練習問題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$

練習問題2.17

$$\textbf{B'}XYZ\ \triangleright_w Y(XZ)$$

$\textbf{B'}=\textbf{CB}$と置くと、
$\textbf{B'}XYZ
\rightarrow \textbf{CB}XYZ$
$\rightarrow \textbf{B}YXZ$　例2.12より$\textbf{CB}XY\rightarrow\textbf{B}YX$なので
$\rightarrow Y(XZ)$　例2.11より