コンビネータ論理

ウィキペディア

索引トップ用語の索引ランキングカテゴリー

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/10 14:50 UTC 版)

コンビネータ計算

ラムダ抽象が関数を作るための唯一の方法だから、コンビネータ計算では何かでそれを置き換える必要がある。コンビネータ計算は、ラムダ抽象の代わりに、原始的な関数の有限集合を提供し、それらから他の関数を構成することができるようにしている。

コンビネータ項

コンビネータ項は以下の形式のうち一つを持つ:

x
P
(E₁ E₂)

xは変数、Pは原始的関数、(E₁ E₂) は項の適用である。原始的関数はコンビネータ、つまり、ラムダ項として見たときには自由変数を持たない関数である。

表記を短縮するために、伝統的に(E₁ E₂ E₃ ... E_n)ないしE₁ E₂ E₃ ... E_nは(...((E₁ E₂) E₃)...E_n)を示す。

コンビネータ論理での簡約

コンビネータ論理では、それぞれの原始的コンビネータは以下のような形の簡約のルールを持つ。

(P x₁ ... x_n) = E

Eは変数x₁ ...x_nのみに言及している項である。これらのルールは、原始的コンビネータが関数として振る舞う方法を定義している。

コンビネータの例

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

(I x) = x

もうひとつの単純なコンビネータはKで、定数関数を作る。(K x)はどんな引数に対してもxを返す関数である。そして、Kはこのように定義する:

((K x) y) = x

もしくは、伝統的な複数の適用の表記に従えば

(K x y) = x

三つ目のコンビネータは、適用を一般化したSである。

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

Sは、それぞれにzを適用したあとxをyに適用する。別の言い方をすれば、zという環境においてxをyに適用する。 SとKがあれば、Iは不必要である。なぜなら、他の二つでこのようにして表現できるからである。

((S K K) x)

= (S K K x)

= (K x (K x))

= x

すべての項xに対して((S K K) x) = (I x)が成り立つが、(S K K)自身はIとは同じではない。これらの項は外延的に同値である。外延的同値は関数の同値という数学的な概念である。二つの関数が、同じ引数に対して常に同じ結果を返すならばそれは等しい。対照的に、原始的なコンビネータと一緒にあるそれらの項自身は、内包的同値という概念を捉える。十分な引数が与えられたときに、原始的なコンビネータに展開されるまで同じ形をもつ時だけ、それらは同値である。

恒等関数を実装するにはたくさんの方法がある。(S K K)とIはそれに含まれている。さらに、(S K S)もそうである。今後、同値という言葉を外延的同値を示し、等しいを同じコンビネータを示すのに使う。

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

S-K basisの完全性

SとKが外延的にすべてのラムダ項と同値なものに合成されうるのは、おそらく驚くべき事実である。したがって、チャーチのテーゼによれば、それはあらゆる計算可能な関数に合成されうる。その証明は、T[ ]という任意のラムダ項を同値なコンビネータにする変換を示すことで与えられる。 T[ ]は以下のように定義する。

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[λx.T[λy.E]] (if x occurs free in E)
T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

これはabstraction eliminationとして知られている。

ラムダ抽象から同値なcombinatorial termへの変換

たとえば、λx.λy.(y x)をコンビネータにしてみよう。

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

= T[λx.T[λy.(y x)]] (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)

任意の二つの項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)

(S (K (S I)) (S (K K) I))という表現は、ラムダ項としての表現λx.λy.(y x)よりもはるかに長い。これは一般的なことである。普通、T[ ]はラムダ項をΘ(n²)に展開する。

T[ ] 変換について

Tは抽象を消去することが動機となっている。規則3、4は自明である:λx.xは明らかにIと等しく、λx.Eはxが自由変数としてEに出現しない時明らかに(KT[E])である。最初の二つの規則も単純である。変数はそれ自身に変換され、コンビネータ項において許されている適用は単にアプリカンドとコンビネータへの引数の変換である。 5番目と6番目の規則は興味深い。5番目は複雑な抽象をコンビネータに変換することを単純に示している。まず本体をコンビネータに変換し、それから抽象を除去する。6番目は実際に抽象を除去する。 λ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)

外延的同値性によって、

       λx.(E₁ E2)     = (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[ ]変換によって生成されたコンビネータはη-reductionによって小さくなりうる。

       T[λx.(E x)] = T[E]   (if x is not free in E)

λx.(E x)はxを引数にとり、Eを適用する関数である。それは外延的にはE自身と同値である。それはつまりEをコンビネータの形にすれば十分である。この例は、この簡略化を根拠付ける。

         T[λx.λy.(y x)]
       = ...
       = (S (K (S I))   T[λx.(K x)])
       = (S (K (S I))   K)                 (by η-reduction)

このコンビネータはより早く、長いものと同値である。

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

同様に、もとのT[ ]はλf.λx.(f x)を(S (S (K S) (S (K K) I)) (K I))に変換したが、η-簡約を用いればλf.λx.(f x)はIに変換される。

One-point basis

すべてのコンビネータがすべてのラムダ項と外延的に等しくなるようなone-point basesが存在する。そのような基底のもっとも単純な例Xはこうである。

       X ≡ λx.((xS)K)

それを確かめるのは難しくない。

       X (X (X X)) =^ηβ K and
       X (X (X (X X))) =^ηβ S.

{K, S}が基底だから、{X}もまた基底である。プログラミング言語IotaはXをその唯一のコンビネータとして使う。 one-point basisのもう一つの簡単な例は

       X' ≡ λx.(x K S K) with
       (X' X') X' =^β K and
       X' (X' X') =^β S

X' はKとSを生成するのにη変換を必要としない。

B,Cコンビネータ

SとKに加え、モイセイ・シェインフィンケリ（ロシア語版、英語版）の論文ではBとCと呼ばれる、以下のような簡約をするコンビネータを含めた。

       (C f x y) = (f y x)
       (B f g x) = (f (g x))

彼は、どのようにしてSとKだけを用いてこれらを表現できるかを説明した。これらのコンビネータは述語論理やラムダ計算をコンビネータ式にする際に非常に有用である。これらはハスケル・カリーと、だいぶ後に計算機における用法と関連付けたデビッド・ターナーによって使われた。これらを使って、以下のように変換のルールを拡張できる。

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[λx.T[λy.E]] (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₁)

BとCコンビネータを使うと、λx.λy.(y x)の変換はこのようになる。

         T[λx.λy.(y x)]
       = T[λx.T[λy.(y x)]]
       = T[λx.(C T[λy.y] x)]     (by rule 7)
       = T[λx.(C I x)]
       = (C I)                   (η-reduction)
       = C_*(traditional canonical notation : X_* = X I)
       = I'(traditional canonical notation: X' = C X)

確かに、(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を用いなくても、この論文^[2]の節3.2のように達成できる。

CL_KとCL_I算法

この記事で述べているCL_K算法とCL_I算法は区別されなければならない。これらの区別は、λ_Kとλ_I算法に対応する。λ_K算法と違い、λ_I算法は抽象を以下のように制限する。

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

λx.Eにおいて、xはEの中で少なくとも一つは自由に出現している。

結果として、Kはλ_IにもCL_Iにも与えられない。CL_Iの定数は、I, B, C,Sであり、CL_Iのすべての項が合成される。λ_KからCL_Kへの変換と似たようなルールに合わせ、すべてのλ_Iの項は、等しい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[ ]の逆変換ではないことに注意。

脚注

^ Seldin, Jonathan. The Logic of Curry and Church.
^ 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. (pdf version)