SKIコンビネータ計算

SKIコンビネータ計算は、組み合わせ論理システムであり、計算システムです。ソフトウェアを書くのには不便ですが、コンピュータプログラミング言語と考えることができます。その代わりに、非常に単純なチューリング完全な言語であるため、アルゴリズムの数学的理論において重要です。型なしラムダ計算の縮小版にたとえることができます。モーゼス・シェーンフィンケル^[1]とハスケル・カリー^[2]によって導入されました。

ラムダ計算のすべての演算は、抽象化除去によって、葉が 3 つのシンボルS、K、I（コンビネータと呼ばれる）のいずれかであるバイナリ ツリーとして SKI 計算にエンコードできます。

このシステムでは、オブジェクトの最も正式な表現にはバイナリ ツリーが必要ですが、タイプセットを簡素化するために、ツリーの省略形として括弧で囲んだ式で表現されることがよくあります。サブツリーはどれでも括弧で囲むことができますが、多くの場合、右側のサブツリーのみが括弧で囲まれ、括弧で囲まれていないアプリケーションでは左結合性が暗黙的に使用されます。たとえば、ISK は(( IS ) K ) を意味します。この表記法を使用すると、左のサブツリーがツリーKSで、右のサブツリーがツリーSKであるツリーは、 KS ( SK )と記述できます。より明示的に表現する必要がある場合は、暗黙の括弧も含めることができます: (( KS )( SK ))。

非公式に、プログラミング言語の専門用語を使用すると、ツリー ( xy ) は、引数yに適用された関数xと考えることができます。評価されると (つまり、関数が引数に「適用」されると)、ツリーは「値を返します」 。つまり、別のツリーに変換されます。「関数」、「引数」、および「値」は、コンビネータまたはバイナリ ツリーのいずれかです。バイナリ ツリーの場合は、必要に応じて関数と考えることもできます。

評価操作は次のように定義されます。

（x、y、z は関数S、K、Iから作成された式を表し、値を設定します）。

I は引数を返します:

私はx = x

K を任意の引数xに適用すると、 1 つの引数を持つ定数関数K xが生成され、これを任意の引数yに適用すると、x が返されます。

Kxy = 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 は、任意のy に適用すると常に同じ結果を生成するため、任意のxに対して「機能的に同等」であると言えます。

これらの定義から、 SKI 計算はラムダ計算の計算を完全に実行できる最小限のシステムではないことが示されます。これは、任意の式におけるIのすべての出現を、任意のxに対して ( SKK ) または ( SKS ) または ( SK x )に置き換えることができ、結果の式は同じ結果を生成するためです。したがって、「I」は単なる構文上の糖衣です。I はオプションであるため、このシステムはSK 計算またはSK コンビネータ計算とも呼ばれます。

1 つの (不適切な) コンビネータのみを使用して完全なシステムを定義することは可能です。例として、Chris Barker のiotaコンビネータがあります。これは、 SとK を使って次のように表現できます。

ι x = x SK

イオタコンビネータからS、K、I を再構築することができます。 ι を自身に適用すると、 ιι = ι SK = SSKK = SK ( KK ) となり、機能的にはIと同等です。K は、 ι をIに 2 回適用することで構築できます(これは ι を自身に適用することと同等です)。 ι(ι(ιι)) = ι(ι SK ) = ι ( ISK ) = ι( SK ) = SKSK = K。 ι をもう一度適用すると、 ι(ι(ι(ιι))) = ι K = KSK = Sとなります。

基底を形成する最も単純な項は、X = λf.f λxyz.xz (yz) λxyz.xであり、XX = K、X (XX) = Sを満たします。

このシステムの用語と派生語は、より正式に定義することもできます。

用語: 用語の集合T は、次の規則によって再帰的に定義されます。

1. S、K、およびIは項です。
2. τ ₁と τ ₂が項である場合、(τ ₁ τ ₂ ) は項です。
3. 最初の 2 つのルールによって用語であることが要求されない限り、何も用語ではありません。

