コンビネータ論理のソースを表示

<!--
{{distinguish2|[[combinational logic]], a topic in digital electronics}}

'''Combinatory logic''' is a notation introduced by [[Moses Schönfinkel]] and [[Haskell Curry]] to eliminate the need for [[Variable (mathematics)|variables]] in [[mathematical logic]].  It has more recently been used in [[computer science]] as a theoretical model of [[computation]] and also as a basis for the design of [[functional programming languages]]. It is based on '''combinators'''. A combinator is a [[higher-order function]] that uses only function application and earlier defined combinators to define a result from its arguments.
-->
'''コンビネータ論理'''（{{lang-en-short|combinatory logic}}、組み合わせ論理）は、{{仮リンク|モイセイ・シェインフィンケリ|ru|Шейнфинкель, Моисей Эльевич|en|Moses Schönfinkel}}（{{lang-ru-short|Моисей Эльевич Шейнфинкель}}、{{lang-en-short|Moses Ilyich Schönfinkel}}）と[[ハスケル・カリー]]（{{lang-en-short|Haskell Brooks Curry}}）によって、[[数理論理学|記号論理]]での[[変数 (数学)|変数]]を消去するために導入された記法である。最近では、[[計算機科学]]において計算の理論的モデルで利用されてきている。また、[[関数型言語|関数型プログラミング言語]]の理論（意味論など）や実装にも応用がある。

コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている[[高階関数]]、'''コンビネータ'''に基づいている。

