SKIコンビネータ計算

SKIコンビネータ計算は型無しラムダ計算を単純化した、ひとつの計算モデルである。このモデルは、ある種のプログラミング言語と考えることができるが、人間によるソースコードの記述には適さない（難解プログラミング言語には時折採用される）。その代わり、このモデルは非常に単純なチューリング完全な言語であるため、アルゴリズムの数学理論においては重要である。また関数型言語を実行する抽象機械のモデルとして使っている例もある^[1]。

ラムダ計算におけるあらゆる演算は、SKIにおいて3つの定数記号S, KおよびI（これらをコンビネータと呼ぶ）および変数記号によって表現できる。2引数の関数適用演算のみを持つ形式言語の構文木と考えれば、定数記号と変数記号を葉とする二分木と捉えることもできる。 実際には、 I はモデルを簡単にするために導入されたものであり、SKIシステムを展開するにはSとKの2つで十分である。

素朴な説明[編集]

非形式的には、またプログラミング言語のジャーゴンとして、木 (xy) は“関数” x に“引数” yを適用したものと考えられる。評価されるとき（すなわち関数に引数を“適用”するとき）、木は“値を返す”、すなわち別の木に変形する。当然“関数”も“引数”も“値”もそれぞれ葉もしくは二分木である。簡単のために関数適用は左結合であるものとし、無駄な括弧は省略するのが普通である。このようにしても曖昧性はない。

評価演算は次のように定義される：

（x、y および z は任意の式とする）

I(Identity combinator) は引数を返す：

Ix = x

K(Constant (独Konstant) combinator) にxだけを適用した場合、任意の引数に対してxを返す1引数の定数関数 Kxを得る：

Kxy = x

S(Substitution combinator) は3つの引数を取って、1つ目の引数に3つ目の引数を適用し、その結果に2つ目の引数に3つ目の引数を適用した結果を適用する。簡単に：

Sxyz = xz(yz)

計算の例： SKSK は S-規則によって KK(SK) に評価される。次に KK(SK) は K-規則によって K に評価される。これ以上適用できないので、ここで計算は終了する。

任意の木 x および y について、 SKxy はいつでも y と評価されることがわかる。すなわち SKx と I は“関数として同値”（外延的同値）であると考えられる。任意の式のすべての I の出現を (SKK) や (SKS) あるいは (SK[任意の式]) に置き換えることができ、結果の式は元の式と外延的に同値である。すなわち I は 糖衣構文にすぎない。

実は、ただ1つのコンビネータを用いて完全な体系を定義することも可能である。1つの例としてChris Bakerによるιコンビネータがある。定義は次の通り：

ιx = xSK

形式的な定義[編集]

SKIコンビネータ論理の項は次の規則により帰納的に定義される：

1. 定数記号（ここではS、K、I）及び変数記号は項である。この形の項を原子（atom）という。
2. M と N が項ならば, (MN)は項である。この形の項を適用（application）という。
3. 以上より項とわかるもののみを項という。

変数記号を含まない項を閉項といい、SKIのみから構成される項を結合子（コンビネータ）という。適用は左結合であるものとし、括弧を省略するのが普通である。SKIコンビネータ計算は次の簡約規則

${\displaystyle {\boldsymbol {S}}MNR\to MR\left(NR\right)}$

${\displaystyle {\boldsymbol {K}}MN\to M}$

${\displaystyle {\boldsymbol {I}}M\to M}$

からなる項書換え系である。矢印の左辺の形をリデックス、右辺の形をコントラクタムという。矢印によって移る項の変形をweak簡約という。簡約関係の同値閉包をweak同値性といい、普通、等号を用いて表す。

ラムダ計算との関係[編集]

任意のコンビネータ項に対して、それと外延的に等価かつ同じ自由変数を持つラムダ項が存在する。これは、コンビネータ項に現れるすべての定数記号を、

S = λxyz.xz(yz)

K = λxy.x

I = λx.x

と置き換えれば良いから明らかである。一方任意のラムダ項に対して、それと外延的に等価かつ同じ自由変数を持つコンビネータ項が存在する。これは、命題論理におけるヒルベルトスタイルと自然演繹スタイルの証明系が等価であることと対応する（演繹定理）。

SKI表現[編集]

自己適用と再帰[編集]

SII は引数をそれ自身に適用させる項である：

SIIα = Iα(Iα) = αα