導出: 導出とは、次の規則によって再帰的に定義される項の有限シーケンスです (α と ι はアルファベット { S、K、I、 (、 )} 上の単語であり、β、γ、および δ は項です)。

1. Δ が α( I β)ιという形式の表現で終わる導出である場合、 Δ の後に αβι という用語が続くものは導出です。
2. Δ が α(( K β)γ)ιという形式の式で終わる導出である場合、Δ の後に αβι という項が続くものは導出です。
3. Δ が α((( S β)γ)δ)ιの形式で終わる導出である場合、Δ の後に項 α((βδ)(γδ))ι が続く導出です。

シーケンスが最初から有効な導出であると仮定すると、これらのルールを使用して拡張できます。長さ 1 のすべての導出は有効な導出です。

SII は、引数を受け取り、その引数を自身に適用する式です。

SII α = I α( I α) = αα

これはUコンビネータ、U x = xxとしても知られています。その興味深い特性の 1 つは、自己適用が不可能であることです。

SII ( SII ) = I ( SII )( I ( SII )) = SII ( I ( SII ) ) = SII ( SII )

あるいは、この式を定義として直接使用すると、すぐにU U = U Uが得られます。

もう 1 つは、あるものを別のものの自己適用に適用する関数を記述できることです。

( 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 gh = g ( hgh ) ; Y g = H g H

H hg = g ( hhg ) ; Y g = HH g

H何か= g ( h何か) ; Y g = H _____ H __ g

または、他の中間Hコンビネータの定義 (「_」の代わりに任意の文字が使用可能) と、それに対応するY定義を使用して、正しく開始します。

S ( K ( SI )) K は、それに続く 2 つの項を逆にします。

S ( K ( SI )) K αβ →

K ( SI )α( K α)β →

SI ( K α)β →

I β( K αβ) →

私はβα→

βα

したがって、これはCIと同等です。そして一般に、S ( K ( S f )) K は、任意のfに対してC fと同等です。

SKI コンビネータ計算では、if-then-else構造の形式でブール論理を実装することもできます。if -then-else構造は、真 ( T ) または偽 ( F )のブール式と 2 つの引数で構成されます。

Txy = x​

そして

Fxy = y である。

鍵となるのは、2 つのブール式を定義することです。最初の式は、基本的なコンビネータの 1 つのように機能します。

T = K

Kxy = x​

2番目もかなり簡単です:

F = SK

SK xy = K y(xy) = y

true と false が定義されると、すべてのブール論理はif-then-else構造で実装できます。

ブールNOT (指定されたブール値の反対を返す) は、FとT を2 番目と 3 番目の値として使用して、 if-then-else構造と同じように動作するため、後置演算として実装できます。

λb.b ( F )( T ) = λb.b ( SK )( K )ではない

これをif-then-else構造にすると、期待通りの結果が得られることが示される。

( T ) = Tではない( F )( T ) = F

( F ) はFではない( F )( T ) = T

ブールOR (それを囲む 2 つのブール値のいずれかがTである場合にTを返す) は、 Tを 2 番目の値とするif-then-else構造と同じように機能するため、インフィックス演算として実装できます。

または= T = K

これを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 (それを囲む 2 つのブール値が両方ともTの場合にTを返す) は、3 番目の値としてFを持つif-then-else構造と同じように機能するため、後置演算として実装できます。

そして= F = SK

これをif-then-else構造にすると、期待どおりの結果が得られることがわかります。

( T )( T )かつ= T ( T )( F ) = T

( T )( F )かつ= T ( F )( F ) = F

( F )( T )かつ= F ( T )( F ) = F

( F )( F )かつ= F ( F )( F ) = F

これは、T、F、NOT (後置演算子として)、OR (中置演算子として)、AND (後置演算子として) を SKI 表記法で定義するため、SKI システムがブール論理を完全に表現できることを証明しています。

SKI 計算は完全であるため、 NOT、OR、AND を前置演算子として表現することもできます。

NOT = S ( SI ( KF ))( KT ) ( S ( SI ( KF ))( KT ) x = SI ( KF ) x ( KT x ) = I x ( KF x ) T = x FT )

または= SI ( KT ) ( SI ( KT ) xy = I x ( KT x ) y = x T y )

そして= SS ( K ( KF )) ( SS ( K ( KF ))として) xy = S x ( K ( KF ) x ) y = xy ( KF y ) = xy F )

