組み合わせ論理

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

組合せ論理は、もともとは量化変数を本質的に排除することによって、論理における量化変数の役割を明確にする「前論理」として意図されていました。量化変数を排除する別の方法は、クワインの 述語関数論理です。組合せ論理の表現力は通常、一階述語論理の表現力を上回りますが、述語関数論理の表現力は一階述語論理と同じです (Quine 1960、1966、1976)。

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

コンピュータサイエンスにおいて、組み合わせ論理は計算の簡略化されたモデルとして使用され、計算可能性理論と証明理論で使用されます。組み合わせ論理は単純ですが、計算の多くの重要な特徴を捉えています。

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

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

ラムダ計算は、ラムダ項と呼ばれるオブジェクトを扱います。これは、次の 3 つの形式の文字列で表すことができます。

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

ここで、⁠ ⁠ は、${\displaystyle v}$定義済みの無限の変数名セットから抽出された変数名であり、⁠ ⁠${\displaystyle E_{1}}$および⁠ ⁠ は${\displaystyle E_{2}}$ラムダ項です。

⁠ ⁠${\displaystyle \lambda v.E_{1}}$の形式の項は抽象化と呼ばれます。変数v は抽象化の仮パラメータと呼ばれ、 ⁠ ⁠ は${\displaystyle E_{1}}$抽象化の本体です。項⁠ ⁠${\displaystyle \lambda v.E_{1}}$は、引数に適用され、仮パラメータv を引数にバインドし、⁠ ⁠${\displaystyle E_{1}}$の結果の値を計算する関数を表します。つまり、vのすべての出現を引数に置き換えた ⁠ ⁠ を返します。${\displaystyle E_{1}}$

⁠ ⁠ の${\displaystyle (E_{1}E_{2})}$形式の項は、アプリケーションと呼ばれます。アプリケーションは、関数の呼び出しまたは実行をモデル化します。つまり、⁠ ⁠で表される関数が、 ${\displaystyle E_{1}}$⁠ ⁠ を${\displaystyle E_{2}}$引数として呼び出され、結果が計算されます。⁠ ⁠ (${\displaystyle E_{1}}$アプリケーション対象と呼ばれることもあります) が抽象化である場合、項は簡約されることがあります。つまり、引数⁠ ⁠は、 ${\displaystyle E_{2}}$⁠ ⁠の仮パラメータの代わりに⁠ ⁠${\displaystyle E_{1}}$の本体に代入され、結果は古いものと同等の新しいラムダ項になります。ラムダ項に⁠ ⁠の形式の部分項が含まれていない場合、それは簡約できず、通常の形式であると言われます。 ${\displaystyle E_{1}}$${\displaystyle ((\lambda v.E_{1})E_{2})}$

⁠ ⁠${\displaystyle E[v:=a]}$という式は、項Eを取り、その中のvの出現すべてをaに置き換えた結果を表します。したがって、次のように書きます。

⁠ ⁠${\displaystyle ((\lambda vE)a)\Rightarrow E[v:=a]}$

慣例により、⁠ ⁠ を${\displaystyle (abc)}$⁠ ⁠${\displaystyle ((ab)c)}$の省略形として使用します(つまり、適用は左結合です)。

この簡約の定義の動機は、それがすべての数学関数の本質的な動作を捉えているからです。例えば、数の2乗を計算する関数を考えてみましょう。次のように書くことができます。

xの2乗は⁠ ⁠${\displaystyle x*x}$

(乗算を示すために 「 ⁠ ⁠ 」を使用します。) ここでの${\displaystyle *}$x は関数の仮パラメータです。特定の引数 (たとえば 3) の平方を評価するには、仮パラメータの代わりに定義に挿入します。

3の2乗は⁠ ⁠${\displaystyle 3*3}$

結果の式⁠ ⁠${\displaystyle 3*3}$を評価するには、乗算と数値 3 に関する知識に頼らなければなりません。あらゆる計算は、適切な基本引数に対する適切な関数の評価の組み合わせにすぎないため、この単純な置換原理で、計算の本質的なメカニズムを捉えるのに十分です。さらに、ラムダ計算では、「3」や「⁠ ⁠${\displaystyle *}$」などの概念は、外部で定義された基本演算子や定数を必要とせずに表現できます。ラムダ計算では、適切に解釈すると数値 3 や乗算演算子のように動作する項を特定できます ( Church エンコーディングを参照) 。

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

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

ラムダ計算では抽象化が関数を作成する唯一の方法であるため、組み合わせ計算では抽象化を置き換える必要があります。組み合わせ計算では、抽象化の代わりに、他の関数を構築できる限られた基本関数のセットを提供します。

