SKIコンビネータでPLUS関数を導出する

概要

ラムダ計算からSKIコンビネータへの変換過程を示す必要があったので、書いた。 ラムダ計算とSKIコンビネータについて基本的なことを知っていることを前提としてる。

SKIコンビネータ

\[ \begin{eqnarray*} \S \fst \snd \thd & \rightarrow & \fst \thd (\snd\ \thd) \\ \K \fst \snd & \rightarrow & \fst \\ \I \fst & \rightarrow & \fst \end{eqnarray*} \]

チャーチ数

チャーチ数は関数によって自然数を表現するための符号化である。 ラムダ計算においては次の様に表記される。

\[ \begin{eqnarray*} \rm{SUCC} &:=& \lambda nfx. f\ (n\ f\ x) \\ 0 &:=& \lambda fx. x \\ 1 &:=& \lambda fx. f x \\ 2 &:=& \lambda fx. f (f x) \\ &\vdots& \end{eqnarray*} \]

チャーチ数はSKIコンビネータにおいては以下のように表記される。

\[ \begin{eqnarray*} \rm{SUCC} &=& \S\ (\B) \\ 0 &=& \S\ \K \\ 1 &=& \I \\ 2 &=& \S\ (\B)\ \I \\ &\vdots& \end{eqnarray*} \]

plus関数の導出

上記で定められたチャーチ数に対応する足し算をする2項演算子plusは ラムダ計算において次のように書ける。

\[ \begin{eqnarray*} \rm{PLUS} &:=& \lambda mnfx. m f (n f x) \end{eqnarray*} \]

上記のラムダ計算からSKIコンビネータへの変換過程を示す。

\[ \begin{eqnarray*} \rm{PLUS}\ m\ n\ f\ x &=& m\ f\ (n\ f\ x) \\ &=& \K\ (m\ f)\ x\ (n\ f\ x) \\ &=& \S\ (\K\ (m\ f))\ (n\ f)\ x \\ &=& \K\ \S\ (m\ f)\ (\K\ (m\ f))\ (n\ f)\ x \\ &=& \S\ (\K\ \S)\ \K\ (m\ f)\ (n\ f)\ x \\ &=& \K\ (\B)\ f\ (m\ f)\ (n\ f)\ x \\ &=& \S\ (\K\ (\B))\ m\ f\ (n\ f)\ x \\ &=& \S\ (\S\ (\K\ (\B))\ m)\ n\ f\ x \\ &=& \K\ \S\ m\ (\S\ (\K\ (\B))\ m)\ n\ f\ x \\ &=& \S\ (\K\ \S)\ (\S\ (\K\ (\B)))\ m\ n\ f\ x \\ \rm{PLUS} &=& \S\ (\K\ \S)\ (\S\ (\K\ (\B))) \end{eqnarray*} \]