翻訳:コンビネータ論理チュートリアル

このページは、Combinatory Logic Tutorialの翻訳です。

• http://homepages.nyu.edu/~cb125/Lambda/ski.html

基本的に超訳です。

訳の正しさは全く保証されません。 訳のおかしい部分は多数あります。

翻訳元サイトの許可を取ったりはしていません。 無認可です。

• 訳者による前書きと感想
• コンビネータ論理チュートリアル

訳者による前書きと感想

• 訳してみたものの、ちょっと、たったこれだけの説明では、はじめてコンビネータ論理を知った人が読んで充分に理解できるとは思えない。
  • どうも、この文書は、原文の上位ディレクトリにあるLambda tutorialを読んだ後に読むべきものっぽいようだ。
  • しかし、流石にこっちまで訳す気力は無い。
• そういう訳で、これだけを読むよりは、Unlambdaのチュートリアルを読んだ方がずっと、コンビネータ論理を理解できそうな気がする。
  • 本格的に理解したい人は、amazon:ものまね鳥をまねるが訳者としてはおすすめ。訳者もこの本で概要を理解した。
  • 教科書的なものに耐性のある人なら、amazon:計算論_計算可能性とラムダ計算も評判が良いようだ(が、訳者には耐性が無かったのでこの本は駄目だった)。

コンビネータ論理チュートリアル

λ簡約は、ややっこしい構文的変換です。 このλ簡約の完全で明確な記述は、全くもって困難で難解です。 そして、λ簡約の実行は、熟練した意味論者にとってすら地雷原に足を踏み入れるようなものです。 それ故に、λ算法の人気度は、もっと簡素化された代替品が無い事に足を引っ張られているように思えるかも知れません。

しかし、そうではないのです。 1920年代(脚注: λ算法よりも古い！)頃に、シェーンフィンケルによって考案され、ハスケル・カリーその他によって開発されたコンビネータ論理(Combinatory Logic)(CL)は、λ算法と等価な表現力を持ち、充分にシンプルです。 この言語(コンビネータ論理)は、括弧や変数(但し、変数名は「x」や「y」のような、一文字のものに限定されます)と共に、三つの特別なシンボル(「S」「K」「I」)を持ちます。 コンビネータ論理のあらゆる式は、他のあらゆる式と組み合わせる事ができます。

(((SK)K)(yS))

慣例により、(式同士の)結合は、左連想(左側から順に優先)で行われます。 このルールにより、前述の式は以下のように括弧を省略して記述できます。

SKK(yS)

(λ算法の)α簡約、β簡約、ν簡約の代わりになる、二つの重要な推論ルールを以下に示します。

KXY ==> X
SXYZ ==> XZ(YZ)

ここでの「X」「Y」「Z」は任意の式を示すメタ変数です。

「K」の意味は「(λ x (λ y x))」だと考える事もできますし、「S」の意味は「(λ x (λ y (λ z ((x z)(y z)))))」だと考える事もできます。 残った特殊シンボル「I」は、「(λ x x)」という意味だと考える事もできますが、「I」は「SKK」と定義する事もできます。 (訳注: 原文では「SKK」ではなく「SSK」になっているが、typoだと思われる。)

SKKX ==> KX(KX) ==> X

この式変換により、あらゆる式Xに対して「SKK」は恒等関数として機能します。

(訳注: ここに、JavaScriptで書かれた、前述の二つのルール(SとKの変換)を行うフォームがある。試す場合は原文を参照する事。)

以上。

λ算法のあらゆる式を変換する事ができます。 (訳注: 但し、Combinator BirdsのΩのような、変換が終了しない式を前述のフォームにかけない事。強制終了させるしかなくなる。)

たった一つの括弧とたった一つの演算子だけでも、論理が成り立つのです。 (訳注: 訳が怪しい。また、ここだけ読むと「SとKの二つが必要では？」と思われるが、Iotaの「SとKを産み出す一つのコンビネータ」を指しているものと思われる。)