組み合わせ論理

組み合わせ論理は、数理論理学における量化変数の必要性を排除するための記法です。これは、モーゼス・シェーンフィンケル^[¹^]とハスケル・カリー[ ²^]^によって導入され、近年ではコンピュータ科学において計算の理論モデルとして、また関数型プログラミング言語の設計の基礎として使用されています。これは、シェーンフィンケルが1920年に導入したコンビネータに基づいています。コンビネータは、特に述語論理において、関数を構築するための類似の方法を提供し、変数の言及を排除するという考えに基づいています。コンビネータは、関数適用と先に定義されたコンビネータのみを使用して引数から結果を定義する高階関数です。

数学において

組み合わせ論理はもともと、量化変数の役割を明確にするための「前論理」として意図されており、本質的には量化変数を排除することによってそれを実現しようとした。量化変数を排除するもう1つの方法は、クワインの述語関数論理である。組み合わせ論理の表現力は通常、一階述語論理の表現力を上回るが、述語関数論理の表現力は一階述語論理の表現力と同一である（クワイン 1960、1966、1976）。

組み合わせ論理の発明者であるモーゼス・シェーンフィンケルは、1924年の最初の論文以降、組み合わせ論理について何も発表していません。ハスケル・カリーは、 1927年後半にプリンストン大学で講師として働いていたときにコンビネータを再発見しました。^{[ 3 ]} 1930年代後半、アロンゾ・チャーチとプリンストンの彼の学生は、関数抽象化のライバル形式であるラムダ計算を発明し、これは組み合わせ論理よりも人気を博しました。これらの歴史的偶然の結果、1960年代と1970年代に理論計算機科学が組み合わせ論理に興味を持ち始めるまで、この主題に関するほぼすべての研究はハスケル・カリーとその学生、またはベルギーのロバート・フェイズによるものでした。カリーとフェイズ（1958）とカリーら（1972）は、組み合わせ論理の初期の歴史を概観しています。組み合わせ論理とラムダ計算のより現代的な扱いについては、1960年代と1970年代にダナ・スコットが考案した組み合わせ論理のモデルを概説したバレンデレグトの著書[ ⁴^]^{を参照してください。}

コンピューティングにおいて

コンピュータ科学において、組み合わせ論理は計算の簡略化されたモデルとして用いられ、計算可能性理論や証明論で活用されている。その単純さにもかかわらず、組み合わせ論理は計算の多くの本質的な特徴を捉えている。

組み合わせ論理は、ラムダ計算の変形と見なすことができ、ラムダ式（関数抽象化を表す）を、自由変数を持たないプリミティブ関数であるコンビネータの限られたセットに置き換えたものです。ラムダ式をコンビネータ式に変換するのは容易であり、コンビネータの簡約はラムダの簡約よりもはるかに簡単です。そのため、組み合わせ論理は、一部の非厳密関数型プログラミング言語やハードウェアのモデリングに用いられてきました。この考え方の最も純粋な形は、プログラミング言語Unlambdaです。Unlambdaの唯一のプリミティブは、文字入出力機能を追加したSコンビネータとKコンビネータです。Unlambdaは実用的なプログラミング言語ではありませんが、理論的には興味深いものです。

組み合わせ論理にはさまざまな解釈が可能である。カリーによる初期の論文の多くは、従来の論理の公理セットを組み合わせ論理の方程式に変換する方法を示した。^{[ 5 ]}ダナ・スコットは1960年代と1970年代に、モデル理論と組み合わせ論理を融合する方法を示した。

ラムダ計算の概要

ラムダ計算はラムダ項と呼ばれるオブジェクトに関係しており、ラムダ項は次の3つの形式の文字列で表現できます。

$v$
$\lambda v.E_{1}$
$(E_{1}E_{2})$

どこ $v$ は、定義済みの無限の変数名セットから抽出された変数名であり、 $E_{1}$ そして $E_{2}$ ラムダ項です。

フォームの利用規約 $\lambda v.E_{1}$ これらは抽象化と呼ばれます。変数 $v$ これは抽象化の形式パラメータと呼ばれ、 $E_{1}$ 抽象化の本体です。 $\lambda v.E_{1}$ は、引数に適用すると仮パラメータを束縛する関数を表します。 $v$ 引数に対して、結果の値を計算します。 $E_{1}$ つまり、それは返される $E_{1}$ 毎回 $v$ 引数に置き換えられました。