== 数学におけるコンビネータ論理 ==
<!--
Combinatory logic was originally intended as a 'pre-logic' that would clarify the role of [[quantifier|quantified variables]] in logic, essentially by eliminating them. Another way of eliminating quantified variables is [[Willard Van Orman Quine|Quine's]] [[predicate functor logic]]. While the [[expressive power]] of combinatory logic typically exceeds that of [[一階述語論理|first-order logic]], the expressive power of [[predicate functor logic]] is identical to that of first order logic ([[#Quine 1960 1966|Quine 1960, 1966, 1976]]).

-->
コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法には[[ウィラード・ヴァン・オーマン・クワイン|クワイン]]の[[述語関手論理]]がある。コンビネータ論理の表現力は[[一階述語論理]]を超える一方、述語関手論理の表現力は一階述語論理と同等である。
<!--
The original inventor of combinatory logic, [[Moses Schönfinkel]], published nothing on combinatory logic after his original 1924 paper, and largely ceased to publish after [[Joseph Stalin]] consolidated his power in 1929. Curry rediscovered the combinators while working as an instructor at the [[Princeton University]] in late 1927.<ref name="Seldin 2006">{{cite journal|last=Seldin|first=Jonathan|title=The Logic of Curry and Church}}</ref> In the latter 1930s, [[アロンゾ・チャーチ]] and his students at [[プリンストン大学|Princeton]] invented a rival formalism for functional abstraction, the [[ラムダ計算|lambda calculus]], which proved more popular than combinatory logic. The upshot of these historical contingencies was that until theoretical computer science began taking an interest in combinatory logic in the 1960s and 70s, nearly all work on the subject was by [[ハスケル・カリー]] and his students, or by [[Robert Feys]] in [[Belgium]]. Curry and Feys (1958), and Curry ''et al.'' (1972) survey the early history of combinatory logic. For a more modern parallel treatment of combinatory logic and the lambda calculus, see [[Henk Barendregt|Barendregt]] correct person?(1984), who also reviews the [[モデル理論|models]] [[Dana Scott]] devised for combinatory logic in the 1960s and 70s.
-->

コンビネータ論理の最初の発明者である{{仮リンク|モイセイ・シェインフィンケリ|ru|Шейнфинкель, Моисей Эльевич|en|Moses Schönfinkel}}は、1924年の論文以降それについて何も出版していない（[[ヨシフ・スターリン]]が1929年に権力を確固なものとしてからはほとんど出版を行なっていない）。1927年後半、カリーは[[プリンストン大学]]の講師として働いているときにコンビネータを再発見した。<ref name="Seldin 2006">{{cite journal|last=Seldin|first=Jonathan|title=The Logic of Curry and Church}}</ref>1930年代後半、[[アロンゾ・チャーチ]]とプリンストン大学の彼の教え子が、[[ラムダ計算]]というライバルとなる関数抽象の形式化を考案し、コンビネータ論理より人気を博すこととなった。こうした歴史的偶然のために、[[理論計算機科学]]が60〜70年代にコンビネータ論理に関心を持ち始めるまで、この分野のほとんどすべての業績は、ほとんどカリーとその教え子、もしくはベルギーの{{仮リンク|ロベール・フェイ|en|Robert Feys}}によるものであった。Curry and Feys (1958) および Curry et al. (1972)  はコンビネータ論理の初期の歴史についてのサーベイ論文である。より最近のコンビネータ論理とラムダ計算の比較については {{仮リンク|ヘンク・バレンドレクト|nl|Henk Barendregt|en|Henk Barendregt|label=Barendregt}} (1984) を参照されたい（[[デイナ・スコット]]が60〜70年代に考案したコンビネータ論理のためのモデル理論についても触れている）。<!-- correct person? -->

<!-- This section needs a LOT of filling in!!! -->

== 計算機科学におけるコンビネータ論理 ==
<!--
In [[計算機科学|computer science]], combinatory logic is used as a simplified model of [[computation]], used in [[computability theory]] and [[proof theory]]. Despite its simplicity, combinatory logic captures many essential features of computation.

Combinatory logic can be viewed as a variant of the [[ラムダ計算|lambda calculus]], in which lambda expressions (representing functional abstraction) are replaced by a limited set of ''combinators'', primitive functions from which [[bound variable]]s are absent. It is easy to transform lambda expressions into combinator expressions, and combinator reduction is much simpler than lambda reduction. Hence combinatory logic has been used to model some [[non-strict programming language|non-strict]] [[functional programming]] languages and [[graph reduction machine|hardware]]. The purest form of this view is the programming language [[Unlambda]], whose sole primitives are the S and K combinators augmented with character input/output. Although not a practical programming language, Unlambda is of some theoretical interest.

Combinatory logic can be given a variety of interpretations. Many early papers by Curry showed how to translate axiom sets for conventional logic into combinatory logic equations (Hindley and Meredith 1990). Dana Scott in the 1960s and 70s showed how to marry [[モデル理論|model]] and combinatory logic.
-->
計算機科学において（[[計算可能性理論]]や[[証明論]]で）は、コンビネータ論理は計算を単純化したモデルとして使われる。単純にもかかわらず、コンビネータ論理は計算の本質的な特徴をとらえている。

コンビネータ論理は[[ラムダ計算]]の変種としても見ることができる。ラムダ式(ラムダ抽象)は、[[自由変数と束縛変数|束縛変数]]のない原始的な関数「コンビネータ」の有限集合によって置き換えられる。ラムダ式をコンビネータ式に変換するのは簡単であり、またコンビネータの簡約はラムダの簡約よりもシンプルである。したがってコンビネータ論理は非正格関数型言語やGraph reduction machineのモデルとして使われている。もっとも純粋な形は、唯一のプリミティブが入出力のために拡張されたSとKのコンビネータの、[[Unlambda]]というプログラミング言語である。実用的なプログラミング言語ではないが、Unlambdaは理論的な関心がある。

コンビネータ論理は解釈の多様性を与えられる。カリーによる論文では、どのように従来の論理のための公理をコンビネータ論理の等式にするかを示した。[[デイナ・スコット]]は、60,70年代にどのようにしてモデル理論とコンビネータ論理を結びつけるかを示した。

== ラムダ計算の概要 ==
{{main|ラムダ計算}}
<!--
The lambda calculus is
concerned with objects called ''lambda-terms'', which are strings of
symbols of one of the following forms:
-->
ラムダ計算は、ラムダ項と呼ばれる以下のような形の記号の列に関係している。

*       ''v''
*       ''λv''.''E1''
*       (''E1'' ''E2'')
<!--
where ''v'' is a variable name drawn from a predefined infinite set of
variable names, and ''E1'' and ''E2'' are lambda-terms.
-->
''v''は予め定義された変数の名前の無限集合から引き出された変数名で、''E1''と''E2''はラムダ項である。
<!--
Terms of the form ''λv.E1'' are called ''abstractions''. The variable ''v'' is
called the [[formal parameter]] of the abstraction, and ''E1'' is the ''body''
of the abstraction.  The term ''λv.E1'' represents the function which, applied
to an argument, binds the formal parameter ''v'' to the argument and then
computes the resulting value of ''E1''---that is, it returns ''E1'', with
every occurrence of ''v'' replaced by the argument.
-->
''λv.E1''の形の項は「抽象」と呼ばれる。''v''はその抽象の仮引数、''E1''は本体と呼ばれる。''λv.E1''という項は、引数に適用されると''v''をその値に束縛し、''E1''の結果の値を評価する。つまり、E1の中にある''v''をその引数で置き換えたものを返す。
<!--
Terms of the form ''(E1 E2)'' are called ''applications''. Applications model
function invocation or execution: the function represented by ''E1'' is to be
invoked, with ''E2'' as its argument, and the result is computed. If ''E1''
(sometimes called the ''applicand'') is an abstraction, the term may be
''reduced'': ''E2'', the argument, may be substituted into the body of ''E1''
in place of the formal parameter of ''E1'', and the result is a new lambda
term which is ''equivalent'' to the old one. If a lambda term contains no
subterms of the form ''((λv.E1) E2)'' then it cannot be reduced, and is said to
be in [[Beta normal form|normal form]].
-->
''(E1 E2)''の形の項は''適用''と呼ばれる。適用は関数の呼び出しもしくは実行を作る:''E1''という関数が、''E2''という引数で呼び出されると、その結果が計算される。もし''E1''(ときどき''applicand''と呼ばれる)がラムダ抽象なら、その項は簡約されるかもしれない: 引数E2は、''E1''の仮引数の場所に置き換えられ、''同値''な新しい項が結果になる。もし、ラムダ項が''((λv.E1) E2)''の形の項を含まないのならば、それは簡約されず、[[β正規形]]と呼ばれる。
<!--
The expression ''E''[''v'' := ''a''] represents the result of taking the term ''E'' and replacing all free occurrences of ''v'' with ''a''.  Thus we write
-->
''E''[''v'' := ''a'']は、''E''の''v''の[[自由変数と束縛変数|自由変数]]としての出現をすべて''a''で置き換えた結果を表現する。したがって、

:((''λv.E'')''a'') => ''E''[''v'' := ''a'']
<!--
By convention, we take ''(a b c d ... z)'' as short for ''(...(((a b) c) d) ... z)''. (i.e., application is [[Associative#Non-associativity|left associative]].)
-->
伝統的に、''(a b c d ... z)''を''(...(((a b) c) d) ... z)''の省略として表記する。(i.e. 適用は左結合である)
<!--
The motivation for this definition of reduction is that it captures
the essential behavior of all mathematical functions. For example,
consider the function that computes the square of a number. We might
write
-->
このような定義をするのは、すべての数学的の根本的な振る舞いを捉えているからである。例えば、ある数の平方を求める関数を考えて欲しい。英語ならこのように書くかもしれない。

:The square of ''x'' is ''x''*''x''
<!--
(Using "*" to indicate multiplication.)  ''x'' here is the [[formal parameter]] of the function. To evaluate the square for a particular
argument, say 3, we insert it into the definition in place of the formal param model eter:
-->
(「*」を乗算の表記に用いている。) ''x''は関数の仮引数である。特定の引数の平方を求めるために、3をあてると、仮引数の場所に3を入れる:

:The square of 3 is 3*3
<!--
To evaluate the resulting expression 3*3, we would have to resort to
our knowledge of multiplication and the number 3. Since any
computation is simply a composition of the evaluation of suitable
functions on suitable primitive arguments, this simple substitution
principle suffices to capture the essential mechanism of computation.
Moreover, in the lambda calculus, notions such as '3' and '*' can be
represented without any need for externally defined primitive
operators or constants. It is possible to identify terms in the
lambda calculus, which, when suitably interpreted, behave like the
number 3 and like the multiplication operator, q.v. [[Church encoding]].
-->
3*3の結果を求めるためには、乗算と3という数の知識に頼らなければならない。あらゆる計算は、単に適切な関数と適切な原始的な引数の評価の合成だから、この単純な置き換えの原理は、計算の本質的なメカニズムを捉えるには十分である。さらに、ラムダ計算では''3''や''*''は外部の演算子や定数をまったく使わずに表現されうる。ラムダ計算では、適切に解釈された時3や乗算演算子のように振る舞う項を識別することが可能である。([[ラムダ計算#諸概念のラムダ式での表現|チャーチエンコーディング]]を参照)
<!--
The lambda calculus is known to be computationally equivalent in power to
many other plausible models for computation (including [[チューリングマシン|Turing machine]]s); that is, any calculation that can be accomplished in any
of these other models can be expressed in the lambda calculus, and
vice versa. According to the [[チャーチ・チューリングのテーゼ]], both models
can express any possible computation.
-->
ラムダ計算は、計算としてほかのもっともらしい計算のモデル([[チューリングマシン]]を含む)と同等の力があることが分かっている。つまり、あらゆる計算を行える他のモデルはラムダ計算で表現でき、逆もそうである。[[チャーチ・チューリングのテーゼ]]によれば、両方のモデルはあらゆる可能な計算を表現できる。
<!--
It is perhaps surprising that lambda-calculus can represent any
conceivable computation using only the simple notions of function
abstraction and application based on simple textual substitution of
terms for variables. But even more remarkable is that abstraction is
not even required. ''Combinatory logic'' is a model of computation
equivalent to the lambda calculus, but without abstraction.  The advantage
of this is that evaluating expressions in lambda calculus is quite complicated
because the semantics of substitution must be specified with great care to
avoid variable capture problems.  In contrast, evaluating expressions in
combinatory logic is much simpler, because there is no notion of substitution.
-->
すべての計算が、ラムダ抽象と適用を基本とした変数の置き換えのシンプルな概念で表現できることは、おそらく驚くべきことである。
しかし、さらに目覚ましいのは、ラムダ抽象も必要がないことである。''コンビネータ論理''はラムダ計算と同等のモデルだが、ラムダ抽象は存在しない。ラムダ計算での式の評価は非常に複雑である(置換の意味論は変数を捉えるのを避けるためのかなりの気配りと共に決めなければならない)。対照的に、コンビネータ論理の式の評価は置換という概念が存在しないため、はるかに簡単である。

== コンビネータ計算 ==
<!--
Since abstraction is the only way to manufacture functions in the
lambda calculus, something must replace it in the combinatory
calculus.  Instead of abstraction, combinatory calculus provides a
limited set of primitive functions out of which other functions may be
built.
-->
ラムダ抽象が関数を作るための唯一の方法だから、コンビネータ計算では何かでそれを置き換える必要がある。コンビネータ計算は、ラムダ抽象の代わりに、<!-- out of which other functions may be
built -->原始的な関数の有限集合を提供し、それらから他の関数を構成することができるようにしている。

=== コンビネータ項 ===
<!--A combinatory term has one of the following forms:-->
コンビネータ項は以下の形式のうち一つを持つ:
*''x''
*''P''
*(''E<sub>1</sub>'' ''E<sub>2</sub>'')
<!--
where ''x'' is a variable, ''P'' is one of the primitive functions, and (''E<sub>1</sub>'' ''E<sub>2</sub>'') is the application of combinatory terms ''E<sub>1</sub>'' and ''E<sub>2</sub>''.  The primitive functions themselves are ''combinators'', or functions that, when seen as lambda terms, contain no [[free variable]]s.
To shorten the notations, a general convention is that (''E<sub>1</sub>'' ''E<sub>2</sub>'' ''E<sub>3</sub>'' ... ''E<sub>n</sub>''), or even ''E<sub>1</sub>'' ''E<sub>2</sub>'' ''E<sub>3</sub>''... ''E''<sub>n</sub>, denotes the term (...((''E<sub>1</sub>'' ''E<sub>2</sub>'') ''E<sub>3</sub>'')... ''E<sub>n</sub>''). This is the same general convention as for multiple application in lambda calculus.
-->
''x''は変数、''P''は原始的関数、(''E<sub>1</sub>'' ''E<sub>2</sub>'') は項の適用である。原始的関数はコンビネータ、つまり、ラムダ項として見たときには自由変数を持たない関数である。

表記を短縮するために、伝統的に(''E<sub>1</sub>'' ''E<sub>2</sub>'' ''E<sub>3</sub>'' ... ''E<sub>n</sub>'')ないし''E<sub>1</sub>'' ''E<sub>2</sub>'' ''E<sub>3</sub>'' ... ''E''<sub>n</sub>は(...((''E<sub>1</sub>'' ''E<sub>2</sub>'') ''E<sub>3</sub>'')...''E<sub>n</sub>'')を示す。

=== コンビネータ論理での簡約 ===
<!--
In combinatory logic, each primitive combinator comes with a reduction rule of the form
-->
コンビネータ論理では、それぞれの原始的コンビネータは以下のような形の簡約のルールを持つ。

:(''P'' ''x<sub>1</sub>'' ... ''x<sub>n</sub>'') = ''E''
<!--
where ''E'' is a term mentioning only variables from the set ''x<sub>1</sub>'' ... ''x<sub>n</sub>''. It is in this way that primitive combinators behave as functions.
-->
''E''は変数''x<sub>1</sub>'' ...''x<sub>n</sub>''のみに言及している項である。これらのルールは、原始的コンビネータが関数として振る舞う方法を定義している。

=== コンビネータの例 ===
<!--
The simplest example of a combinator is '''I''', the identity
combinator, defined by
-->
もっとも単純なコンビネータの例は、以下のように定義される恒等コンビネータ'''I'''である。

:('''I''' ''x'') = ''x''
<!--
for all terms ''x''.  Another simple combinator is '''K''', which
manufactures constant functions:  ('''K''' ''x'') is the function which,
for any argument, returns ''x'', so we say
-->
もうひとつの単純なコンビネータは'''K'''で、定数関数を作る。('''K''' ''x'')はどんな引数に対しても''x''を返す関数である。そして、Kはこのように定義する:

:(('''K''' ''x'') ''y'') = ''x''
<!--
for all terms ''x'' and ''y''.  Or, following the convention for
multiple application,
-->
もしくは、伝統的な複数の適用の表記に従えば

:('''K''' ''x'' ''y'') = ''x''
<!--
A third combinator is '''S''', which is a generalized version of
application:
-->
三つ目のコンビネータは、適用を一般化した'''S'''である。

:('''S''' ''x'' ''y'' ''z'') = (''x'' ''z'' (''y'' ''z''))
<!--
'''S''' applies ''x'' to ''y'' after first substituting ''z'' into
each of them. Or put another way, ''x'' is applied to ''y'' inside the
environment ''z''.
-->
Sは、それぞれに''z''を適用したあと''x''を''y''に適用する。別の言い方をすれば、zという環境において''x''を''y''に適用する。
<!--
Given '''S''' and '''K''', '''I''' itself is unnecessary, since it can
be built from the other two:
-->
'''S'''と'''K'''があれば、'''I'''は不必要である。なぜなら、他の二つでこのようにして表現できるからである。

:(('''S''' '''K''' '''K''') ''x'')
::  =  ('''S''' '''K''' '''K''' ''x'')
::  =  ('''K''' ''x'' ('''K''' ''x''))
::  =  ''x''
<!--
for any term ''x''.  Note that although (('''S''' '''K''' '''K''')
''x'') = ('''I''' ''x'') for any ''x'', ('''S''' '''K''' '''K''')
itself is not equal to '''I'''.  We say the terms are [[extensional equality|extensionally equal]].  Extensional equality captures the
mathematical notion of the equality of functions: that two functions
are ''equal'' if they always produce the same results for the same
arguments.  In contrast, the terms themselves, together with the
reduction of primitive combinators, capture the notion of
''intensional equality'' of functions: that two functions are ''equal''
only if they have identical implementations up to the expansion of primitive
combinators when these ones are applied to enough arguments.  There are many ways to
implement an identity function; ('''S''' '''K''' '''K''') and '''I'''
are among these ways.  ('''S''' '''K''' '''S''') is yet another.  We
will use the word ''equivalent'' to indicate extensional equality,
reserving ''equal'' for identical combinatorial terms.
-->
すべての項''x''に対して(('''S''' '''K''' '''K''') ''x'') = ('''I''' ''x'')が成り立つが、('''S''' '''K''' '''K''')自身は'''I'''とは同じではない。これらの項は外延的に同値である。外延的同値は''関数の同値''という数学的な概念である。二つの関数が、同じ引数に対して常に同じ結果を返すならばそれは''等しい''。対照的に、原始的なコンビネータと一緒にあるそれらの項自身は、''内包的同値''という概念を捉える。十分な引数が与えられたときに、原始的なコンビネータに展開されるまで同じ形をもつ時だけ、それらは同値である。

恒等関数を実装するにはたくさんの方法がある。('''S''' '''K''' '''K''')と'''I'''はそれに含まれている。さらに、('''S''' '''K''' '''S''')もそうである。今後、''同値''という言葉を外延的同値を示し、''等しい''を同じコンビネータを示すのに使う。
<!--
A more interesting combinator is the [[fixed point combinator]] or '''Y''' combinator, which can be used to implement [[recursion]].
-->

さらに面白いコンビネータは、[[再帰]]を実装するために使える[[不動点コンビネータ]](Yコンビネータ)である。

=== S-K basisの完全性 ===
<!--
It is a perhaps astonishing fact that '''S''' and '''K''' can be
composed to produce combinators that are extensionally equal to
''any'' lambda term, and therefore, by Church's thesis, to any
computable function whatsoever.  The proof is to present a transformation,
''T''[&nbsp;], which converts an arbitrary lambda term into an equivalent
combinator.
-->
'''S'''と'''K'''が外延的にすべてのラムダ項と同値なものに合成されうるのは、おそらく驚くべき事実である。したがって、チャーチのテーゼによれば、それはあらゆる計算可能な関数に合成されうる。その証明は、''T''[&nbsp;]という任意のラムダ項を同値なコンビネータにする変換を示すことで与えられる。
<!--
''T''[&nbsp;] may be defined as follows:
-->
''T''[&nbsp;]は以下のように定義する。

#       ''T''[''x'']          => ''x''
#       ''T''[(''E₁'' ''E₂'')]    => (''T''[''E₁''] ''T''[''E₂''])
#       ''T''[''λx''.''E'']       => ('''K''' ''T''[''E''])         (if ''x'' does not occur free in ''E'')
#       ''T''[''λx''.''x'']       => '''I'''
#       ''T''[''λx''.''λy''.''E'']    => ''T''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.''E''<nowiki>]]</nowiki> (if ''x'' occurs free in ''E'')
#       ''T''[''λx''.(''E₁'' ''E₂'')] => ('''S''' ''T''[''λx''.''E₁''] ''T''[''λx''.''E₂''])
<!--
This process is also known as ''abstraction elimination''.
-->
これは''abstraction elimination''として知られている。<!--訳は不明-->

==== ラムダ抽象から同値なcombinatorial termへの変換 ====
<!--
For example, we will convert the lambda term ''λx''.''λy''.(''y'' ''x'') to a
combinator:
-->
たとえば、''λx''.''λy''.(''y'' ''x'')をコンビネータにしてみよう。

:''T''[''λx''.''λy''.(''y'' ''x'')]
::        = ''T''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.(''y'' ''x'')<nowiki>]]</nowiki> (by 5)
::        = ''T''[''λx''.('''S''' ''T''[''λy''.''y''] ''T''[''λy''.''x''])] (by 6)
::        = ''T''[''λx''.('''S''' '''I'''       ''T''[''λy''.''x''])] (by 4)
::        = ''T''[''λx''.('''S''' '''I'''       ('''K''' ''x''))] (by 3 and 1)
::        = ('''S''' ''T''[''λx''.('''S''' '''I''')] ''T''[''λx''.('''K''' ''x'')]) (by 6)
::        = ('''S''' ('''K''' ('''S''' '''I'''))   ''T''[''λx''.('''K''' ''x'')]) (by 3)
::        = ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' ''T''[''λx''.'''K'''] ''T''[''λx''.''x''])) (by 6)
::        = ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' ('''K''' '''K''')   ''T''[''λx''.''x''])) (by 3)
::        = ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' ('''K''' '''K''')   '''I''')) (by 4)
<!--
If we apply this combinator to any two terms ''x'' and ''y'', it
reduces as follows:
-->
任意の二つの項''x''と''y''をこのコンビネータに合成すると、以下のように簡約される。

:          ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' ('''K''' '''K''')   '''I''') x y)
::        = ('''K''' ('''S''' '''I''') x  ('''S''' ('''K''' '''K''')   '''I''' x) y)
::        = ('''S''' '''I''' ('''S''' ('''K''' '''K''')   '''I''' x) y)
::        = ('''I''' y ('''S''' ('''K''' '''K''')   '''I''' x y))
::        = (y ('''S''' ('''K''' '''K''')   '''I''' x y))
::        = (y ('''K''' '''K''' x ('''I''' x) y))
::        = (y ('''K''' ('''I''' x) y))
::        = (y ('''I''' x))
::        = (y x)
<!--
The combinatory representation, ('''S''' ('''K''' ('''S''' '''I''')) ('''S''' ('''K''' '''K''') '''I''')) is much
longer than the representation as a lambda term, ''λx''.''λy''.(y x).  This is typical.  In general, the ''T''[&nbsp;] construction may expand a lambda
term of length ''n'' to a combinatorial term of length
[[Big O notation|Θ]](3<sup>''n''</sup>) {{Citation needed|date=May 2010}}.
-->
('''S''' ('''K''' ('''S''' '''I''')) ('''S''' ('''K''' '''K''') '''I'''))という表現は、ラムダ項としての表現''λx''.''λy''.(y x)よりもはるかに長い。これは一般的なことである。普通、''T''[&nbsp;]はラムダ項を[[ランダウの記法|Θ]](''n''<sup>2</sup>)に展開する。

==== ''T''[&nbsp;] 変換について ====
<!--
The ''T''[&nbsp;] transformation is motivated by a desire to eliminate
abstraction.  Two special cases, rules 3 and 4, are trivial: ''λx''.''x'' is
clearly equivalent to '''I''', and ''λx''.''E'' is clearly equivalent to
('''K''' ''T''[''E'']) if ''x'' does not appear free in ''E''.
-->
Tは抽象を消去することが動機となっている。規則3、4は自明である:''λx''.''x''は明らかに'''I'''と等しく、''λx''.''E''はxが自由変数としてEに出現しない時明らかに('''K'''''T''[''E''])である。
<!--
The first two rules are also simple: Variables convert to themselves,
and applications, which are allowed in combinatory terms, are
converted to combinators simply by converting the applicand and the
argument to combinators.
-->
最初の二つの規則も単純である。変数はそれ自身に変換され、コンビネータ項において許されている適用は単にアプリカンドとコンビネータへの引数の変換である。
<!--
It's rules 5 and 6 that are of interest.  Rule 5 simply says that to
convert a complex abstraction to a combinator, we must first convert
its body to a combinator, and then eliminate the abstraction.  Rule 6
actually eliminates the abstraction.
-->
5番目と6番目の規則は興味深い。5番目は複雑な抽象をコンビネータに変換することを単純に示している。まず本体をコンビネータに変換し、それから抽象を除去する。6番目は実際に抽象を除去する。
<!--
''λx''.(''E₁'' ''E₂'') is a function which takes an argument, say ''a'', and
substitutes it into the lambda term (''E₁'' ''E₂'') in place of ''x'',
yielding (''E₁'' ''E₂'')[''x'' : = ''a''].  But substituting ''a'' into (''E₁'' ''E₂'') in place
of ''x'' is just the same as substituting it into both ''E₁'' and ''E₂'', so
-->
''λx''.(''E₁'' ''E₂'')はaという引数を取り、ラムダ項(''E₁'' ''E₂'')のxを置き換えて (''E₁'' ''E₂'')[''x'' : = ''a'']を生成する関数である。
しかし、(''E₁'' ''E₂'')の中の''x''を''a''で置き換えるのはちょうど''E₁'' and ''E₂''を置き換えるのと同じである。だから

        (''E₁'' ''E₂'')[''x'' := ''a''] = (''E₁''[''x'' := ''a''] ''E₂''[''x'' := ''a''])

        (''λx''.(''E₁'' ''E₂'') ''a'') = ((''λx''.''E₁'' ''a'') (''λx''.''E₂'' ''a''))
                       = ('''S''' ''λx''.''E₁'' ''λx''.''E₂'' ''a'')
                       = (('''S''' ''λx''.''E₁'' ''λx''.''E₂'') ''a'')
<!--
By extensional equality,
-->
外延的同値性によって、

        ''λx''.(''E₁'' ''E2'')     = ('''S''' ''λx''.''E₁'' ''λx''.''E₂'')
<!--
Therefore, to  find  a combinator equivalent to ''λx''.(''E₁'' ''E₂''), it is
sufficient to find a combinator equivalent to ('''S''' ''λx''.''E₁'' ''λx''.''E₂''), and
-->
したがって、''λx''.(''E₁'' ''E₂'')と等しいコンビネータを見つけるには、('''S''' ''λx''.''E₁'' ''λx''.''E₂'')と等しいコンビネータを探せば十分である。そして

        ('''S''' ''T''[''λx''.''E₁''] ''T''[''λx''.''E₂''])
<!--
evidently fits the bill.  ''E₁'' and ''E₂'' each contain strictly fewer
applications than (''E₁'' ''E₂''), so the recursion must terminate in a lambda
term with no applications at all&mdash;either a variable, or a term of the
form ''λx''.''E''.
-->
は明らかにその要件に適合する。''E₁''と''E₂''がそれぞれ(''E₁'' ''E₂'')より厳密に少ない適用を含むため、再帰はすべての変数及び''λx''.''E''の形の項において終了させなければならない。<!-- 訳がおかしい -->
=== 簡約の単純化 ===
==== η-簡約 ====
<!--
The combinators generated by the ''T''[&nbsp;] transformation can be made
smaller if we take into account the ''η-reduction'' rule:
-->
''T''[&nbsp;]変換によって生成されたコンビネータは''η-reduction''によって小さくなりうる。

        ''T''[''λx''.(''E'' ''x'')] = ''T''[''E'']   (if ''x'' is not free in ''E'')
<!--
''λx''.(''E'' x) is the function which takes an argument, ''x'', and
applies the function ''E'' to it; this is extensionally equal to the
function ''E'' itself.  It is therefore sufficient to convert ''E'' to
combinatorial form.
-->
''λx''.(''E'' x)はxを引数にとり、''E''を適用する関数である。それは外延的には''E''自身と同値である。それはつまり''E''をコンビネータの形にすれば十分である。
<!--
Taking this simplification into account, the example above becomes:
-->
この例は、この簡略化を根拠付ける。

          ''T''[''λx''.''λy''.(''y'' ''x'')]
        = ...
        = ('''S''' ('''K''' ('''S''' '''I'''))   ''T''[''λx''.('''K''' ''x'')])
        = ('''S''' ('''K''' ('''S''' '''I'''))   '''K''')                 (by η-reduction)
<!--
This combinator is equivalent to the earlier, longer one:
-->
このコンビネータはより早く、長いものと同値である。

          ('''S''' ('''K''' ('''S''' '''I'''))   '''K''' ''x'' ''y'')
        = ('''K''' ('''S''' '''I''') ''x'' ('''K''' ''x'') ''y'')
        = ('''S''' '''I''' ('''K''' ''x'') ''y'')
        = ('''I''' ''y'' ('''K''' ''x'' ''y''))
        = (''y'' ('''K''' ''x'' ''y''))
        = (''y'' ''x'')
<!--
Similarly, the original version of the ''T''[&nbsp;] transformation
transformed the identity function ''λf''.''λx''.(''f'' ''x'') into ('''S''' ('''S''' ('''K''' '''S''') ('''S''' ('''K''' '''K''') '''I''')) ('''K''' '''I''')).  With the η-reduction rule, ''λf''.''λx''.(''f'' ''x'') is
transformed into '''I'''.
-->
同様に、もとの''T''[&nbsp;]は''λf''.''λx''.(''f'' ''x'')を('''S''' ('''S''' ('''K''' '''S''') ('''S''' ('''K''' '''K''') '''I''')) ('''K''' '''I'''))に変換したが、η-簡約を用いれば''λf''.''λx''.(''f'' ''x'')は'''I'''に変換される。

==== One-point basis ====
<!--
There are one-point bases from which every combinator can be composed extensionally equal to ''any'' lambda term. The simplest example of such a basis is {'''X'''} where:
-->
すべてのコンビネータがすべてのラムダ項と外延的に等しくなるようなone-point basesが存在する。そのような基底のもっとも単純な例'''X'''はこうである。

        '''X''' ≡ ''λx''.((x'''S''')'''K''')
<!--
It is not difficult to verify that:
-->
それを確かめるのは難しくない。
        '''X''' ('''X''' ('''X''' '''X''')) =<sup>ηβ</sup> '''K''' and
        '''X''' ('''X''' ('''X''' ('''X''' '''X'''))) =<sup>ηβ</sup> '''S'''.
<!--
Since {'''K''', '''S'''} is a basis, it follows that {'''X'''} is a basis too. The [[Iota and Jot|Iota]] programming language uses '''X''' as its sole combinator.
-->
{'''K''', '''S'''}が基底だから、{'''X'''}もまた基底である。プログラミング言語[[Lazy K|Iota]]は'''X'''をその唯一のコンビネータとして使う。
<!--
Another simple example of a one-point basis is:
-->
one-point basisのもう一つの簡単な例は

        '''X'''' ≡ ''λx''.(x '''K''' '''S''' '''K''') with
        ('''X'''' '''X'''') '''X'''' =<sup>β</sup> '''K''' and
        '''X'''' ('''X'''' '''X'''') =<sup>β</sup> '''S'''
<!--
'''X' ''' does not need η contraction in order to produce '''K''' and '''S'''.
-->
'''X' '''は'''K'''と'''S'''を生成するのにη変換を必要としない。

==== B,Cコンビネータ ====
<!--
In addition to '''S''' and '''K''', [[Moses Schönfinkel|Schönfinkel]]'s paper included two combinators which are now called '''B''' and '''C''', with the following reductions:
-->
SとKに加え、{{仮リンク|モイセイ・シェインフィンケリ|ru|Шейнфинкель, Моисей Эльевич|en|Moses Schönfinkel}}の論文では'''B'''と'''C'''と呼ばれる、以下のような簡約をするコンビネータを含めた。

        ('''C''' ''f'' ''x'' ''y'') = (''f'' ''y'' ''x'')
        ('''B''' ''f'' ''g'' ''x'') = (''f'' (''g'' ''x''))
<!--
He also explains how they in turn can be expressed using only '''S''' and '''K'''.
-->
彼は、どのようにしてSとKだけを用いてこれらを表現できるかを説明した。
<!--
These combinators are extremely useful when translating predicate logic or lambda calculus into combinator expressions. They were also used by [[Haskell Curry|Curry]], and much later by [[David Turner (computer scientist)|David Turner]], whose name has been associated with their computational use. Using them, we can extend the rules for the transformation as follows:
-->
これらのコンビネータは述語論理やラムダ計算をコンビネータ式にする際に非常に有用である。これらは[[ハスケル・カリー]]と、だいぶ後に計算機における用法と関連付けた[[デビッド・ターナー]]によって使われた。これらを使って、以下のように変換のルールを拡張できる。

#       ''T''[''x'']          => ''x''
#       ''T''[(''E₁'' ''E₂'')]    => (''T''[''E₁''] ''T''[''E₂''])
#       ''T''[''λx''.''E'']       => ('''K''' ''T''[''E''])         (if ''x'' is not free in ''E'')
#       ''T''[''λx''.''x'']       => '''I'''
#       ''T''[''λx''.''λy''.''E'']    => ''T''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.''E''<nowiki>]]</nowiki> (if ''x'' is free in ''E'')
#       ''T''[''λx''.(''E₁'' ''E₂'')] => ('''S''' ''T''[''λx''.''E₁''] ''T''[''λx''.''E₂'']) (if ''x'' is free in both ''E₁'' and ''E₂'')
#       ''T''[''λx''.(''E₁'' ''E₂'')] => ('''C''' ''T''[''λx''.''E₁''] ''T''[''E₂'']) (if ''x'' is free in ''E₁'' but not ''E₂'')
#       ''T''[''λx''.(''E₁'' ''E₂'')] => ('''B''' ''T''[''E₁''] ''T''[''λx''.''E₂'']) (if ''x'' is free in ''E₂'' but not ''E₁'')
<!--
Using '''B''' and '''C''' combinators, the transformation of
''λx''.''λy''.(''y'' ''x'') looks like this:
-->
'''B'''と'''C'''コンビネータを使うと、''λx''.''λy''.(''y'' ''x'')の変換はこのようになる。

          ''T''[''λx''.''λy''.(''y'' ''x'')]
        = ''T''<nowiki>[</nowiki>''λx''.''T''<nowiki>[</nowiki>''λy''.(''y'' ''x'')<nowiki>]</nowiki><nowiki>]</nowiki>
        = ''T''[''λx''.('''C''' ''T''[''λy''.''y''] ''x'')]     (by rule 7)
        = ''T''[''λx''.('''C''' '''I''' ''x'')]
        = ('''C''' '''I''')                   (η-reduction)
        = '''C'''<sub>*</sub>(traditional canonical notation : '''X'''<sub>*</sub> = '''X''' '''I''')
        = '''I''''(traditional canonical notation: '''X'''' = '''C''' '''X''')
<!--
And indeed, ('''C''' '''I''' ''x'' ''y'') does reduce to (''y'' ''x''):
-->
確かに、('''C''' '''I''' ''x'' ''y'')は(''y'' ''x'')に簡約される。

          ('''C''' '''I''' ''x'' ''y'')
        = ('''I''' ''y'' ''x'')
        = (''y'' ''x'')
<!--
The motivation here is that '''B''' and '''C''' are limited versions of '''S'''.
Whereas '''S''' takes a value and substitutes it into both the applicand and
its argument before performing the application, '''C''' performs the
substitution only in the applicand, and '''B''' only in the argument.
-->
その動機は、'''B'''と'''C'''は限定された'''S'''であるということである。
'''S'''は値を取り両方のアプリカンドを置き換えて適用を行う一方。'''C'''はアプリカンドのみ、'''B'''は引数のみを置き換える。
<!--
The modern names for the combinators come from [[Haskell Curry]]'s doctoral thesis of 1930 (see [[B,C,K,W System]]). In [[Moses Schönfinkel|Schönfinkel]]'s original paper, what we now call  '''S''', '''K''', '''I''', '''B''' and '''C''' were called '''S''', '''C''', '''I''', '''Z''', and '''T''' respectively.
-->
そのコンビネータのための近代的な名前は、[[ハスケル・カリー]]の1930年の博士論文による([[B,C,K,Wシステム]]を参照)。{{仮リンク|モイセイ・シェインフィンケリ|ru|Шейнфинкель, Моисей Эльевич|en|Moses Schönfinkel}}のもとの論文では、今'''S''', '''K''', '''I''', '''B''','''C'''と呼んでいるものはそれぞれ'''S''', '''C''', '''I''', '''Z''', '''T'''と呼ばれていた。
<!--
The reduction in combinator size that results from the new transformation rules
can also be achieved without introducing '''B''' and '''C''', as demonstrated in Section 3.2 of
-->
新しい変換の規則によるコンビネータのサイズの短縮は'''B'''と'''C'''を用いなくても、この論文<ref>John Tromp, Binary Lambda Calculus and Combinatory Logic, in ''Randomness And Complexity, from Leibniz To Chaitin'', ed. Cristian S. Calude, World Scientific Publishing Company, October 2008. [http://www.cwi.nl/~tromp/cl/LC.pdf (pdf version)]</ref>の節3.2のように達成できる。

===== CL<sub>K</sub>とCL<sub>I</sub>算法 =====
<!--
A distinction must be made between the '''CL'''<sub>K</sub> as described in this article and the '''CL'''<sub>I</sub> calculus. The distinction corresponds to that between the λ<sub>K</sub> and the λ<sub>I</sub> calculus. Unlike the λ<sub>K</sub> calculus, the λ<sub>I</sub> calculus restricts abstractions to:
-->
この記事で述べている'''CL'''<sub>K</sub>算法と'''CL'''<sub>I</sub>算法は区別されなければならない。これらの区別は、λ<sub>K</sub>とλ<sub>I</sub>算法に対応する。λ<sub>K</sub>算法と違い、λ<sub>I</sub>算法は抽象を以下のように制限する。

::''λx''.''E'' where ''x'' has at least one free occurrence in ''E''.

::''λx''.''E''において、''x''は''E''の中で少なくとも一つは自由に出現している。
<!--
As a consequence, combinator '''K''' is not present in the λ<sub>I</sub> calculus nor in the '''CL'''<sub>I</sub> calculus. The constants of '''CL'''<sub>I</sub> are: '''I''', '''B''', '''C''' and '''S''', which form a basis from which all '''CL'''<sub>I</sub> terms can be composed (modulo equality). Every λ<sub>I</sub> term can be converted into an equal '''CL'''<sub>I</sub> combinator according to rules similar to those presented above for the conversion of λ<sub>K</sub> terms into '''CL'''<sub>K</sub> combinators. See chapter 9 in Barendregt (1984).
-->
結果として、'''K'''はλ<sub>I</sub>にも'''CL'''<sub>I</sub>にも与えられない。'''CL'''<sub>I</sub>の定数は、'''I''', '''B''', '''C''','''S'''であり、'''CL'''<sub>I</sub>のすべての項が合成される。λ<sub>K</sub>から'''CL'''<sub>K</sub>への変換と似たようなルールに合わせ、すべてのλ<sub>I</sub>の項は、等しい'''CL'''<sub>I</sub>に変換される。Barendregt (1984)の第9章を参照されたい。

=== 逆変換 ===
<!--
The conversion ''L''[&nbsp;] from combinatorial terms to lambda terms is
trivial:
-->
コンビネータの項からラムダ項への変換''L''[&nbsp;]は自明である。

        ''L''['''I''']       = ''λx''.''x''
        ''L''['''K''']       = ''λx''.''λy''.''x''
        ''L''['''C''']       = ''λx''.''λy''.''λz''.(''x'' ''z'' ''y'')
        ''L''['''B''']       = ''λx''.''λy''.''λz''.(''x'' (''y'' ''z''))
        ''L''['''S''']       = ''λx''.''λy''.''λz''.(''x'' ''z'' (''y'' ''z''))
        ''L''[(''E₁'' ''E₂'')] = (''L''[''E₁''] ''L''[''E₂''])
<!--
Note, however, that this transformation is not the inverse
transformation of any of the versions of ''T''[&nbsp;] that we have seen.
-->
これは、前述の''T''[&nbsp;]の逆変換ではないことに注意。

== コンビネータ計算の非決定性 ==
<!--
A [[normal form (abstract rewriting)|正規形]] is any combinatory term in which the primitive combinators that occur, if any, are not applied to enough arguments to be simplified. It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc.  This is equivalent to the undecidability of the corresponding problems for lambda terms.  However, a direct proof is as follows:
-->
一般的なコンビネータ項が正規形を持つかどうか、二つのコンビネータ項が同じかどうかは判定できない。これは、対応するラムダ項における非決定性と同じである。直接的な証明は以下のようになる。
まず、以下の項を見てみよう。
<!--
First, observe that the term
-->
        '''Ω''' = ('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
<!--
has no normal form, because it reduces to itself after three steps, as
follows:
-->
この項は正規形を持たない。なぜなら、以下に示すようにこれは自分自身に簡約するからである。

          ('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
        = ('''I''' ('''S''' '''I''' '''I''') ('''I''' ('''S''' '''I''' '''I''')))
        = ('''S''' '''I''' '''I''' ('''I''' ('''S''' '''I''' '''I''')))
        = ('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
<!--
and clearly no other reduction order can make the expression shorter.
-->
そして、明らかにこれ以上短い式を作る簡約はない。
<!--
Now, suppose '''N''' were a combinator for detecting normal forms,
such that
-->
正規形を検出するコンビネータ'''N'''を考えてみよう。

        ('''N''' ''x'') => '''T''', if ''x'' has a normal form
                 '''F''', otherwise.
<!--
(Where '''T''' and '''F''' represent the conventional [[ラムダ計算#諸概念のラムダ式での表現|チャーチエンコーディング]]s of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic. The combinatory versions have '''T''' = '''K''' and '''F''' = ('''K''' '''I''').)
-->
('''T'''と'''F'''は[[ラムダ計算#諸概念のラムダ式での表現|チャーチエンコーディング]]における真理値を表現する。''λx''.''λy''.''x''と''λx''.''λy''.''y''で、コンビネータの形では'''T''' = '''K''' and '''F''' = ('''K''' '''I''')である。)
<!--
Now let
-->
そして、

        ''Z'' = ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''')
<!--
now consider the term  ('''S''' '''I''' '''I''' ''Z'').  Does ('''S''' '''I''' '''I''' ''Z'') have a normal
form?  It does if and only if the following do also:
-->
('''S''' '''I''' '''I''' ''Z'')という項を考えてみよう。('''S''' '''I''' '''I''' ''Z'')は正規形を持つだろうか？それはもしこのようにしたとき、こうなる。

          ('''S''' '''I''' '''I''' ''Z'')
        = ('''I''' ''Z'' ('''I''' ''Z''))
        = (''Z'' ('''I''' ''Z''))
        = (''Z'' ''Z'')
        = ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''' ''Z'')           (definition of ''Z'')
        = ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''' ''Z'' '''I''')
        = ('''B''' '''N''' ('''S''' '''I''' '''I''') ''Z'' '''Ω''' '''I''')
        = ('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
<!--
Now we need to apply '''N''' to ('''S''' '''I''' '''I''' ''Z'').
Either ('''S''' '''I''' '''I''' ''Z'') has a normal form, or it does not.  If it ''does''
have a normal form, then the foregoing reduces as follows:
-->
今、'''N'''を('''S''' '''I''' '''I''' ''Z'')に適用する必要がある。
('''S''' '''I''' '''I''' ''Z'')が正規形を持つか、そうでないか。もしそれが正規形を''持つ''ならば、以下のように簡約される。

          ('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
        = ('''K''' '''Ω''' '''I''')                               (definition of '''N''')
        = '''Ω'''
<!--
but '''Ω''' does ''not'' have a normal form, so we have a contradiction.  But
if ('''S''' '''I''' '''I''' ''Z'') does ''not'' have a normal form, the foregoing reduces as
follows:
-->
しかし、'''Ω'''は正規形を持たないため、矛盾している。もし、('''S''' '''I''' '''I''' ''Z'')が正規形を''持たない''ならば、このように簡約する。

          ('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
        = ('''K''' '''I''' '''Ω''' '''I''')                             (definition of '''N''')
        = ('''I''' '''I''')
          '''I'''
<!--
which means that the normal form of ('''S''' '''I''' '''I''' ''Z'') is simply '''I''', another
contradiction.  Therefore, the hypothetical normal-form combinator '''N'''
cannot exist.
-->
('''S''' '''I''' '''I''' ''Z'')の正規形は単に'''I'''であり、また矛盾を生む。したがって、仮定した正規形コンビネータ'''N'''は存在できない。
<!--
The combinatory logic analogue of [[ライスの定理]] says that there is no complete nontrivial predicate.  A ''predicate'' is a combinator that, when applied,  returns either '''T'''or '''F'''.   A predicate ''N'' is ''nontrivial'' if there are two arguments ''A'' and ''B'' such that ''NA''='''T''' and ''NB''='''F'''. A combinator ''N'' is''complete'' if and only if ''NM'' has a normal form for every argument ''M''.  The analogue of Rice's theorem then says that every complete predicate is trivial. The proof of this theorem is rather simple.

'''Proof:''' By reductio ad absurdum. Suppose there is a complete non trivial predicate, say ''N''.<br />
Because ''N'' is supposed to be non trivial there are combinators ''A'' and ''B'' such that<br />
(''N A'') = '''T''' and<br />
(''N B'') = '''F'''.

Define NEGATION ≡ ''λx.''(if (''N x'') then ''B'' else ''A'') ≡ ''λx.''((''N x'') ''B'' ''A'')<br />
Define ABSURDUM ≡ ('''Y''' NEGATION)

Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM), for<br />
ABSURDUM ≡ ('''Y''' NEGATION) = (NEGATION ('''Y''' NEGATION)) ≡ (NEGATION ABSURDUM).

Because ''N'' is supposed to be complete either:
# (''N'' ABSURDUM) = '''F''' or
# (''N'' ABSURDUM) = '''T'''

Case 1: '''F''' = (''N'' ABSURDUM) = ''N'' (NEGATION ABSURDUM) = (''N A'') = '''T''', a contradiction.<br />
Case 2: '''T''' = (''N'' ABSURDUM) = ''N'' (NEGATION ABSURDUM) = (''N B'') = '''F''', again a contradiction.

Hence (''N'' ABSURDUM) is neither '''T''' nor '''F''', which contradicts the presupposition that ''N'' would be a complete non trivial predicate. '''QED'''.

From this undecidability theorem it immediately follows that there is no complete predicate that can discriminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is '''no''' complete predicate, say EQUAL, such that:<br />
(EQUAL ''A B'') = '''T''' if ''A'' = ''B'' and<br />
(EQUAL ''A B'') = '''F''' if ''A'' ≠ ''B''.<br />
If EQUAL would exist, then for all ''A'', ''λx.''(EQUAL ''x A'') would have to be a complete non trivial predicate.
-->

[[ライスの定理]]におけるコンビネータ論理の例(原文：The combinatory logic analogue)が言うのは、完全で非自明な述語は存在しないという事である。ある述語がコンビネータであるということは、適用の際にTrueかFalseのどちらかを返すということである。もし2つの''NA''='''T'''と''NB''='''F'''を満たすような2つの引数''A'',''B''が存在するとき、その述語''N''は非自明であるという。また、''NM''がいかなる引数''M''についても正規形をしているとき、そしてその時に限り述語''N''が完全であるという。ライスの定理の例は、全ての完全な述語は自明であると述べている。この定理の証明はかなり単純である。

'''証明''':背理法による。完全で非自明な述語の存在を仮定し、'''N''' と呼ぶことにする。

Nは非自明であるから以下を満たすコンビネータA,Bが存在する。

(''N A'') = '''T'''<br />
(''N B'') = '''F'''

Define NEGATION ≡ ''λx.''(if (''N x'') then ''B'' else ''A'') ≡ ''λx.''((''N x'') ''B'' ''A'')<br />
Define ABSURDUM ≡ ('''Y''' NEGATION) 

不動点定理により、
ABSURDUM ≡ ('''Y''' NEGATION) = (NEGATION ('''Y''' NEGATION)) ≡ (NEGATION ABSURDUM)
を満たすABSURDUM = (NEGATION ABSURDUM)が与えられる。

Nは完全であるから以下の2つのうちどちらかを満たす。
# (''N'' ABSURDUM) = '''F'''
# (''N'' ABSURDUM) = '''T'''

場合1: F = '''F''' = (''N'' ABSURDUM) = ''N'' (NEGATION ABSURDUM) = (''N A'') = '''T''' これは矛盾である。

場合2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F これもまた矛盾である。

故に、 (''N'' ABSURDUM) は真であっても偽であってもNが完全で非自明な述語であることに反する。QED。

この論証不明の定理からすぐに、正規形をもつ条件を満たすかどうかを決定することができる完全な述語は存在しないことが導かれる。さらに、

(EQUAL ''A B'') = '''T''' if ''A'' = ''B'' and<br />
(EQUAL ''A B'') = '''F''' if ''A'' ≠ ''B''.<br />

でのEQUALのような完全な述語は存在しないことも言える。
もしもEQUALが存在したならば、全てのAについて λx.(EQUAL x A) は完全で非自明な述語でなければならない。

この結果はコンビネータ論理の決定不能性を'''意味しない'''ことに注意しなければならない。これらの結果のいうところは、コンビネータそれ自身を引数に取り（ある条件を満たす）性質を判定するコンビネータが存在しないということであり、計算論的な意味の不能性を意味するわけではない。実際、コンビネータの'''構文的な'''等価性は上の定理によればコンビネータにより判定することはできない（コンビネータ論理の定義には異なる変数記号を体系内で区別するような規則は何一つとして含まれてはいない）が、明らかに計算可能である。コンビネータ論理の決定不能性を示すには、コンビネータを[[ゲーデル数]]を用いて自然数にコーディングの上で、ゲーデル数を表すコンビネータを引数に取り（ある条件を満たす）性質を判定するコンビネータが存在しないということを証明すればよい。一般に、非自明かつweak同値性に関して閉じたn-項関係は決定不能である。それゆえ、上述したような述語は、ゲーデル数を用いてもなお表現できない。その証明は最初に述べた証明を多少変更するだけで得られる。一方で、あるゲーデル数に対してコンビネータの構文的な等価性を判定するコンビネータを構成することもできる。

== 応用 ==
=== 関数型言語のコンパイル ===
<!--
[[関数型言語]]s are often based on the simple but
universal semantics of the [[ラムダ計算]].
along
David Turner used his combinators to implement the [[SASL (プログラミング言語)|SASL]].

[[Kenneth E. Iverson]] used primitives based on Curry's combinators in his [[J (プログラミング言語)]], a successor to [[APL]]. This enabled what Iverson called [[tacit programming]], that is, programming in functional expressions containing no variables, along with powerful tools for working with such programs. It turns out that tacit programming is possible in a clumsier manner in any APL-like language with user-defined operators 
([http://portal.acm.org/citation.cfm?id=114065&dl=GUIDE&coll=GUIDE Pure Functions in APL and J]).-->
<!--
(Discuss strict vs. [[lazy evaluation]] semantics.  Note implications of
graph reduction implementation for lazy evaluation.  Point out
efficiency problem in lazy semantics: Repeated evaluation of the same
expression, in, e.g. (square COMPLICATED) => (* COMPLICATED
COMPLICATED), normally avoided by eager evaluation and call-by-value.
Discuss benefit of graph reduction in this case: when (square
COMPLICATED) is evaluated, the representation of COMPLICATED can be
shared by both branches of the resulting graph for (* COMPLICATED
COMPLICATED), and evaluated only once.)
-->
<!-- Work in [[combinator library]] somehow. -->

関数型言語は、ラムダ計算がシンプルながら万能性があるため、ラムダ計算をベースとしているものが多いが、ラムダ式はコンビネータ式に変換可能であり、一種のコンパイルとも言える。David Turnerは、SASLの実装にコンビネータを利用した（SASLに限らず、一般に関数型言語の実装に応用可能である）。

[[Kenneth E. Iverson]]は、[[APL]]の後続に位置づけられる[[J (プログラミング言語)]]で、カリーのコンビネータを基本としたプリミティブを採用し、Iversonがtacit programming（[[:en:Tacit programming]]）と呼んだものを可能にした。それは、変数を含まない式で、そのようなプログラムで作業するための強力なツールに沿って行うプログラミングである。APLのような言語では、ユーザー定義の演算子を用いたclumsier mannerで暗黙のプログラミングが可能であることが判明した。([http://portal.acm.org/citation.cfm?id=114065&dl=GUIDE&coll=GUIDE Pure Functions in APL and J])

=== 論理学 ===
[[カリー＝ハワード同型対応]]によれば、論理式と型が対応し、[[直観主義論理]]の含意断片のヒルベルト流の推論図と型付きコンビネータ項が対応する。
<!--
The '''K''' and '''S''' combinators correspond to the axioms
-->
コンビネータ'''K'''、'''S'''は以下の[[公理図式]]に対応する。
:'''AK''': ''A'' → (''B'' → ''A''),
:'''AS''': (''A'' → (''B'' → ''C'')) → ((''A'' → ''B'') → (''A'' → ''C'')),
<!-- and function application corresponds to the detachment (modus ponens) rule -->
そして、関数適用は[[モーダスポネンス]]に対応する。
:'''MP''': ''A'' と ''A'' → ''B'' から ''B'' を推論できる。

コンビネータ項に直和や直積の為の定数を加え、さらに基本型としてbottom <math>\bot</math>、複合型として直積型と直和型を加えたものは、ヒルベルト流の直観主義命題論理と対応する。

== 関連項目 ==
*[[SKIコンビネータ計算]]
*[[B,C,K,Wシステム]]
* [[ラムダ計算]] 
* [[不動点コンビネータ]]
*{{仮リンク|graph reduction machine|en|graph reduction machine}}
*{{仮リンク|supercombinator|en|supercombinator}}
*{{仮リンク|Cylindric algebra|en|Cylindric algebra}} and other approaches to modelling quantification and eliminating variables
*「{{仮リンク|数学パズル ものまね鳥をまねる|en|To Mock a Mockingbird}}」
*{{仮リンク|combinatory categorial grammar|en|combinatory categorial grammar}}
*{{仮リンク|Categorical abstract machine|en|Categorical abstract machine}}
*{{仮リンク|Applicative computing systems|en|Applicative computing systems}}

== 脚注 ==
{{reflist}}

== 参考文献 ==
*[[Hendrik Pieter Barendregt]], 1984. ''The Lambda Calculus, Its Syntax and Semantics''. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland.ISBN 0-444-87508-5
*{{cite book
| last1 = Curry | first1 = Haskell B.
| authorlink1 = Haskell Curry
| last2 = Feys | first2 = Robert
| authorlink2 = Robert Feys
| title = Combinatory Logic
| volume = Vol. I
| year = 1958
| publisher = North Holland
| location = Amsterdam
| isbn = 0-7204-2208-6
}}
*{{cite book
| last1 = Curry | first1 = Haskell B.
| first2 = J. Roger | last2 = Hindley
| first3 = Jonathan P. | last3 = Seldin
| authorlink1 = Haskell Curry
| authorlink2 = J. Roger Hindley
| authorlink3 = Jonathan P. Seldin
| title = Combinatory Logic
| volume = Vol. II
| year = 1972
| publisher = North Holland
| location = Amsterdam
| isbn = 0-7204-2208-6
}}
* Field, Anthony J. and Peter G. Harrison, 1998. ''Functional Programming''. . Addison-Wesley. ISBN 0-201-19249-7
*{{cite
 | last1 = Hindley | first1 = J. Roger
 | last2 = Meredith | first2 = David
 | authorlink1 = J. Roger Hindley
 | authorlink2 = David Meredith
 | title = Principal type-schemes and condensed detachment
 | url = http://projecteuclid.org/euclid.jsl/1183743187
 | id = {{MR|1043546}}
 | journal = [[Journal of Symbolic Logic]]
 | volume = 55
 | issue = 1
 | pages = 90–105
 | year = 1990
}}
* Hindley, J. R., and Seldin, J. P. (2008) ''[http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521898850 λ-calculus and Combinators: An Introduction]''. Cambridge Univ. Press.
* Paulson, Lawrence C., 1995. ''[http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz Foundations of Functional Programming.]'' University of Cambridge.
*<span id="Quine 1960">[[Willard Van Orman Quine|Quine, W. V.]], 1960 "Variables explained away", ''Proceedings of the American Philosophical Society'' '''104''':3:343–347 (June 15, 1960) [http://links.jstor.org/sici?sici=0003-049X%2819600615%29104%3A3%3C343%3AVEA%3E2.0.CO%3B2-W at JSTOR]. Reprinted as Chapter 23 of Quine's ''Selected Logic Papers''(1966), pp. 227–235</span>
* [[:en:Moses Schönfinkel|Moses Schönfinkel]], 1924, "Über die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in ''From Frege to Gödel: a source book in mathematical logic, 1879–1931'', [[Jean van Heijenoort]], ed. Harvard University Press, 1967. ISBN 0-674-32449-8. The article that founded combinatory logic.
*Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. ''[http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf Lectures on the Curry&ndash;Howard Isomorphism.]'' University of Copenhagen and University of Warsaw, 1999.
* [[:en:Raymond Smullyan|Smullyan, Raymond]], 1985. ''[[To Mock a Mockingbird]]''. Knopf. ISBN 0-394-53491-3. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
** [[レイモンド・スマリヤン|スマリヤン]]『ものまね鳥をまねる』（POD版 http://www.morikita.co.jp/books/book/142 、 http://www.morikita.co.jp/books/book/141 ）
*--------, 1994. ''Diagonalization and Self-Reference''. Oxford Univ. Press. Chpts. 17-20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
* Wolfengagen, V.E. ''[http://vew.0catch.com/books/Wolfengagen_CLP-2003-En.djvu Combinatory logic in programming.] Computations with objects through examples and exercises''. -- 2-nd ed. -- M.: "Center JurInfoR" Ltd., 2003. -- x+337 с. ISBN 5-89158-101-9.

== 外部リンク ==
*[[Stanford Encyclopedia of Philosophy]]: "[http://plato.stanford.edu/entries/logic-combinatory/ Combinatory Logic]" by Katalin Bimbó.
*[http://www.sadl.uleth.ca/gsdl/cgi-bin/library?a=p&p=about&c=curry 1920–1931 Curry's block notes.]
*Keenan, David C. (2001) "[http://dkeenan.com/Lambda/index.htm To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction.]"
*Rathman, Chris, "[http://www.angelfire.com/tx4/cus/combinator/birds.html Combinator Birds.]" A table distilling much of the essence of Smullyan (1985).
*[http://cstein.kings.cam.ac.uk/~chris/combinators.html Drag 'n' Drop Combinators.] (Java Applet)
*[http://www.cwi.nl/~tromp/cl/LC.pdf Binary Lambda Calculus and Combinatory Logic.]
*[https://code.google.com/archive/p/clache Combinatory logic reduction web server]

{{Normdaten}}
{{DEFAULTSORT:こんひねえたろんり}}
[[Category:ラムダ計算]]
[[Category:理論計算機科学]]
[[Category:コンビネータ論理|*]]