この項を用いて SII(SII) と表される項は正規形を持たない。すなわち簡約が終了しないという性質を持つ。

S(K(SII))(S(S(KS)K)(K(SII))) は第一引数の不動点を与える項であり、Yで表す。Yコンビネータは次を満たす：

Yx = x(Yx)

このような性質を持つ閉項を不動点コンビネータといい、不動点コンビネータを用いることで再帰的呼び出しを含む項を定義できる。詳細は不動点コンビネータを参照。

式の逆転[編集]

S(K(SI))K は次にくる2つの項を逆転させる:

S(K(SI))Kαβ →

K(SI)α(Kα)β →

SI(Kα)β →

Iβ(Kαβ) →

Iβα

βα

ブール論理[編集]

SKIコンビネータ計算ではブール論理の計算が可能である。これは、次を満たす真（T）または偽（F）を表す閉項によって実現される：

Txy = x

Fxy = y

T と F を合せてChurch booleanという。これは具体的に次のように定義できる：

T = K

F = SK

Kxy = x

SKxy = Ky(xy) = y

真と偽を定義すれば、今やブール論理の全ての演算は if-then-else 構造によって実装できる。

入力となるChurch booleanの否定を得るには、入力に F と T を順に適用すればよい。したがって NOT は次のように定義できる：

NOT = S(SI(KF))(KT)

NOTx = S(SI(KF))(KT)x = SI(KF)x(KTx) = Ix(KFx)(KTx) = xFT

入力となる2つのChurch booleanの論理和を得るには、入力1に T と入力2を順に適用すればよい。したがって OR は次のように定義できる：

OR = SI(KT)

ORxy = Ix(KTx)y = xTy

入力となる2つのChurch booleanの論理積を得るには、入力1に入力2と F を順に適用すればよい。したがって AND は次のように定義できる：

AND = SS(K(KF))

ANDxy = Sx(K(KF)x)y = xy(KFy) = xyF

直観主義論理との関係[編集]

コンビネータ K および S は、よく知られた次の命題論理の公理図式と対応する：

AK: A ${\displaystyle \to }$ (B ${\displaystyle \to }$ A),
AS: (A ${\displaystyle \to }$ (B ${\displaystyle \to }$ C)) ${\displaystyle \to }$ ((A ${\displaystyle \to }$ B) ${\displaystyle \to }$ (A ${\displaystyle \to }$ C)).

関数適用は推論規則モーダスポネンスと対応する：

MP: ${\displaystyle A\to B,A\vdash B}$

公理 AK, AS 及び推論規則 MP は、直観主義命題論理の含意断片に対して健全かつ完全である。この体系に爆発原理 F → A と排中律に類する規則（例：パースの法則）を追加したものは古典命題論理と対応する。

関連項目[編集]

• コンビネータ論理
• B,C,K,Wシステム
• 不動点コンビネータ
• ラムダ計算
• 関数型言語
• Lazy K プログラミング言語
• Unlambda プログラミング言語
• To Mock a Mockingbird（英語版）
• SKK - 名称がSKK=Iともかけられている。

脚注[編集]

出典[編集]

参考文献[編集]

• Smullyan, Raymond M. (1985). To mock a mocking bird and other logic puzzles : including an amazing adventure in combinatory logic (1st ed.). New York: Knopf. ISBN 0-394-53491-3. OCLC 11725613 
  • レイモンド・スマリヤン 著、阿部剛久、黒沢俊雄、福島修身、山口裕 訳『数学パズルものまね鳥をまねる : 愉快なパズルと結合子論理の夢の鳥物語』森北出版、1998年5月。ISBN 4-627-01901-7。OCLC 587130399。 
• Smullyan, Raymond M. (1994). Diagonalization and self-reference. Oxford: Clarendon Press. ISBN 0-19-853450-7. OCLC 30666843 
• 古森雄一、小野寛晰『現代数理論理学序説』日本評論社、2010年。ISBN 978-4-535-78556-4。OCLC 703471604。 

外部リンク[編集]

• O'Donnell, Mike "The SKI Combinator Calculus as a Universal System."
• Keenan, David C. (2001) "To Dissect a Mockingbird."
• Rathman, Chris, "Combinator Birds."
• Drag 'n' Drop Combinators (Java Applet) - ウェイバックマシン（2008年10月29日アーカイブ分）.