組み合わせ項は次のいずれかの形式になります。

プリミティブ関数はコンビネータ、つまりラムダ項として見たときに自由変数を含まない関数です。

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

組合せ論理では、各基本コンビネータには次の形式の簡約規則が付随する。

( P × ₁ ... × _n ) = E

ここで、E は集合{ x ₁ ... x _n }の変数のみを表す項です。このようにして、プリミティブコンビネータは関数として動作します。

最も単純なコンビネータの例は、次のように定義される恒等コンビネータ Iである。

(私 x ) = x

全ての項xに対してである。もう一つの単純なコンビネータはKであり、定数関数を生成する。( K x ) は任意の引数に対してx を返す関数なので、

(( K x ) y ) = x

すべての項xとyについて。あるいは、多重適用の慣例に従って、

( K x y ) = x

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

( S x yz ) = ( xz ( yz ))

S は、まず各要素にz を代入してから、 x をyに適用します。言い換えると、x は環境z内でyに適用されます。

SとKが与えられれば、I自体は不要です。他の 2 つから構築できるからです。

(( SKK ) x )

= ( SKK x )

= ( K x ( K x ))

= x

任意の項xについて成り立ちます。任意のxについて(( SKK ) x ) = ( I x )ですが、 ( SKK ) 自体はIと等しくないことに注目してください。これらの項は外延的に等しいといいます。外延的等価性は、関数の等価性という数学的な概念をとらえています。つまり、 2 つの関数が同じ引数に対して常に同じ結果を生成する場合、それらの関数は等しいということです。対照的に、項自体は、原始コンビネータの簡約とともに、関数の内包的等価性という概念をとらえています。つまり、 2 つの関数は、原始コンビネータの展開まで同一の実装を持つ場合のみ等しいということです。恒等関数を実装する方法は多数あります。( SKK ) とI は、これらの方法の 1 つです。( SKS ) も別の方法です。外延的等価性を示すために「同等」という語を使用し、同一の組み合わせ項に対しては 「等しい」を使用します。

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

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

T [ ]は次のように定義されます。

1. T [ x ] ⇒ x
2. T [( E ₁ E ₂)] ⇒ ( T [ E ₁] T [ E ₂])
3. T [ λx . E ] ⇒ ( K T [ E ]) （ xがE内で自由に出現しない 場合）
4. T [ λx . x ] ⇒ I
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]]（ x がE内で自由に出現する）
6. T [ λx .( E ₁ E ₂)] ⇒ ( S T [ λx . E ₁] T [ λx . E₂ ]) ( x がE ₁ またはE ₂に自由に出現する場合

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

このプロセスは、抽象化除去とも呼ばれます。この定義は網羅的です。つまり、すべてのラムダ式は、これらのルールの 1 つだけに従います (上記のラムダ計算の概要を参照)。

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

1. [ x ] y  := K y
2. [ x ] x  :=私
3. [ x ]( E1 E2 ) := S ([ x ] E1 )([ x ] E2 )

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

たとえば、ラムダ項λx . λy .( y x ) を組み合わせ項に変換します。

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

= 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 ³ )の組合せ項に拡張することがあります。^[7]

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の代わりに( E ₁ E ₂)にa を代入することは、 E ₁ と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 )

外延的平等により、

λ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 ₂ ) よりも厳密に少ない適用が含まれているため、再帰は適用がまったくないラムダ項、つまり変数またはλx . Eの形式の項で終了する必要があります。

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

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

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

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

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

= ...

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

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

SとKに加えて、Schönfinkel (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 ))

これらのコンビネータは、述語論理やラムダ計算をコンビネータ式に変換するときに非常に便利です。これらはCurryによっても使用され、その後David Turnerによっても使用され、その名前は計算での使用と関連付けられています。これらを使用すると、変換の規則を次のように拡張できます。

1. T [ x ] ⇒ x
2. T [( E₁ E₂ )] ⇒ ( T [ E₁ ] T [ E₂ ])
3. T [ λx . E ] ⇒ ( K T [ E ]) ( x がE内で自由でない 場合)
4. T [ λx . x ] ⇒ I
5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]]（ x がE内で自由である）
6. T [ λx .( E₁ E₂ )] ⇒ ( S T [ λx . E₁ ] T [ λx . E₂ ]) ( x がE₁とE₂ の両方で自由である場合)
7. T [ λx .( E₁ E₂ )] ⇒ ( C T [ λx . E₁ ] T [ E₂ ]) ( xがE₁では自由だがE₂では自由でない場合)
8. T [ λx .( E₁ E₂ )] ⇒ ( B T [ E₁ ] T [ λx . E₂ ]) ( xがE₂では自由だがE₁では自由でない場合)

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

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

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

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

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