フォームの利用規約 $E_{1}E_{2}$ これらはアプリケーションと呼ばれます。アプリケーションは関数呼び出しまたは実行をモデル化します。 $E_{1}$ 呼び出す必要があります。 $E_{2}$ 引数として、結果が計算されます。 $E_{1}$ （時には適用対象とも呼ばれる）は抽象概念であり、この用語は次のように簡略化できる。 $E_{2}$ 議論は、本文に置き換えることができる。 $E_{1}$ 形式パラメータの代わりに $E_{1}$ 、その結果は、古いラムダ項と同等の新しいラムダ項になります。ラムダ項に次の形式のサブ項が含まれていない場合 $((\lambda v.E_{1})E_{2})$ そうなると、それは還元できず、正規形であると言われる。

その表現 $E[v:=a]$ 項を取る結果を表す $E$ そして、すべての自由な出現箇所を置き換える $v$ その中に $a$ ということで、次のように書きます。

((\lambda vE)a)\Rightarrow E[v:=a]

慣例として、 $(abc)$ 略語として $((ab)c)$ （つまり、適用は左結合である）。

この還元の定義の動機は、それがすべての数学関数の本質的な振る舞いを捉えている点にある。例えば、ある数の二乗を計算する関数を考えてみよう。次のように書くことができる。

の二乗

x

は

x*x

（「 $*$ （乗算を表す。） $x$ ここに、関数の仮引数を示します。特定の引数（例えば3）に対して二乗を計算するには、定義の中で仮引数の代わりに3を挿入します。

の二乗

3

は

3*3

結果として得られる式を評価する $3*3$ 乗算と数 3 の知識に頼らざるを得ません。あらゆる計算は適切な関数を適切な原始引数に対して評価することの合成にすぎないため、この単純な置換原理で計算の本質的なメカニズムを捉えるのに十分です。さらに、ラムダ計算では、「3」や「 $*$ は、外部で定義された基本演算子や定数を必要とせずに表現できます。ラムダ計算では、適切に解釈すると数値 3 や乗算演算子のように振る舞う項を識別することが可能です( Church エンコーディングを参照) 。

ラムダ計算は、チューリングマシンを含む他の多くの妥当な計算モデルと計算能力において同等であることが知られています。つまり、これらの他のモデルで実行可能な計算はすべてラムダ計算で表現でき、その逆もまた同様です。チャーチ＝チューリングのテーゼによれば、どちらのモデルもあらゆる可能な計算を表現できます。

ラムダ計算が、単純な変数への項のテキスト置換に基づく関数抽象化と適用という単純な概念のみを使用して、考えられるあらゆる計算を表現できるというのは、おそらく驚くべきことだろう。しかし、さらに注目すべきは、抽象化さえ必要としないということだ。組み合わせ論理は、ラムダ計算と同等の計算モデルだが、抽象化は含まれていない。この利点は、ラムダ計算では、変数キャプチャの問題を避けるために置換の意味論を非常に慎重に指定する必要があるため、式の評価が非常に複雑になることである。対照的に、組み合わせ論理では置換の概念がないため、式の評価ははるかに簡単である。

組み合わせ計算

ラムダ計算では抽象化によってのみ関数を生成できるため、組み合わせ計算ではそれに代わる何らかの方法が必要となる。組み合わせ計算では、抽象化の代わりに、他の関数を構築するための限られた基本関数セットを提供する。

組み合わせ項

組み合わせ項は、以下のいずれかの形式をとります。

基本関数はコンビネータ、つまりラムダ項として見た場合、自由変数を含まない関数です。

表記を簡略化するために、一般的な慣例として、 $(E_{1}E_{2}E_{3}...E_{n})$ あるいは $E_{1}E_{2}E_{3}...E_{n}$ 、は用語を表します $(...((E_{1}E_{2})E_{3})...E_{n})$ これは、ラムダ計算における多重適用の場合と同じ一般的な慣例（左結合性）です。

組み合わせ論理の縮小

組み合わせ論理では、各基本コンビネータには次の形式の還元規則が付属する。

(P\ x_{1}\dots x_{n})=E

どこ $E$ セット内の変数のみに言及する用語です $\{x_{1}\dots x_{n}\}$ このようにして、原始的なコンビネータは関数のように振る舞う。

コンビネータの例

コンビネータの最も単純な例は $I$ 、同一性コンビネータ、定義は

(I\ x)=x

すべての条件について $x$ もう一つの単純なコンビネータは $K$ 定数関数を生成するもの： $(Kx)$ は、任意の引数に対して、 $x$ だから私たちは言う

((K\ x)\ y)=x

すべての条件について $x$ そして $y$ または、複数適用に関する慣例に従い、

(K\ x\ y)=x

3番目のコンビネータは $S$ これは、アプリケーションの一般化バージョンです。

(S\ x\ y\ z)=(x\ z\ (y\ z))

