SKIコンビネータ リンク等まとめ
SKIコンビネータは一手書き換えによるチューリング完全な計算モデルの一つで、S,K,I,(,)の5つの記号のみでアルゴリズムを記述できるものです。
計算機科学や数理論理学の文脈で非常に重要な役割を果たし、同じく一手書き換え系であるラムダ計算と深く関係します。
詳しくは以下のwikiをご覧ください。
便利なツール
以下のSKI combinator calculatorで挙動を確かめることができます。
らむだフレンズは非常に有用なツールで、ラムダ式をSKIコンビネータに翻訳する機能がついています。
ラムダ計算との対応
SKIコンビネータはラムダ計算から自由変数を取り除いたものです。
SとKはそれぞれ、束縛変数を内部に持つ場合と持たない場合の関数適用に対応します。
ヒルベルト流論理との対応
カリーハワード対応により、ヒルベルト流命題論理と深く関係します。
combinator bird
スマリヤンは有用なコンビネータに鳥の名前を付けています。
以下のリンクでその一覧をみることができます。
（スマリヤンはいろんなコンビネータに独特な名前を付けています）
この中で特に重要なのがヴィレオと呼ばれるコンビネータです。
ヴィレオ$${V}$$は$${Vxyz=zxy}$$のように振る舞います。
不動点
コンビネータ$${x,y}$$が$${xy=y}$$を満たすとき、$${y}$$は$${x}$$の不動点であるといいます。
不動点コンビネータ
コンビネータ$${\theta}$$は$${x(\theta x)=\theta x}$$となる場合、$${\theta}$$を不動点コンビネータ(賢者コンビネータ)といいます。
不動点コンビネータを使うと再帰を行うことができます。
預言者コンビネータ
コンビネータ$${O}$$が$${Oxy=y(xy)}$$という性質を持っているとき、$${O}$$は預言者コンビネータであるといいます。
預言者コンビネータの不動点は賢者コンビネータになります。
二重不動点・二重賢者対
対$${y_{1},y_{2}}$$は、$${x_{1}y_{1}y_{2}=y_{1}}$$かつ$${x_{2}y_{1}y_{2}=y_{2}}$$ならば、対$${x_{1},x_{2}}$$の二重不動点といいます。
全ての対$${x_{1},x_{2}}$$が二重不動点を持つとき、その体系は弱二重不動点性を持つと言います。
すべての$${x}$$と$${y}$$に対して、対$${(\theta_{1}xy,\theta_{2}xy)}$$が$${(x,y)}$$の二重不動点になるような対$${(\theta_{1},\theta_{2})}$$を二重賢者対と言います。
二重賢者対が存在するとき、その体系は強二重不動点性を持つと言います」。
同様に二重預言コンビネータを考えることができます。
論理コンビネータ
真と偽に対応するコンビネータを導入しましょう。
$${t}$$を$${K}$$であるとし、$${f}$$を$${KI}$$であるとします。
否定を表す$${N}$$は$${N:=Vft}$$で導入できます。
同様に、連言は$${c:=Rf}$$、選言は$${d:=Tt}$$、含意は$${i:=Rt}$$、同値命題は$${e:=CSN}$$とします。
ただし、$${Rxyz=yzx}$$、$${Txy=yx}$$、$${Cxyz=xzy}$$とします。
算術コンビネータ
0のエンコードとして$${I}$$を、後者関数として$${suc:=Vf}$$を用いると、
$${I,suc(I),suc(suc(I))…}$$は自然数として扱えます。
ゼロ試験子、原始再帰作用素、μ再帰作用素を作っておけば、SKIで直観的にプログラムができるようになると思います。
参考文献：
『スマリヤン 数理論理学講義 下巻』
著 レイモンド・M・スマリヤン
監訳 田中一之
訳 川辺治之
この記事が参加している募集
この記事が気に入ったらサポートをしてみませんか？