= ( C I ) (η-還元)

${\displaystyle =\mathbf {C} _{*}}$(伝統的な標準表記法: )${\displaystyle \mathbf {X} _{*}=\mathbf {XI} }$

${\displaystyle =\mathbf {I} '}$(伝統的な標準表記法: )${\displaystyle \mathbf {X} '=\mathbf {CX} }$

そして実際、( C I x y )は( y x )に簡約されます。

  ( C I x y )

= (私 y x )

= ( y x )

ここでの動機は、BとC がSの限定バージョンであるということです。S は値を受け取り、適用を実行する前にそれを適用対象と引数の両方に代入しますが、C は適用対象でのみ代入を実行し、B は引数でのみ代入を実行します。

コンビネータの現代的な名前は、 1930 年のHaskell Curry博士論文に由来しています ( B、C、K、W システムを参照)。Schönfinkelの元の論文では、現在 S 、 K 、 I 、 B 、 C と呼ばれる ものは、それぞれS 、 C 、 I 、 Z 、 Tと呼ばれていました。

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

この記事で説明されている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が非自明なのは、2 つの引数AとBがあり、 N A = TかつN B = Fである場合です。コンビネータNが完全であるのは、 N M がすべての引数Mに対して正規形を持つ場合です。このおもちゃのモデルに対するライスの定理の類似は、すべての完全な述語は自明であるということです。この定理の証明はかなり簡単です。^[9]

この定義不可能定理から、正規形を持つ項と正規形を持たない項を区別できる完全な述語は存在しないということが直ちに分かります。また、EQUAL などの完全な述語は存在しないということも分かります。

(等しいAB ) = T 、 A = Bの場合、かつ

A ≠ Bの場合、(EQUAL AB ) = Fとなります。

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

ただし、この定義不可能性定理からは、明らかに決定可能な項の多くの特性も完全な述語によって定義できないということも直ちに導かれることに注意してください。たとえば、項に現れる最初の原始関数文字がKであるかどうかを判断できる述語は存在しません。これは、述語による定義可能性が決定可能性の合理的なモデルではないことを示しています。

David Turner は、コンビネータを使用してSASL プログラミング言語を実装しました。

ケネス・E・アイバーソンは、 APLの後継であるプログラミング言語Jで、カリーのコンビネータに基づくプリミティブを使用しました。これにより、アイバーソンが暗黙のプログラミングと呼んだ、変数を含まない関数式でのプログラミングと、そのようなプログラムを操作する強力なツールが可能になりました。暗黙のプログラミングは、ユーザー定義の演算子を持つAPLのような言語で可能であることがわかりました。^[10]

カリー・ハワード同型性は、論理とプログラミングの関係を暗示しています。直観論理の定理の証明はすべて、型付きラムダ項の簡約に対応し、その逆もまた同様です。さらに、定理は関数の型シグネチャで識別できます。具体的には、型付き組み合わせ論理は、証明理論のヒルベルト システムに対応します。

KおよびSコンビネータは公理に対応する 。

AK : A → ( B → A )、

: ( A → ( B → C )) → (( A → B ) → ( A → C )) 、

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

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

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

${\displaystyle X\Vdash A\iff A\in X.}$

この定義は、→ の充足条件に従います。一方で、 、および がかつとなるようなものである場合、モーダスポネンスにより となります。他方で、の場合、演繹定理により、したがって の演繹閉包は、、および となるような元となります。 ${\displaystyle X\Vdash A\to B}$${\displaystyle Y\in W}$${\displaystyle Y\supseteq X}$${\displaystyle Y\Vdash A}$${\displaystyle Y\Vdash B}$${\displaystyle X\not \Vdash A\to B}$${\displaystyle X,A\not \vdash B}$${\displaystyle X\cup \{A\}}$${\displaystyle Y\in W}$${\displaystyle Y\supseteq X}$${\displaystyle Y\Vdash A}$${\displaystyle Y\not \Vdash B}$

A を微積分では証明できない任意の式とします。すると、 A は空集合の演繹閉包Xに属さないため、A は直観的に有効ではありません。 ${\displaystyle X\not \Vdash A}$

• 応用コンピューティングシステム
• B、C、K、Wシステム
• カテゴリカル抽象マシン
• 組み合わせ範疇文法
• 明示的な置換
• 固定小数点コンビネータ
• グラフ削減マシン
• ラムダ計算と円筒代数、モデリングの定量化と変数の除去への他のアプローチ
• SKIコンビネータ計算
• スーパーコンビネーター
• マネシツグミをあざける