$S$ 適用する $x$ に $y$ 最初に置換した後 $z$ それぞれの中へ。言い換えれば、 $x$ 適用される $y$ 環境内部 $z$ 。

与えられた $S$ そして $K$ 、 $I$ それはそれ自体は不要である。なぜなら、他の2つから構築できるからである。

((S\,K\,K)\,x)

=(S\,K\,K)\,x

=K\,x\,(K\,x)

=x

いかなる期間においても $x$ . ただし、 $((S\,K\,K)\,x)=(Ix)$ いかなる場合でも $x$ 、 $(S\,K\,K)$ それ自体は等しくない $I$ 。これらの項は外延的に等しいと言います。外延的等価性は、関数の等価性という数学的概念を捉えています。つまり、2 つの関数は、同じ引数に対して常に同じ結果を生成する場合に等しいとみなされます。対照的に、項自体は、原始コンビネータの縮小とともに、関数の内包的等価性の概念を捉えています。つまり、2 つの関数は、原始コンビネータの展開まで同一の実装を持つ場合にのみ等しいとみなされます。恒等関数を実装する方法はたくさんあります。 $(S\,K\,K)$ そして $I$ これらもその方法の一つです。 $(S\,K\,S)$ もう一つはこれです。ここでは「等価」という言葉を外延的等価性という意味で使います。

より興味深いコンビネータは固定点コンビネータまたは $Y$ コンビネータは、再帰を実装するために使用できます。

SK基盤の完全性

SとKを組み合わせることで、任意のラムダ項と外延的に等しいコンビネータを生成でき、したがって、チャーチのテーゼによれば、あらゆる計算可能な関数と等価である。証明は、任意のラムダ項を等価なコンビネータに変換する変換T [ ]を提示することである。

T [ ] は次のように定義できます。

T [ x ] ⇒ x
T [( E ₁E ₂ )] ⇒ ( T [ E ₁ ] T [ E ₂ ])
T [ λx . E ] ⇒ ( K T [ E ]) ( x がEに自由に出現しない場合)
T [ λx . x ] ⇒ I
T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] ( xがEに自由に含まれる)
T [ λx .( E ₁E ₂ )] ⇒ ( S T [ λx . E ₁ ] T [ λx . E ₂ ]) ( x がE ₁またはE ₂に自由に存在する場合)

与えられたT [ ] は、型付けされた数学関数ではなく、項書き換え関数であることに注意してください。最終的にはコンビネータを生成しますが、変換によって、規則 (5) により、ラムダ項でもコンビネータでもない中間式が生成される場合があります。

このプロセスは抽象化除去とも呼ばれます。この定義は網羅的です。任意のラムダ式は、これらの規則のうち正確に1つに従います（上記のラムダ計算の概要を参照）。

これは、変数と適用から構築された式Eを受け取り、[ x ] E x = Eが成り立つような変数 x が自由でないコンビネータ式 [ x ]E を生成するブラケット抽象化のプロセスに関連しています。ブラケット抽象化の非常に単純なアルゴリズムは、式の構造に関する帰納法によって次のように定義されます。^[⁶^]

[ x ] y := K y
[ x ] x := I
[ x ]( E ₁E ₂ ) := S ([ x ] E ₁ )([ x ] E ₂ )

括弧抽象化は、括弧抽象化アルゴリズムを用いてラムダ抽象化を解釈することにより、ラムダ項からコンビネータ式への変換を誘導します。

ラムダ項を同等の組み合わせ項に変換する

例えば、ラムダ項λx . λy .( y x ) を組み合わせ項に変換してみましょう。

T [ λx . λy .( y x )]

= T [ λx . T [ λy .( y x ) ]] (5による)

= T [ λx .( S T [ λy . y ] T [ λy . x ])] (6による)

= T [ λx .( SI T [ λy . x ])] (4による)

= T [ λx .( SI ( K T [ x ]))] (3による)

= T [ λx .( SI ( K x ))] (1による)

= ( S T [ λx .( SI )] T [ λx .( K x )]) (6による)

= ( S ( K ( SI )) T [ λx .( K x )]) (3 による)

= ( S ( K ( SI )) ( S T [ λx . K ] T [ λx . x ])) (6 による)

= ( S ( K ( SI )) ( S ( KK ) T [ λx . x ])) (3 による)

= ( S ( K ( SI )) ( S ( KK ) I )) (by 4)

この組み合わせ項を任意の2つの項xとyに適用すると（それらをキューのように「右側から」コンビネータに投入することによって）、次のように簡略化されます。

( S ( K ( S I )) ( S ( K K ) I ) xy)

= ( K ( S I ) x ( S ( K K ) I x) y)

