SKIコンビネータ計算のソースを表示

<!--
'''SKIコンビネータ計算''' is a [[model of computation|computational system]] that may be perceived as a reduced version of untyped [[lambda calculus]]. It can be thought of as a computer programming language, though it is not useful for writing software. Instead, it is important in the mathematical theory of [[algorithm|algorithms]] because it is an extremely simple [[Turing complete]] language.
-->
'''SKIコンビネータ計算'''は型無し[[ラムダ計算]]を単純化した、ひとつの[[計算モデル]]である。このモデルは、ある種のプログラミング言語と考えることができるが、人間によるソースコードの記述には適さない（[[難解プログラミング言語]]には時折採用される）。その代わり、このモデルは非常に単純な[[チューリング完全]]な言語であるため、[[アルゴリズム]]の数学理論においては重要である。また[[関数型言語]]を実行する[[抽象機械]]のモデルとして使っている例もある<ref>D. A. Turner ''A new implementation technique for applicative languages''</ref>。

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

== 素朴な説明 ==
<!--
Informally, and using programming language jargon, a tree (''xy'') can be thought of as a "function" ''x'' applied to an 
"argument" ''y''. When "evaluated" (''i.e.'', when the function is "applied" to the argument), the tree "returns a value", ''i.e.'', transforms into another tree. Of course, all three of the "function", the "argument" and the "value" are either combinators, or binary trees, -- remove: and if they are binary trees they too may be thought of as functions whenever the need arises. --
-->
非形式的には、またプログラミング言語の[[ジャーゴン]]として、木 (''xy'') は“関数” ''x'' に“引数” ''y''を適用したものと考えられる。評価されるとき（すなわち関数に引数を“適用”するとき）、木は“値を返す”、すなわち別の木に変形する。当然“関数”も“引数”も“値”もそれぞれ葉もしくは二分木である。簡単のために関数適用は左結合であるものとし、無駄な括弧は省略するのが普通である。このようにしても曖昧性はない。

<!--
The '''evaluation''' operation is defined as follows:

(''x'', ''y'', and ''z'' represent expressions made from the functions '''S''', '''K''', and '''I''', and set values):

'''I''' returns its argument:
:'''I'''''x'' = ''x''

'''K''', when applied to any argument ''x'', yields a one-argument constant function '''K'''''x'' , which, when applied to any argument, returns ''x'':
:'''K'''''xy'' = ''x''

'''S''' is a substitution operator.  It takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third.  More clearly:
:'''S'''''xyz'' = ''xz''(''yz'')
-->
'''評価'''演算は次のように定義される：

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

'''I'''('''I'''dentity combinator) は引数を返す：
: '''I'''''x'' = ''x''

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

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

<!--
Example computation: '''SKSK''' evaluates to '''KK'''('''SK''') by the '''S'''-rule. Then if we evaluate '''KK'''('''SK'''), we get '''K''' by the '''K'''-rule.  As no further rule can be applied, the computation halts here. 

Note that, for all trees ''x'' and all trees ''y'', '''SK'''''xy'' will always evaluate to ''y'' -- remove: in two steps, '''K'''''y''(''xy'') = ''y'', so the ultimate result of evaluating '''SK'''''xy'' will always equal the result of evaluating ''y''. -- We say that '''SK'''''x'' and '''I''' are "functionally equivalent" because they always yield the same result when applied to any ''y''.

-- remove: Note that from these definitions it can be shown that SKI calculus is not the minimum system that can fully perform the computations of lambda calculus, as -- all occurrences of '''I''' in any expression can be replaced by ('''SKK''') or ('''SKS''') or ('''SK''' whatever) and the resulting expression will yield the same result. So the "'''I'''" is merely [[syntactic sugar]].

In fact, it is possible to define a complete system using only one combinator. An example is Chris Barker's [[Iota and Jot|iota]] combinator, defined as follows:
: ι''x'' = ''x'''''SK'''
-->
計算の例： '''SKSK''' は '''S'''-規則によって '''KK'''('''SK''') に評価される。次に '''KK'''('''SK''') は '''K'''-規則によって '''K''' に評価される。これ以上適用できないので、ここで計算は終了する。

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

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