• Barendregt, Hendrik Pieter (1984)。ラムダ計算、その構文と意味論。論理学と数学の基礎研究。第 103 巻。北ホラント。ISBN 0-444-87508-5。
• Cherlin, Edward (1991)。「APLとJ の純粋関数」。APL '91 国際会議議事録 - APL '91。pp. 88–93。doi : 10.1145 /114054.114065。ISBN 0897914414.S2CID 25802202  。
• カリー、ハスケル・ブルックス( 1930)。「組合せ論理の基礎」[組合せ論理の基礎]。アメリカ数学ジャーナル(ドイツ語) 。52 (3)。ジョンズ・ホプキンス大学出版局: 509–536。doi :10.2307/2370619。JSTOR  2370619。
• カリー、ハスケル・ブルックス、フェイズ、ロバート（1958年）。組合せ論理学。第1巻。アムステルダム：北ホラント。ISBN 0-7204-2208-6。
• カリー、ハスケル・ブルックス、ヒンドリー、J. ロジャー、セルディン、ジョナサン P. (1972)。組合せ論理。第 2 巻。アムステルダム: 北ホラント。ISBN 0-7204-2208-6。
• エンゲラー、E. (1995)。組み合わせプログラム(PDF)。ビルクホイザー。 5～6ページ。
• フィールド、アンソニー J.;ハリソン、ピーター G. (1998)。関数型プログラミング。Addison- Wesley。ISBN 0-201-19249-7。
• Goldberg, Mayer (2004). 「拡張ラムダ計算における 1 点基底の構築」. 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]. Lambda-Calculus and Combinators: An Introduction (第2版). Cambridge University Press . ISBN 9780521898850。
• Lachowski, Łukasz (2018). 「ラムダ計算から組合せ論理への標準的な変換の複雑さについて」。数理論理学に関する報告。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]。「変数の説明」。Selected Logic Papers ( Enl. ed.、第 2 版)。マサチューセッツ州ケンブリッジ:ハーバード大学出版局。pp. 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)。『アラバマ物語とその他の論理パズル、組み合わせ論理の驚くべき冒険を含む』。Knopf。ISBN 0-394-53491-3組み合わせ論理へのやさしい入門書。バードウォッチングの比喩を使った一連の娯楽パズルとして紹介されています。
• スマリヤン、レイモンド（1994）。対角化と自己言及。オックスフォードロジックガイド。第27巻。オックスフォードおよびニューヨーク：オックスフォード大学出版局。ISBN 978-0198534501第 17 章から第 20 章は、組み合わせ論理のより正式な入門であり、特に固定小数点の結果に重点を置いています。
• Sørensen, Morten Heine B; Urzyczyn, Paweł (2006) [1999]. Curry–Howard 同型性に関する講義(PDF) . 論理学と数学の基礎研究。第 149 巻 (第 1 版) 。Elsevier。p . 442。ISBN 978-0444520777. 2005年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). 「括弧抽象化のための別のアルゴリズム」. The Journal of Symbolic Logic . 44 (2): 267–270. doi :10.2307/2273733. JSTOR  2273733. S2CID  35835482.
• Wolfengagen, VE (2003)。プログラミングにおける組み合わせ論理: 例と演習によるオブジェクトの計算 (第 2 版)。モスクワ: "Center JurInfoR" Ltd. ISBN 5-89158-101-9。
• ウルフラム、スティーブン（2021）。コンビネータ： 100年にわたる展望。ウルフラムメディア。ISBN 978-1-57955-043-1シェーンフィンケル (1924) によって導入されてから 100 年後のコンビネータの発展を祝う（電子書籍：ISBN 978-1-57955-044-8） 

• スタンフォード哲学百科事典：「組み合わせ論理」、Katalin Bimbó著。
• 1920–1931 カリーのブロックノート。
• Keenan, David C. (2001)「アラバマ物語を解剖する: アニメーションによる簡約化によるラムダ計算のグラフィカル表記法」
• Rathman, Chris、「Combinator Birds」。Smullyan (1985) のエッセンスの多くを抽出した表。
• ドラッグ アンド ドロップ コンビネータ (Java アプレット)
• バイナリラムダ計算と組み合わせ論理。
• 組み合わせ論理削減ウェブサーバー
• Wolfram, Stephen (2020年4月29日). コンビネータ: 100周年記念。YouTubeのWolfram Physics Project 。 2023年9月26日閲覧。