= ( S I ( S ( K K ) I x) y)

= ( I y ( S ( K K ) I xy))

= (y ( S ( K K ) I xy))

= (y ( K K x ( I x) y))

= (y ( K ( I x) y))

= (y ( I x))

= (yx)

組み合わせ表現 ( S ( K ( SI )) ( S ( KK ) I )) は、ラムダ項λx . λy .(yx) としての表現よりもはるかに長い。これは典型的な例である。一般に、T [ ] 構成は、長さn のラムダ項を長さΘ ( n ³ )の組み合わせ項に展開することができる。^[⁷^]

T [ ]変換の説明

T [ ] 変換は抽象化を排除したいという 願望から生じています。 2 つの特別なケース、ルール 3 と 4 は自明です。λx . xは明らかにIと等価であり、x がEで自由でない場合にλx . Eは明らかに ( K T [ E ])と等価です。

最初の2つのルールも単純です。変数はそれ自身に変換され、組み合わせ論的に許容される適用は、適用対象と引数をコンビネータに変換するだけでコンビネータに変換されます。

注目すべきはルール5とルール6です。ルール5は、複雑な抽象化をコンビネータに変換するには、まずその本体をコンビネータに変換し、次に抽象化を消去する必要があることを単純に述べています。ルール6は実際に抽象化を消去します。

λx .( E ₁E ₂ ) は、引数aを受け取り、それをxの代わりにラムダ項 ( E ₁E ₂ ) に代入して( E ₁E ₂ )[ x : = a ] を生成する関数です。しかし、xの代わりにa を( E ₁E _{2 ) に代入することは、}E ₁とE _{2 の}両方に代入することと同じなので、

( 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 )

外延的等価性により、

λx .( E ₁E ₂ ) = ( S λx . E ₁λx . E ₂ )

したがって、 λx .( E ₁E ₂ )と同等のコンビネータを見つけるには、( S λx . E ₁λx . E ₂ )と同等のコンビネータを見つけるだけで十分であり、

( S T [ λx . E ₁ ] T [ λx . E ₂ ])

明らかに条件を満たしています。 E ₁とE ₂はそれぞれ ( E ₁E _{2 ) よりも厳密に少ない適用を含んでいるため、再帰は適用がまったくないラムダ項 (変数、または}λx . Eの形式の項) で終了する必要があります。

変換の簡略化

η還元

T [ ]変換によって生成されるコンビネータは、η縮小 規則を考慮に入れると小さくすることができる。

T [ λx .( E x )] = T [ E ] ( xがEで自由でない場合)

λx .( E x) は、引数xを受け取り、関数Eを適用する関数です。これは、関数E自体と外延的に等価です。したがって、 E を組み合わせ形式に変換すれば十分です。

この簡略化を考慮すると、上記の例は次のようになります。

T [ λx . λy .( y x )]

= ...

= ( S ( K ( SI )) T [ λx .( K x )])

= ( S ( K ( SI )) K ) (η還元による)

このコンビネータは、先に述べたより長いコンビネータと同等です。

( S ( K ( SI )) K x y )

= ( K ( SI ) x ( K x ) y )

= ( SI ( K x ) y )

= ( I y ( K x y ))

= ( y ( K x y ))

= ( yx )

同様に、 T [ ] 変換の元のバージョンでは、恒等関数λf . λx .( f x ) が ( S ( S ( KS ) ( S ( KK ) I )) ( KI )) に変換されました。η 縮小規則では、λf . λx .( f x ) はIに変換されます。

1ポイントベース

あらゆるコンビネータを外延的に任意のラムダ項と等しく構成できるような一点基底が存在する。そのような基底の簡単な例は { X } であり、ここで次のようになる。

X ≡ λx .((x S ) K )

以下のことは容易に確認できる。

X ( X ( X X )) = ^βKおよび

X ( X ( X ( X X ))) = ^βS。

{ K , S } は基底であるため、{ X } も基底となる。Iotaプログラミング言語は、Xを唯一のコンビネータとして使用する。

1点基準のもう一つの簡単な例は次のとおりです。

X' ≡ λx .(x K S K ) で

( X' X' ) X' = ^βKおよび

X' ( X' X' ) = ^βS

最も単純な既知の1点基底は、Sを少し修正したものである。

S' ≡ λxλyλz . (xz) (y (λw. z))) で

S' ( S' S' ) ( S' ( S' S' ) S' S ' S' S ' S' ) = ^βKおよび