結合子KとS は、文論理の 2 つのよく知られた公理に対応します。

AK : A → ( B → A )、

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

関数の適用は、 modus ponens規則に対応します。

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

公理AKとAS、および規則MP は、直観主義論理の含意部分に対して完全です。組み合わせ論理がモデルとして持つためには、次の条件を満たす必要があります。

• 古典論理の含意的断片は、排中律、すなわちパースの法則に対する組み合わせ的類似物を必要とするであろう。
• 完全な古典論理では、文の公理F → Aの組み合わせ類似物が必要になります。

コンビネータの型と対応する論理公理との間のこの関係は、カリー・ハワード同型性の一例です。

還元には複数の方法があるかもしれません。演算の順序を崩さない限り、すべて同じです。

• ${\displaystyle {\textrm {SKI(KIS)}}}$
  • ${\displaystyle {\textrm {SKI(KIS)}}\Rightarrow {\textrm {K(KIS)(I(KIS))}}\Rightarrow {\textrm {KIS}}\Rightarrow {\textrm {I}}}$
  • ${\displaystyle {\textrm {SKI(KIS)}}\Rightarrow {\textrm {SKII}}\Rightarrow {\textrm {KI(II)}}\Rightarrow {\textrm {KII}}\Rightarrow {\textrm {I}}}$
• ${\displaystyle {\textrm {KS(I(SKSI))}}}$
  • ${\displaystyle {\textrm {KS(I(SKSI))}}\Rightarrow {\textrm {KS(I(KI(SI)))}}\Rightarrow {\textrm {KS(I(I))}}\Rightarrow {\textrm {KS(II)}}\Rightarrow {\textrm {KSI}}\Rightarrow {\textrm {S}}}$
  • ${\displaystyle {\textrm {KS(I(SKSI))}}\Rightarrow {\textrm {S}}}$
• ${\displaystyle {\textrm {SKIK}}\Rightarrow {\textrm {KK(IK)}}\Rightarrow {\textrm {KKK}}\Rightarrow {\textrm {K}}}$

• 組み合わせ論理
• B、C、K、Wシステム
• 固定小数点コンビネータ
• ラムダ計算
• 関数型プログラミング
• アンラムダプログラミング言語
• SKI よりもさらにシンプルになるように設計されたIotaおよび Jotプログラミング言語。
• マネシツグミをあざける

• オドネル、マイク「ユニバーサル システムとしての SKI コンビネータ計算」
• キーナン、デビッド C. (2001)「アラバマ物語」
• ラスマン、クリス、「コンビネーター バード」。
• 「ドラッグ アンド ドロップ コンビネータ (Java アプレット)」
• 「モバイル プロセスの計算、パート I (PostScript)」(Milner、Parrow、Walker 著) の25 ～ 28 ページで、SKI 計算のコンビネータグラフ削減のスキームを示しています。
• Nock プログラミング言語は、従来のアセンブリ言語がチューリング マシンに基づいているのと同じように、SK コンビネータ計算に基づくアセンブリ言語と見なすことができます。Nock 命令 2 (「Nock 演算子」) は S コンビネータであり、Nock 命令 1 は K コンビネータです。Nock のその他の基本命令 (命令 0、3、4、5、および疑似命令「暗黙の cons」) は、汎用計算には必要ありませんが、バイナリ ツリー データ構造と算術を処理する機能を提供することでプログラミングをより便利にします。Nock は、これらの基本命令から構築できる 5 つの命令 (6、7、8、9、10) も提供します。