表記法 このシステムにおけるオブジェクトの最も正式な表現は二分木を必要とするが、組版を簡略化するために、それらはしばしば括弧で囲まれた式として表現され、それが表す木の略記法となる。任意のサブツリーを括弧で囲むことができるが、多くの場合、右側のサブツリーのみが括弧で囲まれ、括弧のない適用については左結合性が暗黙的に示される。例えば、ISK は (( IS ) K ) を意味する。この表記法を用いると、左サブツリーが木KS で右サブツリーが木SKである木は KS ( SK )と書くことができる。より明示的な表現が必要な場合は、暗黙の括弧も含めることができる。(( KS )( SK ))。
非公式に、そしてプログラミング言語の専門用語を用いると、木 ( xy ) は、関数x を引数y に適用したものと考えることができます。評価されるとき (つまり 、「関数」が引数に「適用」されるとき)、木は「値を返す」、つまり 別の木に変換されます。「関数」、「引数」、「値」は、コンビネータまたは適用ノードを持つ二分木のいずれかです。二分木の場合は、必要に応じて関数と考えることもできます。
評価操作 は次のように定義されます。
( x 、y 、zは 、コンビネータS 、K 、I から作成された式を表し、場合によっては、まだ特定されていないSKI 式を表す変数である可能性があります)。
。
I x = x Kを任意の引数 x に適用すると、1 つの引数を持つ定数関数K x が生成され、これを任意の引数y に適用すると、x が返されます。
K xy = x S は置換演算子です。3つの引数を取り、最初の引数を3番目の引数に適用した結果を返し、その結果を2番目の引数を3番目の引数に適用した結果に再度適用します。より明確に言うと次のようになります。
S xyz = xz ( yz )計算例：SKSK は S ルールによりKK ( SK )と評価されます。次にKK ( SK ) を評価すると、 K ルールによりK が得られます。これ以上適用できるルールがないため、計算はここで停止します。
すべての木x とすべての木y に対して、SK xy は 常に2 段階でyに評価されます。K y ( xy ) = yなので、 SK xy の評価の最終結果は常にy の評価結果と同じになります。SK x とIは 、任意の x に対して「機能的に同等」であると言えます。なぜなら、これらは任意のy に適用したときに常に同じ結果をもたらすからです 。
これらの定義から、SKI計算は最小限のシステムでありながら、ラムダ計算のあらゆる計算を完全に実行できることが示されます。任意の式中のIは、任意の xに対して( SKK )または( SKS )または( SK x )に置き換えることができ、結果として得られる式は同じ結果になります。したがって、「I 」は単なる構文糖衣 です。Iは省略可能であるため、このシステムは SK計算 またはSKコンビネータ計算 とも呼ばれます。
1つの（不適切な）コンビネータのみを使用して完全なシステムを定義することが可能です。例として、クリス・バーカー のイオタコンビネータがあり、これは S とK を用いて次のように表現できます。
ι x = x SK = S (λ x . x S )(λ x . K ) x = S ( S (λ x . x )(λ x . S ))( KK ) x = S ( SI ( KS ))( KK ) x イオタコンビネータからS 、K 、I を 再構成することが可能です。ι をそれ自身に適用すると、ιι = ι SK = SSKK = SK ( KK ) となり、これはI と機能的に等価です。Kは、 ι を I に 2 回適用することによって構築できます(これは ι をそれ自身に適用することと等価です)。ι(ι(ιι)) = ι(ιι SK ) = ι ( ISK ) = ι( SK ) = SKSK = K 。ι をもう 1 回適用すると、ι(ι(ι(ιι))) = ι K = KSK = S となります。
基底を形成する最も単純な項は X = λ f . f ( λ xyz . x z ( y z ) ) (λ xyz . x ) であり、これは XX = K および X (XX) = S を 満たします。
この体系における用語と導出は、より形式的に定義することもできる。
用語 ：用語の集合T は、以下の規則によって再帰的に定義されます。
S 、K 、I は用語です。τ 1 とτ 2 が項である場合、( τ 1 τ 2 ) は項です。最初の2つの規則によってそうであると定められていない限り、何ものも用語ではない。 導出 ：導出とは、次の規則によって再帰的に定義される有限個の項の列です（ここで、 α とι はアルファベット{ S 、K 、I 、（、）}上の単語であり、 β 、γ 、δ は項です）。
Δ がα ( I β) ι の形式の式で終わる導出である場合、Δ に続く項αβι は導出である。Δ がα (( K β) γ ) ι の形式の式で終わる導出である場合、Δ に続く項αβι は導出である。Δ がα ((( S β) γ ) δ ) ι の形式で終わる導関数である場合、 Δ の後に項α (( βδ )( γδ )) ι が続く導関数です。そもそも有効な導出である数列は、これらの規則を用いて拡張することができる。長さ1の導出はすべて有効な導出である。
ラムダ項をSKIコンビネータに変換する 外延性により、ラムダ計算の式は、以下の規則に従って、対応するSKIコンビネータ計算の式に変換できます。
λ x . x = I λ x . c = K c (ただし、c はx に依存しない) λ x . c x = c (ただし、c はx に依存しない) λ x 。y z = S (λ x . y ) (λ x . z ) 任意の引数に適用した場合、各規則の左辺式と右辺式はどちらも同じ結果を生成する。
SKI式
自己適用と再帰 SIIは 、引数を受け取り、その引数を自身に適用する式です。
SII α = I α ( I α ) = αα これはU コンビネータ、U x = xx とも呼ばれます。その興味深い性質の一つは、自己適用が既約であることです。
SII ( SII ) = I ( SII )( I ( SII )) = SII ( I ( SII )) = SII ( SII )または、方程式U x = xx を 定義として直接使用すると、すぐにU U = U U が得られます。
もう一つの利点は、あるものを別のものの自己適用に適用する関数を作成できることです。
( S ( K α )( SII )) β = K αβ ( SII β ) = α ( I β( I β )) = α ( ββ ) あるいは、 H xy = x ( yy )という別のコンビネータを直接定義するものと見なすこともできる。
この関数は再帰を 実現するために使用できます。βが α を他の何かの自己適用に適用する関数である場合、
β = H α = S ( K α )( SII )すると、このβ の自己適用は、そのα の固定点となる。
SII β = ββ = α ( ββ ) = α ( α ( ββ )) =… \displaystyle \ldots } または、導出された定義から直接、H α ( H α ) = α ( H α ( H α )) となります。
α が 、あるρ とνに対して αρν によって計算される「計算ステップ」を表す場合、ρν′ が 「残りの計算」（α が ν から「計算」するあるν′ に対して）を表すと仮定すると、その固定点ββ は 再帰計算全体を表します。なぜなら、 「残りの計算」呼び出しに同じ関数 ββ を使用すること（ ββν = α ( ββ ) ν ）は再帰の定義そのものだからです。ρν ′ = ββν′ = α(ββ)ν′ = ... 。項α は、発散を避けるために、何らかの「基本ケース」で停止し、その時点で再帰呼び出しを行わないように、何らかの条件式を使用する必要があります。
これは次のように形式化できます。
β = H α = S ( K α )( SII ) = S ( KS ) K α ( SII ) = S ( S ( KS ) K )( K ( SII )) α として
Y α = SII β = SII ( H α ) = S ( K ( SII )) H α = S ( K ( SII ))( S ( S ( KS ) K )( K ( SII ))) α これにより、 Y コンビネータの可能なエンコードの1つが 得られます。より短いバリエーションでは、 H α( H α) = SHH α = SSIH αであるため、その2つの先頭のサブタームを単にSSIに置き換えます。
B、C、W コンビネータ同等のコードがはるかに短くなります。
Y α = S ( KU )( SB ( KU ))α = U ( B α U ) = BU ( CBU )α = SSI ( CBU )αそして、擬似Haskell 構文では、非常に短いY = U . (. U )となります。
このアプローチに従うと、他の不動点コンビネータの定義も可能になります。したがって、
H gx = g ( xx ) ; Y g = H g ( H g ) ; Y = S(KU)(SB(KU)) = SS(S(S(KS)K))(K(SII)) H hg = g ( hhg ) ; Θ g = HH g ; Θ = U(B(SI)U) = SII(S(K(SI))(SII)) H gh = g ( hgh ) ; Y′ g = H g H ; Y′ = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K) H gyz = g ( yyz ) ; Θ 4 g = H g ( H g )( H g ) ; Θ 4 = B(WW)(BW(BBB)) H 何か = g ( h何か ) ; Y H g = H _____ H __ g （「_」の代わりに何でも入る）またはその他の中間的なH コンビネータの定義と、それに対応するY H [ 5 ] L abcdefghijklmnopqstuvwxyzr = r ( thisisafixedpointcombinator ) ; Y K LLLLLLLLLLLLLLLLLLLLLLLLLL 厳密なプログラミング言語 では、Y コンビネータは スタックオーバーフローが 発生 末尾呼び出し最適化 の場合は停止しません。[ 6 ] コンビネータは、適用評価順序が有効な 厳密な言語 (イーガー言語とも呼ばれる)で動作します。
Y コンビネータとの違いは、 Q x = B （ U x ） 私 = S （ K （ U x ） ） 私 = S （ B S （ B K U ） ） （ K 私 ） x {\displaystyle Qx=B(Ux)I=S(K(Ux))I=S(BS(BKU))(KI)x} η {\displaystyle \eta } Y の平易な表現の拡張形U x {\displaystyle Ux} Y = BU ( CBU )の場合、 Z = BU ( CBQ ) = S ( KU )( SB ( KQ ))となります。
Z = λ f 。 （ λ x 。 f （ λ v 。 x x v ） ） （ λ x 。 f （ λ v 。 x x v ） ） = λ f 。 U （ λ x 。 f （ λ v 。 U x v ） ） = S （ λ f 。 U ） （ λ f 。 λ x 。 f （ λ v 。 U x v ） ） = S （ K U ） （ λ f 。 S （ λ x 。 f ） （ λ x 。 λ v 。 U x v ） ） = S （ K U ） （ λ f 。 S （ K f ） （ λ x 。 λ v 。 U x v ） ） = S （ K U ） （ S （ λ f 。 S （ K f ） ） （ λ f 。 λ x 。 λ v 。 U x v ） ） = S （ K U ） （ S （ S （ λ f 。 S ） （ λ f 。 K f ） ） （ K （ λ x 。 λ v 。 U x v ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ λ x 。 λ v 。 U x v ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ λ x 。 S （ λ v 。 U x ） （ λ v 。 v ） ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ λ x 。 S （ K （ U x ） ） 私 ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ S （ λ x 。 S （ K （ U x ） ） ） （ λ x 。 私 ） ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ S （ λ x 。 S （ K （ U x ） ） ） （ K 私 ） ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ S （ S （ λ x 。 S ） （ λ x 。 K （ U x ） ） ） （ K 私 ） ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ S （ S （ K S ） （ S （ λ x 。 K ） （ λ x 。 U x ） ） ） （ K 私 ） ） ） ） = S （ K U ） （ S （ S （ K S ） K ） （ K （ S （ S （ K S ） （ S （ K K ） U ） ） （ K 私 ） ） ） ） {\displaystyle {\begin{aligned}\\Z&=\lambda f.(\lambda x.f(\lambda v.xxv))(\lambda x.f(\lambda v.xxv))\\&=\lambda f.U(\lambda x.f(\lambda v.Uxv))\\&=S(\lambda f.U)(\lambda f.\lambda x.f(\lambda v.Uxv))\\&=S(KU)(\lambda f.S(\lambda x.f)(\lambda x.\lambda v.Uxv))\\&=S(KU)(\lambda f.S(Kf)(\lambda x.\lambda v.Uxv))\\&=S(KU)(S(\lambda f.S(Kf))(\lambda f.\lambda x.\lambda v.Uxv))\\&=S(KU)(S(S(\lambda f.S)(\lambda f.Kf))(K(\lambda x.\lambda v.Uxv)))\\&=S(KU)(S(S(KS)K)(K(\lambda x.\lambda v.Uxv)))\\&=S(KU)(S(S(KS)K)(K(\lambda x.S({\color {Red}\lambda v.Ux})(\lambda v.v))))\\&=S(KU)(S(S(KS)K)(K(\lambda x.S(K(Ux))I)))\\&=S(KU)(S(S(KS)K)(K(S(\lambda x.S(K(Ux)))(\lambda x.I))))\\&=S(KU)(S(S(KS)K)(K(S(\lambda x.S(K(Ux)))(KI))))\\&=S(KU)(S(S(KS)K)(K(S(S(\lambda x.S)(\lambda x.K(Ux)))(KI))))\\&=S(KU)(S(S(KS)K)(K(S(S(KS)(S(\lambda x.K)(\lambda x.Ux)))(KI))))\\&=S(KU)(S(S(KS)K)(K(S(S(KS)(S(KK)U))(KI))))\\\end{aligned}}}
反転表現 S ( K ( SI )) K は 、それに続く 2 つの項を反転させます。
S ( K ( SI )) K αβ →K ( SI )α( K α)β →SI ( K α)β →I β( K αβ) →I βα →βα したがって、これはCI と同等です。一般に、任意のfに対して、 S ( K ( S f )) Kは C f と同等です。
ブール論理 SKIコンビネータ計算では、if-then-else 構造の形でブール論理 を実装することもできます。if -then-else 構造は、真（T ）または偽（F ）のいずれかである ブール式 と、次の2つの引数で構成されます。
T xy = x そして
F xy = y 重要なのは、2つのブール式を定義することです。1つ目は、基本的なコンビネータの1つと同じように機能します。
T = K K xy = x 2つ目もかなり単純です。
F = SK SK xy = K y ( xy ) = y 真と偽が定義されれば、すべてのブール論理は、if-then-else 構造として機能するブール値を用いて実装できる。
ブール値のNOT （指定されたブール値の反対を返す）は、if-then-else 構造と同様に機能し、F とT は2番目と3番目の値になります。
NOT b = b FT = S ( SI ( KF ))( KT ) b これをif-then-else 構造に入れると、期待通りの結果が得られます。
NOT ( T ) = ( T ) FT = F NOT ( F ) = ( F ) FT = T ブール論理OR （ 2つのブール引数値のいずれかがTの場合に T を返す）は、2番目の値としてTを持つ if-then-else 構造と同じように機能します。
または ab = a T b = SI ( KT ) ab これをif-then-else 構造に入れると、期待通りの結果が得られます。
または ( T )( T ) = ( T ) T ( T ) = T または ( T )( F ) = ( T ) T ( F ) = T または ( F )( T ) = ( F ) T ( T ) = T または ( F )( F ) = ( F ) T ( F ) = F ブールAND （引数のブール値が両方ともTの場合に T を返す）は、3番目の値としてFを持つ if-then-else 構造と同じように機能します。
かつ ab = ab F = S a ( KF ) b = SS ( K ( KF )) ab これをif-then-else 構造に入れると、期待通りの結果が得られます。
AND ( T )( T ) = ( T )( T ) F = T かつ ( T )( F ) = ( T )( F ) F = F かつ ( F )( T ) = ( F )( T ) F = F かつ ( F )( F ) = ( F )( F ) F = F これは、SKIシステムがブール論理を完全に表現できることを証明するものである。
SKI 計算は完全で あるため、例えば、他の論理コンビネータも表現できます。
XOR ab = OR ( AND a ( NOT b )) ( AND ( NOT a ) b )となることによって
XOR abxy = ( a ( b FT ) F ) T (( a FT ) b F ) xy = a ( byx )( bxy )同様に
NOT bxy = b FT xy = b ( F xy )( T xy ) = byx または abxy = a T bxy = a ( T xy )( bxy ) = ax(bxy) そして abxy = ab F xy = a ( bxy )( F xy ) = a(bxy)y
直観主義論理との関連性 コンビネータK とSは、 命題論理 の2つのよく知られた公理に対応する。
AK : A → ( B → A )AS : ( A → ( B → C )) → (( A → B ) → ( A → C ))関数適用は、 モーダス・ポネンスの 規則に対応します。
MP A とA → B からB を推論する。公理AK とAS 、および規則MPは、 直観主義論理 の含意断片に対して完全である。組み合わせ論理がモデルとして持つためには、
コンビネータの種類とそれに対応する論理公理との間のこの関係は、カリー・ハワード同型 の一例である。
参考文献 ↑ シェーンフィンケル、M. (1924)。 「バウスタイン・デア・数学論理」。数学アンナレン 。92 ( 3–4 ): 305–316 .土井 : 10.1007/BF01448013。S2CID 118507515。 ファン・ヘイエノールト、ジャン 編（2002）[1967] 「 数理論理学の構成要素について」 『 数理論理学資料集 1879–1931 』ハーバード大学出版局、 355–366 頁 。ISBN 9780674324497 。↑ カリー、ハスケル・ブルックス (1930)。「組合せ論理の基礎」 [ 組合せ論理の基礎 ] 。American Journal of Mathematics (ドイツ語)。52 ( 3)。ジョンズ・ホプキンス大学出版 局 : 509–536。doi : 10.2307 / 2370619。JSTOR 2370619 。 ↑ https://tromp.github.io/ ↑ Larry Wos、William McCune (1988 年 9 月)。 「自動定理証明を用いた固定点コンビネータの探索：予備報告」 (PDF) 。 アルゴンヌ国立研究所。2024 年 12 月 12 日 取得 。 ↑ 「Klop 2007による構成」 https://ncatlab.org/nlab/show/fixed-point+combinator ↑ ベネ、アダム（2017年8月17日）。 「JavaScriptにおける固定小数点コンビネータ」 。 ベネスタジオ 。Medium 。 2020年 8月2日 取得 。 スミュリアン、レイモンド （1985）。『モッキンバードを嘲笑う』 。ISBN 0-394-53491-3 。— (1994). 「第17章～第20章」『 対角線化と自己参照 』オックスフォード大学出版局。ISBN 9780198534501 OCLC 4735538 93 。
外部リンク オドネル、マイク「普遍的なシステムとしてのSKIコンビネータ計算」 キーナン、デイビッド・C. (2001)「マネシツグミを解剖する」 ラスマン、クリス、「コンビネーターバード」 「ドラッグ＆ドロップ式コンビネーター（Javaアプレット）」 『モバイルプロセスの計算、パートI （PostScript）』（ミルナー、パロウ、ウォーカー共著）の25～28ページでは、SKI計算のためのコンビネータグラフ縮小 のスキームが示されています。 Nockプログラミング言語は、従来のアセンブリ言語がチューリングマシンに基づいているのと同様に、SKコンビネータ計算に基づいたアセンブリ言語と見なすことができます。Nock命令2（「Nock演算子」）はSコンビネータであり、Nock命令1はKコンビネータです。Nockの他の基本命令（命令0、3、4、5、および擬似命令「implicit cons」）は、汎用計算には必須ではありませんが、二分木データ構造と算術演算を扱うための機能を提供することで、プログラミングをより便利にします。Nockには、これらの基本命令から構築できたであろう5つの命令（6、7、8、9、10）も用意されています。 