S' ( S' ( S' S' ( S' S' ( S' S' ))( S' ( S ' S ' ( S' S' )))))) S' S' = ^βS。

実際、そのような基底は無限に存在する。^{[ 8 ]}

コンビネータB、C

SとKに加えて、シェーンフィンケル（1924）は現在BとCと呼ばれる2つのコンビネータを含めており、以下の簡略化が行われている。

( C f g x ) = (( f x ) g )

( B f g x ) = ( f ( g x ))

彼はまた、それらがSとKのみを使用してどのように表現できるかについても説明しています。

B = ( S ( KS ) K )

C = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

これらのコンビネータは、述語論理やラムダ計算をコンビネータ式に変換する際に非常に役立ちます。これらはカリーによっても使用され、さらに後にはデビッド・ターナーによっても使用され、彼の名前はこれらの計算上の使用と関連付けられています。これらを使用すると、変換のルールを次のように拡張できます。

T [ x ] ⇒ x
T [( E ₁E ₂ )] ⇒ ( T [ E ₁ ] T [ E ₂ ])
T [ λx . E ] ⇒ ( K T [ E ]) ( xがEで自由でない場合)
T [ λx . x ] ⇒ I
T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] ( xがEの自由要素である)
T [ λx .( E ₁E ₂ )] ⇒ ( S T [ λx . E ₁ ] T [ λx . E ₂ ]) ( x がE ₁とE ₂の両方で自由である場合)
T [ λx .( E ₁E ₂ )] ⇒ ( C T [ λx . E ₁ ] T [ E ₂ ]) ( x がE ₁では自由だがE ₂では自由でない場合)
T [ λx .( E ₁E ₂ )] ⇒ ( B T [ E ₁ ] T [ λx . E ₂ ]) ( x がE ₂では自由だがE ₁では自由でない場合)

BおよびCコンビネータを使用すると、 λx . λy .( y x )の変換は次のようになります。

T [ λx . λy .( y x )]

= T [ λx . T [ λy .( y x )]]

= T [ λx .( C T [ λy . y ] x )] (規則7による)

= T [ λx .( C I x )]

= ( C I ) (η-還元)

={\mathsf {C}}_{*}

（伝統的な正統表記法：

{\mathsf {X}}_{*}={\mathsf {XI}}

）

={\mathsf {I}}'

（伝統的な正統表記法：

{\mathsf {X}}'={\mathsf {CX}}

）

そして実際、（C I x y ）は（ y x ）に簡略化されます。

( C I x y )

= ( I y x )

= ( y x )

ここで重要なのは、BとCはSの限定版であるという点です。Sは値を受け取り、適用前にその値を対象物とその引数の両方に代入しますが、Cは対象物のみに代入を行い、Bは引数のみに代入を行います。

コンビネータの現代的な名称は、ハスケル・カリーの1930年の博士論文に由来する（B、C、K、Wシステムを参照）。シェーンフィンケルの原著論文では、現在 S、K、I、B 、 Cと呼ばれているものは、それぞれS、C、I、Z、Tと呼ばれていた。

新しい変換規則によって生じるコンビネータサイズの縮小は、BとCを導入することなく達成することもでき、これはTromp（2008）のセクション3.2で実証されています。

CL _Kと CL _{I の}微積分

本稿で説明するCL _KとCL _I計算の間には区別を設ける必要がある。この区別はλ _Kとλ _I計算の区別に対応する。λ _K計算とは異なり、λ _I計算では抽象化を以下のように制限する。

λx . Eただし、 xはEに少なくとも 1 つの自由出現を持つ。

その結果、コンビネータKは λ _I計算にもCL _{I計算にも存在しません。CL}_Iの定数はI、B、C、Sであり、これらがすべてのCL _I項を構成する基底を形成します(等号を法として)。すべての λ _I項は、上記で λ _K項をCL _Kコンビネータに変換する場合と同様の規則に従って、外延的に等しいCL _Iコンビネータに変換できます。Barendregt (1984) の第 9 章を参照してください。

逆変換

組み合わせ項からラムダ項への変換L [ ]は自明である。

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 ₂ ])

ただし、この変換は、これまで見てきたT [ ]のどのバージョンの逆変換でもないことに注意してください。

組み合わせ計算の決定不能性

正規形とは、出現する原始的な組み合わせ子が、簡略化できるほど十分な引数に適用されていない組み合わせ項のことである。一般的な組み合わせ項が正規形を持つかどうか、2つの組み合わせ項が等価であるかどうかなどは、決定不能である。これは、ラムダ項に関する同様の問題と同様の方法で示すことができる。

述語による定義不可能性

