blog.monophile.net

Takaaki Yamamoto

東京工業大学において計算機科学と応用数学を学び、 情報科学芸術大学院大学[IAMAS]においてメディア表現を専攻し修了。 digitiminimi Inc. において、インフラエンジニアとして生計をたててている。

各種環境の構築と管理を承ります。

  • 仮想環境: Openstack, GCP, AWS, Azure, ...
  • アプリケーション: WordPress, GitLab, Redmine, ...

List

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

\[ \def\fst{[1]} \def\snd{[2]} \def\thd{[3]} \def\S{\rm S} \def\K{\rm K} \def\I{\rm I} \def\B{\S\ (\K\ \S)\ \K} \]

概要

ラムダ計算から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*} \]