0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

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

Last updated at Posted at 2024-12-19

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

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?