上記の決定不能問題（同値性、正規形の存在など）は、適切な符号化（例えば、チャーチ符号化）の下での項の構文表現を入力として受け取ります。項の構文表現ではなく、項自体に直接適用されるコンビネータによって項のプロパティを「計算」する、おもちゃのような自明な計算モデルも考えることができます。より正確には、述語を、適用するとTまたはFを返すコンビネータとします（ここで、 TとF は、組み合わせ論理に変換された、真と偽の従来のチャーチ符号化λx . λy . xとλx . λy . yを表します。組み合わせバージョンでは、T = KおよびF = ( K I )となります）。述語Nは、 NA = TかつN B = Fとなる2 つの引数AとBが存在する場合に非自明です。コンビネータN は、すべての引数Mに対してN M が正規形を持つ場合に完全です。このおもちゃのモデルに対するライスの定理の類似物は、すべての完全な述語は自明であると述べている。この定理の証明はかなり簡単である。^[⁹^]

証拠

背理法による。完全な非自明な述語、例えばNがあると仮定する。N は非自明であると仮定されるため、次のような組み合わせ子AとBが存在する。

( NA ) = Tおよび

( N B ) = F。

否定を次のように定義する ≡ λx .(if ( N x ) then B else A ) ≡ λx .(( N x ) B A )

不条理を定義します ≡ ( Y否定)

不動点定理によれば、ABSURDUM = (NEGATION ABSURDUM) となります。

不条理 ≡ ( Y否定) = (否定 ( Y否定)) ≡ (不条理否定)。

Nは完全であると想定されているため、以下のいずれかになります。

（N ABSURDUM）= Fまたは
( N ABSURDUM) = T

ケース 1: F = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N A ) = T、矛盾です。
ケース2：T = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N B ) = F、これも矛盾です。

したがって、（N ABSURDUM）はTでもFでもなく、 Nが完全な非自明な述語であるという前提に矛盾する。証明終了

この定義不可能性定理から、正規形を持つ項と正規形を持たない項を区別できる完全な述語は存在しないことが直ちに導かれる。また、次のような完全な述語（例えば EQUAL）は存在しないことも導かれる。

(EQUAL AB ) = T は、 A = Bの場合に成立し、

(EQUAL AB ) = F (A ≠ B の場合)。

EQUALが存在するならば、すべてのAに対してλx. (EQUAL x A )は完全な非自明な述語でなければならない。

しかし、この定義不可能性の定理から、明らかに決定可能な項の多くの性質も完全な述語では定義できないことがすぐに導かれることに注意すべきである。例えば、項に最初に現れる原始関数文字がKであるかどうかを判定できる述語は存在しない。これは、述語による定義可能性が決定可能性の妥当なモデルではないことを示している。

アプリケーション

関数型言語のコンパイル

デビッド・ターナーは、自身のコンビネータを用いてSASLプログラミング言語を実装した。

Kenneth E. Iverson は、APLの後継である自身のプログラミング言語 Jで、Curry のコンビネータに基づくプリミティブを使用しました。これにより、Iverson が暗黙的プログラミングと呼んだもの、つまり変数を含まない関数式でのプログラミングが可能になり、そのようなプログラムを扱うための強力なツールも提供されました。暗黙的プログラミングは、ユーザー定義演算子を備えた APL ライクな言語であればどれでも可能であることが判明しました。^[¹⁰^]

論理

カリー・ハワード同型性は、論理学とプログラミングの間の関連性を示唆している。直観主義論理の定理の証明はすべて、型付きラムダ項の還元に対応し、その逆もまた然りである。さらに、定理は関数型のシグネチャと同一視できる。具体的には、型付き組み合わせ論理は、証明論におけるヒルベルト系に対応する。

KおよびSコンビネータは、以下の公理に対応します。

AK : A → ( B → A )

AS : ( A → ( B → C )) → (( A → B ) → ( A → C )),

そして関数適用は分離（モーダス・ポネンス）規則に対応する

MP : AとA → BからBを推論する。

AK、AS、MPからなる計算体系は、直観主義論理の含意部分については完全であり、それは次のように見ることができる。包含関係によって順序付けられた、演繹的に閉じたすべての論理式の集合の集合Wを考える。すると $\langle W,\subseteq \rangle$ は直観主義的クリプキフレームであり、モデルを定義します。 $\Vdash$ このフレーム内で

X\Vdash A\iff A\in X.

この定義は、→を満たす条件に従います。一方では、 $X\Vdash A\to B$ 、そして $Y\in W$ は、 $Y\supseteq X$ そして $Y\Vdash A$ 、それから $Y\Vdash B$ モーダス・ポネンスによって。一方、もし $X\not \Vdash A\to B$ 、それから $X,A\not \vdash B$ 演繹定理により、演繹的閉包は $X\cup \{A\}$ 要素です $Y\in W$ そのため $Y\supseteq X$ 、 $Y\Vdash A$ 、そして $Y\not \Vdash B$ 。