== 形式的な定義 ==
SKIコンビネータ論理の項は次の規則により帰納的に定義される：
# 定数記号（ここでは'''S'''、'''K'''、'''I'''）及び変数記号は項である。この形の項を原子（atom）という。
# M と N が項ならば, (MN)は項である。この形の項を適用（application）という。
# 以上より項とわかるもののみを項という。
変数記号を含まない項を閉項といい、'''SKI'''のみから構成される項を結合子（コンビネータ）という。適用は左結合であるものとし、括弧を省略するのが普通である。SKIコンビネータ計算は次の簡約規則
: <math>\boldsymbol S MNR\to MR\left(NR\right) </math>
: <math>\boldsymbol K MN\to M </math>
: <math>\boldsymbol I M\to M</math>
からなる[[項書換え系]]である。矢印の左辺の形をリデックス、右辺の形をコントラクタムという。矢印によって移る項の変形をweak簡約という。簡約関係の同値閉包をweak同値性といい、普通、等号を用いて表す。

==ラムダ計算との関係==
任意のコンビネータ項に対して、それと外延的に等価かつ同じ自由変数を持つラムダ項が存在する。これは、コンビネータ項に現れるすべての定数記号を、
: '''S''' = &lambda;''xyz''.''xz''(''yz'')
: '''K''' = &lambda;''xy''.''x''
: '''I''' = &lambda;''x''.''x''
と置き換えれば良いから明らかである。一方任意のラムダ項に対して、それと外延的に等価かつ同じ自由変数を持つコンビネータ項が存在する。これは、命題論理におけるヒルベルトスタイルと自然演繹スタイルの証明系が等価であることと対応する（[[演繹定理]]）。

==SKI表現==
=== 自己適用と再帰 ===
<!-- expressionは式, functionは関数であるが、前節の定義に合せて項と訳す。 -->
<!--
'''SII''' is an expression that takes an argument and applies that argument to itself:
: '''SII'''α = '''I'''α('''I'''α) = αα
-->
'''SII''' は引数をそれ自身に適用させる項である：
: '''SII'''α = '''I'''α('''I'''α) = αα
この項を用いて '''SII'''('''SII''') と表される項は正規形を持たない。すなわち簡約が終了しないという性質を持つ。

'''S'''('''K'''('''SII'''))('''S'''('''S'''('''KS''')'''K''')('''K'''('''SII'''))) は第一引数の不動点を与える項であり、'''Y'''で表す。Yコンビネータは次を満たす：
: '''Y'''x = x('''Y'''x)
このような性質を持つ閉項を[[不動点コンビネータ]]といい、不動点コンビネータを用いることで再帰的呼び出しを含む項を定義できる。詳細は[[不動点コンビネータ]]を参照。

=== 式の逆転 ===
'''S'''('''K'''('''SI'''))'''K''' は次にくる2つの項を逆転させる:
: '''S'''('''K'''('''SI'''))'''K'''αβ →
: '''K'''('''SI''')α('''K'''α)β →
: '''SI'''('''K'''α)β →
: '''I'''β('''K'''αβ) →
: '''I'''βα
: βα

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

'''T''' と '''F''' を合せてChurch booleanという。これは具体的に次のように定義できる：
: '''T''' = '''K'''
: '''F''' = '''SK'''
: '''K'''''xy'' = ''x''
: '''SK'''''xy'' = '''K'''''y(xy)'' = ''y''

<!--
Once true and false are defined, all Boolean logic can be implemented in terms of ''if-then-else'' structures.
-->
真と偽を定義すれば、今やブール論理の全ての演算は ''if-then-else'' 構造によって実装できる。

入力となるChurch booleanの否定を得るには、入力に '''F''' と '''T''' を順に適用すればよい。したがって '''NOT''' は次のように定義できる：
: '''NOT''' = '''S'''('''SI'''('''KF'''))('''KT''')
: '''NOT'''x = '''S'''('''SI'''('''KF'''))('''KT''')x = '''SI'''('''KF''')x('''KT'''x) = '''I'''x('''KF'''x)('''KT'''x) = x'''FT'''

入力となる2つのChurch booleanの論理和を得るには、入力1に '''T''' と入力2を順に適用すればよい。したがって '''OR''' は次のように定義できる：
: '''OR''' = '''SI'''('''KT''')
: '''OR'''xy = '''I'''x('''KT'''x)y = x'''T'''y

入力となる2つのChurch booleanの論理積を得るには、入力1に入力2と '''F''' を順に適用すればよい。したがって '''AND''' は次のように定義できる：
: '''AND''' = '''SS'''('''K'''('''KF'''))
: '''AND'''xy = '''S'''x('''K'''('''KF''')x)y = xy('''KF'''y) = xy'''F'''

== 直観主義論理との関係 ==
<!--
The combinators '''K''' and '''S''' correspond to two well-known axioms of [[sentential logic]]:

'''AK''': ''A'' <math>\to</math> (''B'' <math>\to</math> ''A'')<br>
'''AS''': (''A'' <math>\to</math> (''B'' <math>\to</math> ''C'')) <math>\to</math> ((''A'' <math>\to</math> ''B'') <math>\to</math> (''A'' <math>\to</math> ''C''))
-->
コンビネータ '''K''' および '''S''' は、よく知られた次の命題論理の公理図式と対応する：

'''AK''': ''A'' <math>\to</math> (''B'' <math>\to</math> ''A''),<br>
'''AS''': (''A'' <math>\to</math> (''B'' <math>\to</math> ''C'')) <math>\to</math> ((''A'' <math>\to</math> ''B'') <math>\to</math> (''A'' <math>\to</math> ''C'')).

<!--
Function application corresponds to the rule [[modus ponens]]:

'''MP''': from ''A'' and ''A'' <math>\to</math> ''B'', infer ''B''.
-->
関数適用は推論規則[[モーダスポネンス]]と対応する：

'''MP''': <math>A\to B,A\vdash B</math>

<!--
The axioms '''AK''' and '''AS''', and the rule '''MP''' are complete for the implicational fragment of [[intuitionistic logic]]. In order for combinatory logic to have as a model:
*The [[implicational propositional calculus|implicational fragment]] of [[classical logic]], would require the combinatory analog to the [[law of excluded middle]], ''e.g.'', [[Peirce's law]];
*[[sentential logic|Complete classical logic]], would require the combinatory analog to the sentential axiom '''F''' <math>\to</math> ''A''.
-->
公理 '''AK, AS''' 及び推論規則 '''MP''' は、[[直観主義論理|直観主義命題論理]]の[[含意断片]]に対して健全かつ完全である。この体系に爆発原理 '''F''' → ''A'' と[[排中律]]に類する規則（例：[[パースの法則]]）を追加したものは古典命題論理と対応する。

== 関連項目 ==
* [[コンビネータ論理]]
* [[B,C,K,Wシステム]]
* [[不動点コンビネータ]]
* [[ラムダ計算]]
* [[関数型言語]]
* [[Lazy K]] プログラミング言語
* [[Unlambda]] プログラミング言語
* {{仮リンク|To Mock a Mockingbird|en|To_Mock_a_Mockingbird}}
* [[SKK]] - 名称がSKK=Iともかけられている。

== 脚注 ==

=== 出典 ===
{{Reflist}}

== 参考文献 ==
* {{Cite book |last=Smullyan |first=Raymond M. |author-link=:en:Raymond Smullyan |title=[[:en:To Mock a Mockingbird|To mock a mocking bird and other logic puzzles : including an amazing adventure in combinatory logic]] |edition=1st |date=1985 |publisher=Knopf |isbn=0-394-53491-3 |location=New York |oclc=11725613}}
** {{Cite book |和書 |author=レイモンド・スマリヤン |author-link=レイモンド・スマリヤン |title=数学パズルものまね鳥をまねる : 愉快なパズルと結合子論理の夢の鳥物語 |date=1998年5月 |publisher=森北出版 |isbn=4-627-01901-7 |translator=阿部剛久、黒沢俊雄、福島修身、山口裕 |oclc=587130399}}
* {{Cite book |last=Smullyan |first=Raymond M. |author-link=:en:Raymond Smullyan |title=Diagonalization and self-reference |date=1994 |publisher=Clarendon Press |isbn=0-19-853450-7 |location=Oxford |oclc=30666843}}
* {{Cite book |和書 |author=古森雄一 |author-link=古森雄一 |title=現代数理論理学序説 |date=2010 |publisher=日本評論社 |isbn=978-4-535-78556-4 |author2=小野寛晰 |author2-link=小野寛晰 |oclc=703471604}}

== 外部リンク ==
* O'Donnell, Mike "[http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/Formal_Organization_of_Knowledge/Examples/combinator_calculus/ The SKI Combinator Calculus as a Universal System.]"
* Keenan, David C. (2001) "[http://dkeenan.com/Lambda/index.htm To Dissect a Mockingbird.]"
* Rathman, Chris, "[http://www.angelfire.com/tx4/cus/combinator/birds.html Combinator Birds.]"
* {{Wayback|url=http://cstein.kings.cam.ac.uk/~chris/combinators.html|title=Drag 'n' Drop Combinators (Java Applet)|date=20081029051502}}.

[[Category:ラムダ計算]]
[[Category:コンビネータ論理]]