A を、計算において証明できない任意の式とする。このとき、Aは空集合の演繹的閉包Xに属さないので、 $X\not \Vdash A$ 、そしてAは直観的に妥当ではない。

参考文献

↑ Schönfinkel 1924、組み合わせ論理の基礎を築いた論文。英語訳: Schönfinkel (1967)。
↑カリー 1930。
↑セルディン 2008。
↑ Barendregt 1984 .
↑ヒンドレー＆メレディス 1990。
↑ターナー 1979。
↑ラホウスキー 2018。
↑ゴールドバーグ 2004。
↑エンゲラー 1995。
↑チェルリン 1991。

文学

バレンデレヒト、ヘンドリック・ピーター（1984）。ラムダ計算、その構文と意味論。論理学と数学の基礎に関する研究。第 103巻。ノース・ホランド。ISBN 0-444-87508-5。
ビンボ、カタリン (2012)。組み合わせロジック: 純粋、応用、型付き。ISBN 978-1-4398-0000-3。
Cherlin, Edward (1991). 「APLとJにおける純粋関数」。APL '91国際会議議事録 - APL '91。pp . 88–93。doi : 10.1145 /114054.114065。ISBN 0897914414. S2CID 25802202 .
カリー、ハスケル・ブルックス(1930)。「組合せ論理の基礎」。American Journal of Mathematics (ドイツ語)。52 ( 3)。ジョンズ・ホプキンス大学出版局: 509–536。doi : 10.2307 / 2370619。JSTOR 2370619。
カリー、ハスケル・ブルックス、フェイズ、ロバート（1958）。組み合わせ論理学。第 1巻。アムステルダム：ノース・ホランド。ISBN 0-7204-2208-6。{{cite book}}ISBN /日付の不一致（ヘルプ）
カリー、ハスケル・ブルックス；ヒンドリー、J・ロジャー；セルディン、ジョナサン・P（1972）。組み合わせ論理学。第 II巻。アムステルダム：ノース・ホランド。ISBN 0-7204-2208-6。
エンゲラー、E. (1995)。組み合わせプログラム(PDF)。ビルクホイザー。5～ 6ページ。
フィールド、アンソニー・J.、ハリソン、ピーター・G. (1998).関数型プログラミング. アディソン・ウェスリー. ISBN 0-201-19249-7。
Goldberg, Mayer (2004). 「拡張ラムダ計算における一点基底の構成」. Information Processing Letters . 89 (6): 281–286 . doi : 10.1016/j.ipl.2003.12.005 .
Hindley, J. Roger ; Meredith, David (1990). "主型スキームと凝縮分離" . Journal of Symbolic Logic . 55 (1): 90– 105. doi : 10.2307/2274956 . JSTOR 2274956 . MR 1043546 . S2CID 6930576 .
Hindley, J. Roger ; Seldin, Jonathan P. (2008) [1986].ラムダ計算とコンビネータ：入門（第2 版）. Cambridge University Press . ISBN 9780521898850。
Lachowski, Łukasz (2018). 「ラムダ計算の組み合わせ論理への標準変換の複雑性について」 . Reports on Mathematical Logic . 2018 (53): 19–42 . doi : 10.4467/20842589RM.18.002.8835 . 2018年9月9日取得。
ポールソン、ローレンス C. (1995).関数型プログラミングの基礎. ケンブリッジ大学。
クワイン、ウィラード・ヴァン・オーマン（1960）。「説明された変数」。アメリカ哲学会紀要。104（3）：343–347。JSTOR 985250。クワイン（1996）の第23章として再録。
クワイン、ウィラード・ヴァン・オーマン( 1996) [ 1960]。「変数の説明」。『論理学論文選集』（増補版、第2版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。227-235頁。ISBN 9780674798373。
モーセのシェーンフィンケル(1924)。「バウスタインの数学的論理学」(PDF)。Mathematische Annalen (ドイツ語)。92 ( 3–4 ): 305–316 .土井: 10.1007/bf01448013。S2CID 118507515。組み合わせ論理を確立した記事。英語翻訳:シェーンフィンケル (1967)
シェーンフィンケル、モーセ(1967) [1924]。Van Heijenoort、Jean (編)。Über die Bausteine der mathematischen Logik [数学的論理の構成要素について]。フレーゲからゲーデルまで: 数理論理学の情報源の本、1879 ～ 1931 年。シュテファン・バウアー＝メンゲルベルク訳。米国マサチューセッツ州ケンブリッジ: Harvard University Press。355 ～ 366ページ。ISBN 978-0674324497. OCLC 503886453 .
セルディン、ジョナサン P. (2008 年 3 月 3 日)。「カレーと教会の論理」(PDF) 。2023年9 月 17 日取得。
スムリアン、レイモンド（1985）。『モッキンバードを嘲笑う、そして組み合わせ論理の驚くべき冒険を含むその他の論理パズル』。クノップフ。ISBN 0-394-53491-3組み合わせ論理への穏やかな入門書。鳥の観察を比喩として用いた、一連の楽しいパズル形式で提示される。
スムリアン、レイモンド（ 1994）。対角線と自己参照。オックスフォード論理ガイド。第 27巻。オックスフォードおよびニューヨーク：オックスフォード大学出版局。ISBN 978-0198534501第17章から第20章は、組み合わせ論理のより正式な入門であり、特に不動点定理に重点を置いている。
Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999].カリー・ハワード同型性に関する講義(PDF) . 論理学と数学の基礎に関する研究. 第 149 巻 (第 1 版). Elsevier . p. 442. ISBN 978-04445207772005年10月16日にオリジナル（PDF）からアーカイブされました。2017年4月22日に取得。
Tromp, John (2008). 「二項ラムダ計算と組み合わせ論理」(PDF) . Calude, Cristian S. (編) 『ランダム性と複雑性：ライプニッツからチャイティンまで』所収。World Scientific Publishing Company。2016年3月4日にオリジナル(PDF)からアーカイブ済み。
Turner, David A. (1979). 「括弧抽象化のための別のアルゴリズム」。『記号論理学ジャーナル』44 ( 2 ): 267–270。doi : 10.2307/ 2273733。JSTOR 2273733。S2CID 35835482。
Wolfengagen, VE (2003).プログラミングにおける組み合わせ論理：例と演習によるオブジェクトを用いた計算（第2 版）。モスクワ：Center JurInfoR Ltd. ISBN 5-89158-101-9。
Wolfram, Stephen (2021). Combinators: A Centennial View . Wolfram Media . ISBN 978-1-57955-043-1シェーンフィンケル（1924年）によってコンビネータが提唱されてから100年を記念する祝賀行事。(電子書籍: ISBN) 978-1-57955-044-8）

外部リンク

スタンフォード哲学百科事典：「組み合わせ論理」カタリン・ビンボ著。
1920年～1931年のカリーのブロックノート。
キーナン、デイビッド・C. (2001) 「モッキンバードを解剖する：アニメーションによる簡約化を用いたラムダ計算の図式表記法」
ラスマン、クリス、「コンビネーターバード」。スムリアン（1985）のエッセンスを凝縮した表。
ドラッグ＆ドロップで操作できるコンビネータ。（Javaアプレット）
二項ラムダ計算と組み合わせ論理。
組み合わせ論理削減ウェブサーバー
Wolfram, Stephen (2020年4月29日). Combinators: 100周年記念. Wolfram Physics Project on YouTube . 2023年9月26日閲覧.

[FOOTNOTESchönfinkel1924The_article_that_founded_combinatory_logic._English_translation:_[[#CITEREFSchönfinkel1967|Schönfinkel_(1967)]]-1] Schönfinkel 1924、組み合わせ論理の基礎を築いた論文。英語訳: Schönfinkel (1967)。

[FOOTNOTECurry1930-2] カリー 1930。

[FOOTNOTESeldin2008-3] セルディン 2008。

[FOOTNOTEBarendregt1984-4] Barendregt 1984 .

[FOOTNOTEHindleyMeredith1990-5] ヒンドレー＆メレディス 1990。

[FOOTNOTETurner1979-6] ターナー 1979。

[FOOTNOTELachowski2018-7] ラホウスキー 2018。

[FOOTNOTEGoldberg2004-8] ゴールドバーグ 2004。

[FOOTNOTEEngeler1995-9] エンゲラー 1995。

[FOOTNOTECherlin1991-10] チェルリン 1991。

2

[ 3 ]

4

[ 5 ]

[

[

[ 8 ]

[

[

数学において

コンピューティングにおいて

ラムダ計算の概要

組み合わせ計算

組み合わせ項

組み合わせ論理の縮小

コンビネータの例

SK基盤の完全性

ラムダ項を同等の組み合わせ項に変換する

T [ ]変換の説明

変換の簡略化

η還元

1ポイントベース

コンビネータB、C

CL Kと CL I の微積分

逆変換

組み合わせ計算の決定不能性

述語による定義不可能性

アプリケーション

関数型言語のコンパイル

論理

関連項目

参考文献

文学

外部リンク

CL _Kと CL _{I の}微積分