SKIコンビネータ AGAIN

by Akihiko Koga
27th Feb 2019 (Update)
11th Feb 2019 (First)

計算機(主にソフトウェア)の話題 へ
ホームページトップへ戻る

目次

  1. 趣旨
  2. 概略
  3. ちょっと動かしてみる
  4. Simple SKI Interpreter の機能の説明
  5. コンビネータ論理の基礎
  6. プログラムリスト
  7. プログラムの変更履歴
  8. 補足事項
  9. 参考文献

趣旨

SKI コンビネータのことは,以前,ある程度,

コンビネータ論理(Combinatory Logic) のお話
- λ式から SKI を使った式への変換のトレース -

で話したのですが,そこでは動くものを提供しませんでした.先ほど,せっかく,

簡単な演算子順位法によるパーサー in Ruby

でパーサを作ったので,これを利用して,本当に簡単なコンビネータのインタープリタを 作って遊ぶのも面白いかなと思います.

概略

ここで作って遊ぶのは,コンビネータの式を入力すると,その式のリダクションを行って結果を 表示するインタープリタです.コンビネータとしては最初から3種類,

  1. S ?X ?Y ?Z => (?X ?Z) (?Y ?Z)
  2. K ?X ?Y => ?X
  3. I ?X => ?X
というコンビネータが組み込まれています.ここで ?X, ?Y, ?Z など ? で始まる名前は どんな式にもマッチするもので,上の式はマッチした式を => の右側の並びに変えるという 意味を持っています.一応,式の読み方としては左から括弧が付きます.つまり, X Y Z U V という並びがあれば,(((X Y) Z) U) V という意味です.本などに載っている コンビネータは1文字で途中に空白を挟まずに書けますが,ここでは文字の間は1文字以上の 空白で区切ってください.その代わりに一文字より長い名前のコンビネータが使えます. 途中に括弧が挟まり,アルファベットが続かないところは空白を 入れる必要はありません.

コンビネータの理論では,この3つのコンビネータだけで,帰納的な関数を記述できると いうことが示されます.ここでは実際に動かしてその雰囲気を味わいましょう.

ちょっと動かしてみる

まずはちょっとだけ動かしてみましょう.

対話的に実行できる Ruby のインタープリタを入手します.Ruby のバージョンは 2.3 以降なら動くと思います(今(2019年2月11日現在)は,Version 2.6 位ですかね)

次に,「簡単な演算子順位法によるパーサー in Ruby」の パーサーの掲載リスト から,その掲載リストをコピーして,ファイルに保存し,Ruby に読み込みます.

最後に,このページの SKI コンビネータインタープリタの掲載リスト をやはり,コピーしてファイルに保存し,先ほどパーサーを読み込ませた Ruby に 続いて読み込ませます.

以上で準備は整いましたので,Ruby のインタープリタで top という関数を動かしてください. 以下,ちょっと動かしてみたログを示します.日本語で書いている部分は,何をやっているかの 説明ですから,ちょっと追いかけてみてください.

まずRubyのインタープリタを起動します.
c:\0-ruby\sop>irb

次に,パーサーとこのページに掲載したSKIのインタープリタを読み込みます.
私はパーサーはファイル sop.rb ,SKI インタープリタは ski000.rb という
名前のファイルに格納しています.
irb(main):001:0> load "sop.rb"
=> true
irb(main):002:0> load "ski000.rb"
=> true

関数 top を呼び出すと,簡単なコマンドの説明が出て,実行が始まります.
irb(main):003:0> top
Welcome to Simple SKI Interpreter
commands are
    :q to quit
    :s to show definition identifiers and rules
    :o to toggle one step mode
    :di, :dr to delete an identifier or a rule
    :lim NNN to set limit number of translation
    Identifier := Exp to define an identifier
    Head => Body to define a rule
    Other input is evaluated as an combinator exp

「:」で始まるいくつかのコマンド以外は,とにかく打ち込めば,
それがコンビネータの式だと思って実行が始まります.
まずは,上で簡単に説明した S, K, I の働きを確認してみましょう.
x, y, z もなにかコンビネータだと思ってください.でも定義が与えられて
いないので,それらはこのまま変化しません.コンビネータの式はこのように
名前が空白や括弧で区切られて並べられたものです.ただし,括弧はきちんと
対応が付くようにしておいてください.
ski> S x y z
Evaluation of S x y z
  0: -> x z (y z)
Value = x z (y z)
ski> K x y
Evaluation of K x y
  0: -> x
Value = x
ski> I x
Evaluation of I x
  0: -> x
Value = x
はい,以上でとりあえず,S, K, I の働きの確認は終わりました.

次の式ではK は x y までにしか作用しないので z は残ります.
ski> K x y z
Evaluation of K x y z
  0: -> x z
Value = x z

K は二つの並びを後ろにとってその最初のものを返すコンビネータでした.
ski> K x y
Evaluation of K x y
  0: -> x
Value = x

では,二つのうちの後ろを返すコンビネータの式は書けるでしょうか?
実は,K I がそうです.やってみましょう.
ski> K I x y
Evaluation of K I x y
  0: -> I y
  1: -> y
Value = y
うまくいきました.

では,K I というコンビネータの式に名前を付けておきましょう.
それには次のようにします.ここではこれにfalseという名前を付けます.
ski> false := K I
identifier false is defined. Use :s for check
はい,名前(identifier)が定義できました.

:s というコマンドは現在の名前とコンビネータの定義を表示します.
上がコンビネータの定義で,現在は,S, K, I というコンビネータが定義されています.
下が名前で,先ほど := で定義した false が表示されています.
ski> :s
 Definition of combinator(s)
    S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
    K ?X ?Y => ?X
    I ?X => ?X
 Definition of identifier(s)
    false := K I
 End

名前を定義すると,それを式の中で使うことができるようになります.
これは単に,入力の中の名前がその定義で置き換えられるだけです.
そうして名前が置き換えられたコンビネータの式はコンビネータの規則が提供できる限り,
規則に従ってどんどん書き換えられていき,その過程が表示されます.
いま定義した false を使ってみましょう.
ski> false x y
Evaluation of K I x y
  0: -> I y
  1: -> y
Value = y
はい,先ほどの K I と同じ効果が得られています.

次はほんのちょっとだけ長いコンビネータ式を入力してみましょう.
(S I I) が二つです.前の S I I には括弧はついていませんが,ついていなければ,
左から括弧がくくられているというルールを思い出してください.
ski> S I I (S I I)
Evaluation of S I I (S I I)
  0: -> I (S I I) (I (S I I))
  1: -> S I I (S I I)
  2: -> I (S I I) (I (S I I))
  3: -> S I I (S I I)
  4: -> I (S I I) (I (S I I))
  5: -> S I I (S I I)
  6: -> I (S I I) (I (S I I))
  7: -> S I I (S I I)

    途中略

 34: -> I (S I I) (I (S I I))
 35: -> S I I (S I I)
 36: -> I (S I I) (I (S I I))
 37: -> S I I (S I I)
 38: -> I (S I I) (I (S I I))
 39: -> S I I (S I I)
Value = S I I (S I I)
なにやら,二つの式が交互に現れる列ができました.実はこれは
無限ループになります.このシステムではデフォルトでは40回で計算を打ち切っているので
0から39までで終わっています.この回数はコマンドで設定することができます.
しかし,コンビネータの式はうかつなものを入れると巨大になりながら無限ループすると
いうのが結構ありますから,変換回数の制限は付けておいたほうが良いです.
今回のものは大きさが変わらずに無限ループだったので,この回数制限で救われましたが
ものによっては数倍に大きくなりながら無限ループするものがあり,その場合は
計算リソースを食い尽くしてしまいますから Ctrl-C などで止めてください.

それにしても,あれだけ単純な S, K, I のコンビネータの組み合わせで,止まらない
ループができること自体が不思議です.計算の神秘ですね.


ski> S I I x
Evaluation of S I I x
  0: -> I x (I x)
  1: -> x x
Value = x x
S I I は実は引数を2倍にするコンビネータの式だったのです.
ですから,(S I I) (S I I) は後ろの (S I I) が2倍になり,前の (S I I) が
消えるので,結局,(S I I) (S I I) のまま変わらないというわけです.

これにも名前をつけておきましょう.
ski> xxx:= S I I
identifier xxx is defined. Use :s for check
ski> xxx S
Evaluation of S I I S
  0: -> I S (I S)
  1: -> S S
Value = S S
ski> :s
 Definition of combinator(s)
    S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
    K ?X ?Y => ?X
    I ?X => ?X
 Definition of identifier(s)
    false := K I
    xxx := S I I
 End
はい,false と xxx の二つの名前ができましたね.

名前は再度定義すると書き換えられます
ski> xxx:=I
identifier xxx is defined. Use :s for check
ski> :s
 Definition of combinator(s)
    S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
    K ?X ?Y => ?X
    I ?X => ?X
 Definition of identifier(s)
    false := K I
    xxx := I
 End

あと,名前を消したり,新しいコンビネータを定義したりと
いった機能がありますが,それは後で追々説明していきます.とりあえず,
S, K, I だけでも再帰的関数の定義ができる能力がありますので,コンビネータの
ことをいろいろ調べれば,ここまで説明した機能でも十分遊べると思います.

終了するには :q を入力します.
ski> :q
=> nil
irb(main):004:0>

とりあえず,簡易インタープリタの動かし方をざっと説明しました. 最後にも書きましたようにこれだけで,実は,結構遊べますので,適当に いじってみてください.

とりあえず,次の機能を持つコンビネータの式を考えてみるというのはどうでしょう.

  1. 式 x -> x x x
    S I I は x を x x に変えました.これをなんとか2回利用できれば できそうな気はします.それには S を使います.以上,ヒントでした.

  2. 式 x y -> y x

  3. 式 x y z u -> (x u) (y u) (z u)

  4. 式 x y z -> x (y z)

上で左端に書いてある「式」というのは,S, K, I と括弧を使った並びのことです. 例えば,式が S I I なら, x を x x にするなどです.思いついたものが正解かどうかは 実行してみれば分かります.正解は1つとは限りません.どれか1つでも見つかれば結構です, 虫食い算みたいで結構な暇つぶしになると思います.

上の問題の中で最後の式は,先ほどの引数を倍にするコンビネータの式 S I I と組み合わされて, コンビネータの式が帰納的関数の能力を持つことに関連してとても重要です.

そのうち,続きを書くと思います.2019.02.11 (月)

Simple SKI Interpreter の機能の説明

一応,一通り,Simple SKI Interpreter の機能の説明をしておきます.

利用のための環境ですが,Ruby の バージョン 2.3 以降と,対話型インタープリタが あれば利用可能と思います.私は Windows で, irb を使っていますが, Linux でも irb は動いているみたいなので本インタープリタを利用可能でしょう. Mac についてはあまり良く知りませんが,irb はあるようですね.android の ruboto などの 環境では,それぞれの ruby の関数は実行可能なのですが,read-eval loop が書けないので 本ページのプログラムをそのまま利用することはできません.

続いて,起動と終了ですが,Ruby の対話型インタープリタ(irb など)に,

簡単な演算子順位法によるパーサー in Ruby

を読み込んだ後,以下に掲載した SKI コンビネータインタープリタの掲載リスト を読み込んで,関数 top を呼び出してください.そうすれば,Simple SKI Interpreter に 入ります.終了するためにはコマンド :q を入れて改行を入れてください.Ruby の インタープリタに戻ります.

Simple SKI Interpreter のコマンドは次の4種類に分かれます.

  1. ":" から始まる名称のコマンド
    これには以下のコマンドがあります.
    1. :q ... Simple SKI Interpreter を終了させます.

    2. :s ... 現在定義されているコンビネータと名前を表示します.

    3. :o ... ワンステップモードの ON/OFF を切り替えます.
      本インタープリタは コンビネータの式が入力されると,まず,定義されている名前を 対応するコンビネータの式で置き換え,あとは,コンビネータの 定義に従って式を変換しては表示し,変換しても直前と同じなら 変換をやめるという動作をしています.ワンステップモードが ON の場合は,一つのコンビネータの適用を終えるごとに表示し, ワンステップモードが OFF のときは,全種類のコンビネータの 適用が終わった後に表示します.したがって,ワンステップモードが OFF の方が一般に表示回数は少なくてすみますが,その途中経過が 省略されているので分かりにくい欠点もあります.最初は ワンステップモードは ON になっています.

      どのコンビネータの適用を最初に行うか,式のどの部分に適用するか など,コンビネータの適用戦略についてはいろいろ議論があるところですが, これについては,プログラムで見つかった順ということで,プログラムを 見たり,改造したりしてみてください.

    4. :di ... 名前の削除
      下に説明する ":=" で定義した名前の定義を削除します.

      :di 名前

      という形で使います.

    5. :dr ... コンビネータの削除
      下に説明する => で定義したコンビネータの定義を削除します.

      :dr コンビネータ名

      という形で使います.左辺がコンビネータ名のルールが消されます.

    6. :ci ... すべての名前の削除

    7. :cr ... すべてのコンビネータの削除

    8. :clear ... すべての名前とコンビネータの削除

    9. :reset ... 名前とコンビネータの定義を最初の状態に戻します.

    10. :p ... コンビネータの式の木表示

      次の形で指定されたコンビネータの式を木の形で表示します.

      :p コンビネータ式

      関数適用は ".." で表示されます.

      例:

      ski> :p (S x y z => (x z) (y z))
          (=> (.. (.. (.. S
                          x)
                      y)
                  z)
              (.. (.. x
                      z)
                  (.. y
                      z)))
      

      コンビネータの式が実際にはどのような構造をしているかを調べるために 便利です.入力の中には関数適用だけでなく,"=>" も使うことができます.

    11. :lim ... 変換回数制限の変更

      本ツールは無限ループ回避のために,変換回数を制限しています. その制限回数を変更します.

      :lim 制限回数

      という形で使ってください.制限回数の初期値は 40 です.

    12. :load ... ファイルからのコマンドの読み込み

      端末からコマンドを読み込んで実行する代わりに,ファイルからコマンドを 読み込んで実行します.ファイルの中に xxx := 式 などの列を書いておくと いちいち端末から入力しないで便利です.このコマンドは,

      :load ファイル名

      という形で使います.ファイル名はダブルクォートで囲んでください.

  2. 名前(identifier)を定義する ":=" を含んだ式
    本ツールでは,

    名前 := コンビネータの式

    のような式を入植すると,指定されたコンビネータ式を名前で参照することが できるようになります.名前はアルファベットと数字,アンダーバーの 組み合わせの綴りにしてください.ここで定義した名前はコンビネータ式の入力の ときに使うことができるようになります.

  3. コンビネータの定義を行う "=>" を含んだ式
    本ツールでは最初から,S, K, I のコンビネータは定義されていますが, 他のコンビネータを定義したいことがあります.それにはこの=> を 含んだ式を使ってください.例えば,

    M ?X => ?X ?X

    とすると,与えられた引数を二つ並べるコンビネータが定義できます. これは S, K, I を使って表すと,S I I に相当するものですね. コンビネータを定義するとき,引数は ? で始まる名前にして全部異なるように してください.つまり,

    Comb ?X ?X => S S K ?X

    などとしないでください.特にチェックはしていませんので間違えた場合は 上で説明したコマンド :dr で消してから入れなおしてください.

  4. その他
    コンビネータの式が入力されたと扱い,コンビネータの定義を適用して形が 変化する限り,変換を続け,その過程を表示します.ただし,無限ループを 回避するために,上で述べた制限回数に達したら停止して結果を表示します. 適用ごとに大きさが倍々に増えるコンビネータの式などはすぐ計算リソースが 枯渇してしまいますので,そういう時は Ctrl-C などで強制的に停止してください.

コンビネータ論理の基礎

目次

  1. コンビネータの定義
  2. コンビネータ S, K, I
  3. コンビネータによる論理値,論理演算の表現
  4. コンビネータによる自然数の表現
    1. バーレントレクトらの自然数の表現方法ダッシュ
    2. チャーチ流の自然数の表現方法に関して
  5. コンビネータによる再帰の実現方法

ここではコンビネータ論理の,ほんの基礎部分だけを書いておきます.本格的に説明するのは 私の能力では無理だからです.ご興味のある方は, 参考文献に挙げたコンビネータ論理の成書を当たってみてください.

  1. コンビネータの定義
    ここらあたりは数学的に厳密に定義していない書き物が多いです.実は私は 定年前に会社を辞めて,いま,ほぼ無職なので,お金がなくて,成書を買うことが できません.それで正確な定義を調べることができません.

    そこで,去年(2018年),某勉強会に行ったとき,某 KWB 大先生に教えて もらったことをベースに自分流に書いてみます.お金のある人は,ぜひ, 参考文献にある本を買って正確な定義を 調べてみてください.

    定義

    集合 C の二つの元 x, y に集合 C の元 (xy) が 対応させられているとき,集合 C適用系といい, 集合 C の元をコンビネータ という. ただし,C は二個以上の元を持つものとする.

    この定義内の (xy) で x と y の間には二項演算子が省略されているとみることが できますから,この定義は,C には二項演算が定義されていて,Cの要素を コンビネータというと言っているにすぎません.今日的にはこのように二項演算の 定義された集合はマグマ(magma)といいます.昔は,これを groupoid亜群 と言ったりしていましたが, 今は,マグマ(magma)ですね.ちなみに,マグマで結合法則が成り立つものを 半群(semigroup),さらに単位元 (unit) のあるものを モノイド(monoid),逆元(inverse)もあるものを群(group) と言いますね.

    このような用語を使うと,適用系とはマグマで,その元をコンビネータというという ことですね.

    マグマで一番単純なマグマは自由マグマ(free magma)と呼ばれるものです. これは,A を何か集合とするとき,この集合の要素を葉とする二進木の集合です. FreeMagma(A) で,A から生成される自由マグマを表すことにすると, これは以下のように定義されます.ただし,「・」はここで定義される演算とします.

    1. A ⊆ FreeMagma(A)
    2. x, y ∈ FreeMagma(A) ならば x・y ∈ FreeMagma(A)
    3. FreeMagma(A) の元は上の二つの規則で生成されたものだけである

    計算機屋さんになじみの深いものとしては,LISP の S-式の集合は,アトムから 二項演算 cons(-, -) で生成される自由マグマですね.

    多くの流儀では,この自由マグマをベースにコンビネータが定義されています. Wikipedia の記述もこの自由マグマに要素間に

    f ?x1 ... ?xn => ?x1, ..., ?xn と A の元を使った自由マグマの式

    (f ?x1 ... ?xn は二項演算を意識して書くと (...(f・?x1)・...・?xn)

    ?x1, ?xn は FreeMagma(A) の任意の元

    という変換ルールの集合があるとして話を進めているようです.

    これを前者の流儀と合わせると,

    両者を融合する定義

    A を集合とし,FreeMagma(A) の上の変換ルールの集合を R とする.
    Eq(R) でこの反射的対称的推移的閉包(reflexive symmetric transitive closure),つまり,R の方向を無視して,これを 0 回以上適用して行ける 要素は等しいと見る関係を表す.このとき,商空間 FreeMagma(A)/Eq(R) を 適用系といい,この要素をコンビネータと言う

    とすることにより,二つの流儀で共有するコンビネータの定義を与えることが できるように思います.

    この定義だと,任意のコンビネータの式をコンビネータということができるのですが, とりあえず,以下では,S, K, I など変換ルールが陽に与えられたものが,いかにも コンビネータっぽいので,A の要素をコンビネータとよび,それ以外の演算を含んだ式は コンビネータの式と呼ぶことにします.ここらあたりは,このページにローカルな 呼び方なのですが,ご容赦ください.

    補足:λ計算の読み物などを読むと,「コンビネータとは,閉じた(即ち, 自由変数を持たない)λ式である」という定義もあります.

  2. コンビネータ S, K, I
    これらについては,コンビネータ論理(Combinatory Logic) のお話 で,変な絵付きで詳しく話したのですが,こちらでも 簡単に説明しておきます.

    まず,それぞれのルールですが,以下の通りです.

    1. S ?X ?Y ?Z => (?X ?Z) (?Y ?Z)
    2. K ?X ?Y => ?X
    3. I ?X => ?X

    I は,S と K で作ることができますし,単純なので説明を省略します.

    K は,役割的に考えると,二つの捉え方ができます.一つは真偽値の true という捉え方で,もう一つは定数関数を作る作用素としての捉え方です.

    1. 真偽値の true を表す
      二つの引数のうち,最初のものを返す作用素ですから

      if true then ?X else ?Y end

      のような役割をしていると考えることができます.もし,後ろを返すコンビネータの 式 false があれば,式 E1 E2 E3 で,E1 が true か false に必ず 変換できるなら,この式は E1 が true のときは E2, false のときは E3 を返す関数を表すことになります.一応,後ろを返すコンビネータの式と しては,K I があります.

      K I x y -> I y -> y

      確かに,後ろの引数 y になりました.ちなみに,-> は「変換される」 を表すことにします.

    2. 定数関数を作る作用素を表す
      (K Exp) は後ろに何が来ても Exp を返します.したがって,(K Exp) は 定数関数 Exp を表すと考えることができます(ラムダ式で書くと λx.Exp ですね). これは上の false を作るときに使えます.false x y -> y ですから, false x が I になればよい訳です.そのためには,false はどんな 引数が来ても I を返す式であればよい訳ですが,それは K に I を 抱きかかえさせて,I を返す定数関数にしてしまえばよい訳です. ということで,false = K I という式が求まる訳です.

    S は引数 ?Z を ?X と ?Y に分配する機能を持っています.変数の文字を変えて

    S ?f ?g ?x => (?f ?x) (?g ?x)

    と書けば雰囲気がでるでしょうか.

    プログラミング言語やλ計算では,関数はパラメータを持つことができ,実際の 関数呼び出しでそのパラメータにもらった引数の値は,パラメータの名前で 関数の処理の色々な場所に分配され,使われます.このとき,パラメータの名前が 問題になることがしばしばあります.皆さんは,静的なバインディングと動的な バインディングがしばしば,プログラミングのミスを誘発することをご存知でしょう. 古くは LISP で Funarg 問題と呼ばれる問題が発生することもありました. コンビネータ論理ではパラメータがありませんので,この問題が起こりません. その代わり,S のようなコンビネータで,引数をプログラム(あるいはコンビネータの 式)のあちこちに届けてやる必要があります.S はこのメカニズムを提供します.

    後の説明にも使いますので,次のλ記法を覚えておいてください.これは, λ計算のごくごく簡単な部分だけです.

    λx.E はなにか x をとって,それを E の中の x に 代入したもの E' を返す関数を表す.

    例として,(λx.(K x)) (S I) は K (S I)) になります.

    いま,λx.(E1 E2) という式を別の式 E に適用することを考えます. λ計算の計算メカニズムがかれば,E1 と E2 の中の x が表れるところに E を代入するということができますが,コンビネータ論理にはこのような パラメータのメカニズムはありません.その代わりに,コンビネータ S で E1 と E2 に E を届け,(E1 E) (E2 E) という式を作り,E1, E2 にそれぞれ, E を取り込んで使ってもらうようにすることで,パラメータのメカニズムを 実現しようというものです.

    (S I I) は貰った引数を二つにするコンビネータの式でした.これは,S が x を それ自身を返すコンビネータ I 二つに x を分配している訳です.二つに分配できるなら それをもう一つ使えば3つに分配することも可能です.つまり,(S F I) x が (F x) x ですから F を x を二つに増やすコンビネータ式にしてしまえばよい訳です, これは前の節で出した問題のうちの1つのヒントです.

  3. コンビネータ M と B
    コンビネータ,特に,S, K, I だけでも,コンビネータの式には, チューリングマシンと同等の計算能力があります.それを示すのに重要なのが次の 二つの機能を持ったコンビネータです.これらは S, K, I で作ることができますが, また,名前も持っています.

    1. M ?x => ?x ?x
      これはすでに何度も出てきた S I I で実現ができます.

    2. B ?x ?y ?z => ?x (?y ?z)

    なぜ重要かと言いますと,この二つを使うことにより不動点演算子 を作ることができるからです.コンビネータの式 E がコンビネータの式 F の 不動点とは

    E -> F E

    となることを言います.不動点演算子 Fix とは Fix F が F の不動点と なるようなコンビネータのことです.つまり,

    (Fix F) -> F (Fix F)

    となります.このような Fix を M と B を組み合わせて作ることができます. どうやったら良いでしょう.これはとりあえず,問題にしておきます.

    なお,Fix F を Simple SKI Interpreter に入れると止まりません. でも,回数制限がありますから,いくつか試してみると良いでしょう.

    (そのうち答えを書くかもしれません)

  4. コンビネータによる論理値,論理演算の表現
    true = K, false = K I はすでにお話しました.これらの下に, 論理演算 not, or, and, imply などを作って遊びましょう.

    これらの演算は true, false のどちらかを必ず引数に取るとして 設計して結構です.

    お手本に not をやってみます.not はλ記法を使って書けば

    not = λx.(x false true)

    のように,真偽値を受け取って,それを if 文の条件部分相当のところに 持って行って,then-部分に false, else-部分に true を置けばできます. これを S を使って実現することを考えると,

    not = S λx.(x false) λx.true

    の中のλ式がコンビネータの式に置き換えられれば良い訳です. λx.true は定数関数ですから,(K true) で実現できます. λx.(x false) は,やはり S を使って引数 x を分配し,前は x そのものを, 後ろは定数 true を返しますから,

    (S I (K false))

    で実現できます.まとめると,

    S (S I (K false)) (K true)

    となります.実際にインタープリタで確かめてみましょう.

    not を今求めたコンビネータの式として定義します.
    
    not を定義する前には true (K) と false (K I) を定義するようにしてください.
    ski> false := K I
      Identifier false is defined.
    ski> true := K
      Identifier true is defined.
    ski> not := S (S I (K false)) (K true)
      Identifier true is defined.
    
    正しく定義されたかどうか見てみましょう
    ski> :s
     Definition of combinator(s)
        S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
        K ?X ?Y => ?X
        I ?X => ?X
     Definition of identifier(s)
        false := K I
        true := K
        not := S (S I (K (K I))) (K K)
     End
    true, false は展開されていますが,正しく定義されています.
    
    not true を実行してみます.
    ski> not true
    Evaluation of S (S I (K (K I))) (K K) K
      0: -> S I (K (K I)) K (K K K)
      1: -> I K (K (K I) K) (K K K)
      2: -> I K (K I) K
      3: -> K (K I) K
      4: -> K I
    Value = K I
    ただしく,K I = false になりました
    
    not false を実行してみます.
    ski> not false
    Evaluation of S (S I (K (K I))) (K K) (K I)
      0: -> S I (K (K I)) (K I) (K K (K I))
      1: -> I (K I) (K (K I) (K I)) (K K (K I))
      2: -> I (K I) (K I) K
      3: -> K I (K I) K
      4: -> I K
      5: -> K
    Value = K
    ski>
    こちらも正しく K = true になりました.
    	

    では or, and, imply を各自で定義してみてください. or はラムダ式でいうと,λx.(x true y) を実現すればよいですね

  5. コンビネータによる自然数の表現

    S, K, I がチューリングマシンと同等の能力を持つことを確信するためには, つまり,再帰関数がこれで記述できることを確信するには,まずは,再帰関数の 計算対象である自然数を模擬する体形を S, K, I で構築しなければなりません. 自然数を表す方法は色々なものがあるようですが,その中で2つの方法が主流だそうです. それらは,チャーチ(Alonzo Church)流の自然数とバーレンットレクト(Henk Barendregt)と Barendsen の教科書 Introduction to Lambda Calculus [Barendregt] に書いてあるものです.ここではまず,後者,バーレンットレクト(Henk Barendregt)らの 教科書に書いてあるものを少し私流に変えさせていただいた方法 を説明し,後でチャーチ流のものについても少し触れようと思います.バーレントレクト等の 方法そのものでなく,似て非なるものを説明するということでとても心苦しいのですが, 説明がかなり楽になりますので,差の部分は明示するようにしますので,皆様の方で 後で置き換えてください

    1. バーレントレクトらの自然数の表現方法ダッシュ

      これは考え方はかなり単純ですが,SKI だけでやっていると,その単純な考え方が 見えてこないことがありますので,まずは,考え方を理解するために,SKI に こだわらないでやって,あとで,それらが SKI で実現できることをお話します. ここの実験は SKI インタープリタの最初の状態,つまり,S, K, I の コンビネータだけが定義されている状態から始めてください.プログラムを Ruby に読み込んで,top を起動した状態です.最初の状態に戻すには :reset コマンドを実行するのが簡単です.

      まず,準備として,次のような関係をもつコンビネータの集まり pair, 1st, 2ndを考えてみます.

      • pair x y は何らかの式を表す
      • 1st (pair x y) -> x
      • 2nd (pair x y) -> y

      ここで XXX -> YYY は,0回以上の変換で XXX が YYY に変換されることを表すとします.

      これはぶっちゃけ,LISP の cons, car, cdr ですね.

      これらは,次のようなコンビネータの変換式を定義しておくと実現できます.

      • pair ?x ?y ?which => ?which ?x ?y
      • 1st ?pair => ?pair K
      • 2nd ?pair => ?pair (K I)

      K x y -> x ,つまり最初の要素を返し,(K I) x y -> I y -> y, つまり,2番目の要素を返すことを思い出してください.また,pair は, 実は,ヴィレオと呼ばれるコンビネータで,V で表され,S, K, I で実現可能です. ( 一応言っておくと,V は,(S ((S (K S)) ((S (K K)) ((S (K S)) ((S (K (S I))) ((S (K K)) I)))))) (K ((S (K K)) I)) とすれば実現できます)

      一応,うまく行くか確かめてみましょう.

      定義が最初の状態に戻っていることを確実にするため :reset しておきます.
      ski> :reset
        Id(s) and Rules return to originals
      
      まず,上の定義を入れます.
      ski> pair ?x ?y ?which => ?which ?x ?y
      rule of 'pair ?x ?y ?which' is defined. Use :s for check.
      ski> 1st ?pair => ?pair K
      rule of '1st ?pair' is defined. Use :s for check.
      ski> 2nd ?pair => ?pair (K I)
      rule of '2nd ?pair' is defined. Use :s for check.
      
      うまく定義されたか確認します.
      ski> :s
       Definition of combinator(s)
          S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
          K ?X ?Y => ?X
          I ?X => ?X
          pair ?x ?y ?which => ?which ?x ?y
          1st ?pair => ?pair K
          2nd ?pair => ?pair (K I)
       Definition of identifier(s)
       End
      組み込みの S, K, I に加えて,pair, 1st, 2nd がちゃんと定義されてました.
      
      ski> 1st (pair a b)
      Evaluation of 1st (pair a b)
        0: -> pair a b K
        1: -> K a b
        2: -> a
      Value = a
      1st は OK です.
      
      ski> 2nd (pair a b)
      Evaluation of 2nd (pair a b)
        0: -> pair a b (K I)
        1: -> K I a b
        2: -> I b
        3: -> b
      Value = b
      2nd も OK です.
      ski>	

      うまく行きました.

      真偽値 true は K で,false は (K I) で表すことは前に述べましたが, K, (K I) をすぐ,true, false に読み替えられないので,しばらく, true, false を未定義のコンビネータとしてそのままの名前で使います.

      ここでのの表現方法では自然数を次のように表します.

      • 0 は pair true I
        (注意:バーレントレクトらの教科書に書いてある方法では, 0 を表現するのに I を 使っています.次で,0 かどうかの判定を行うコンビネータ is_zero の 説明が難しくなるので,ここを (pair true I) にしました)

      • n は (pair false <n-1 の表現>)
        というように再帰的に定義します.自然数 n の全体を書くと,

        のように,一番奥に 0 つまり (pair true I) があって,それを n 個の (pair false -) が取り囲んでいます.木の形で書けば,

        です.

      この形を理解してしまうと, 0 かどうか調べるコンビネータの式 is_zero, 1 加える add1,1 引く sub1 はすぐできると思います.

      • is_zero ?n => 1st ?n
        0 = pair true I 以外はみな第1成分が false になっています.

      • add1 ?n => pair false ?n
        上に書いた自然数の再帰的な定義そのものですね.

      • sub1 ?n => 2nd ?n
        false を一つ剥がせばよい訳です.ただし,0 = (pair true I) に適用すると 自然数でないものになってしまいますから,1 以上の自然数にだけ適用される ように気を付けます.

      一応,確認しましょう.

      まず,is_zero, add1, sub1 を定義します.先ほどからの続きですので
      pair, 1st, 2nd はすでに定義されています.
      ski> is_zero ?n => 1st ?n
      rule of 'is_zero ?n' is defined. Use :s for check.
      ski> add1 ?n => pair false ?n
      rule of 'add1 ?n' is defined. Use :s for check.
      ski> sub1 ?n => 2nd ?n
      rule of 'sub1 ?n' is defined. Use :s for check.
      
      次にこれらを使って.自然数 0, 1, 2, 3 を定義します.
      こちらはコンビネータの式を表す名前として定義します.別にコンビネータとして
      定義しても良いのですが,変換ルールっぽいものをコンビネータとして定義して
      単にコンビネータの列を短く書きたい場合は名前付けをしています.
      ski> 0 := pair true I
      identifier 0 is defined. Use :s for check
      ski> 1 := add1 0
      identifier 1 is defined. Use :s for check
      ski> 2 := add1 1
      identifier 2 is defined. Use :s for check
      ski> 3 := add1 2
      identifier 3 is defined. Use :s for check
      
      今まで定義したものをみてみましょう.
      ski> :s
       Definition of combinator(s)
          S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
          K ?X ?Y => ?X
          I ?X => ?X
          pair ?x ?y ?which => ?which ?x ?y
          1st ?pair => ?pair K
          2nd ?pair => ?pair (K I)
          is_zero ?n => 1st ?n
          add1 ?n => pair false ?n
          sub1 ?n => 2nd ?n
       Definition of identifier(s)
          0 := pair true I
          1 := add1 (pair true I)
          2 := add1 (add1 (pair true I))
          3 := add1 (add1 (add1 (pair true I)))
       End
      こんな感じの定義です.
      
      では 3 はどんな値になっているでしょうか.
      ski> 3
      Evaluation of add1 (add1 (add1 (pair true I)))
        0: -> pair false (add1 (add1 (pair true I)))
        1: -> pair false (pair false (add1 (pair true I)))
        2: -> pair false (pair false (pair false (pair true I)))
      Value = pair false (pair false (pair false (pair true I)))
      add1 が全部展開されると,このように false を 3 回 pair で
      0 = (pair true I) にくっつけた形です.
      
      is_zero が正しく働くかどうか確かめてみます.
      まず,0 に対しては?
      ski> is_zero 0
      Evaluation of is_zero (pair true I)
        0: -> 1st (pair true I)
        1: -> pair true I K
        2: -> K true I
        3: -> true
      Value = true
      はい,ただしく true になりました.
      
      1 に対しては?
      ski> is_zero 1
      Evaluation of is_zero (add1 (pair true I))
        0: -> 1st (add1 (pair true I))
        1: -> add1 (pair true I) K
        2: -> pair false (pair true I) K
        3: -> K false (pair true I)
        4: -> false
      Value = false
      これも正しく,false になりました.
      
      しつこいですが,2 に対しても調べておきます.
      ski> is_zero 2
      Evaluation of is_zero (add1 (add1 (pair true I)))
        0: -> 1st (add1 (add1 (pair true I)))
        1: -> add1 (add1 (pair true I)) K
        2: -> pair false (add1 (pair true I)) K
        3: -> K false (add1 (pair true I))
        4: -> false
      Value = false
      はい,正しく動作しています.
      
      では,計算結果に対してうまく働くか?
      ski> is_zero (sub1 1)
      Evaluation of is_zero (sub1 (add1 (pair true I)))
        0: -> 1st (sub1 (add1 (pair true I)))
        1: -> sub1 (add1 (pair true I)) K
        2: -> sub1 (pair false (pair true I)) K
        3: -> 2nd (pair false (pair true I)) K
        4: -> pair false (pair true I) (K I) K
        5: -> K I false (pair true I) K
        6: -> I (pair true I) K
        7: -> pair true I K
        8: -> K true I
        9: -> true
      Value = true
      大丈夫みたいです.
      
      関数を二つ重ねでは?
      ski> is_zero (sub1 (sub1 2))
      Evaluation of is_zero (sub1 (sub1 (add1 (add1 (pair true I)))))
        0: -> 1st (sub1 (sub1 (add1 (add1 (pair true I)))))
        1: -> sub1 (sub1 (add1 (add1 (pair true I)))) K
        2: -> sub1 (sub1 (pair false (add1 (pair true I)))) K
        3: -> sub1 (sub1 (pair false (pair false (pair true I)))) K
        4: -> 2nd (sub1 (pair false (pair false (pair true I)))) K
        5: -> sub1 (pair false (pair false (pair true I))) (K I) K
        6: -> 2nd (pair false (pair false (pair true I))) (K I) K
        7: -> pair false (pair false (pair true I)) (K I) (K I) K
        8: -> K I false (pair false (pair true I)) (K I) K
        9: -> I (pair false (pair true I)) (K I) K
       10: -> pair false (pair true I) (K I) K
       11: -> K I false (pair true I) K
       12: -> I (pair true I) K
       13: -> pair true I K
       14: -> K true I
       15: -> true
      Value = true
      これも大丈夫です.
      
      最後にsub1 で 0 にならないものに対しては?
      ski> is_zero (sub1 (sub1 3))
      Evaluation of is_zero (sub1 (sub1 (add1 (add1 (add1 (pair true I))))))
        0: -> 1st (sub1 (sub1 (add1 (add1 (add1 (pair true I))))))
        1: -> sub1 (sub1 (add1 (add1 (add1 (pair true I))))) K
        2: -> sub1 (sub1 (pair false (add1 (add1 (pair true I))))) K
        3: -> sub1 (sub1 (pair false (pair false (add1 (pair true I))))) K
        4: -> sub1 (sub1 (pair false (pair false (pair false (pair true I))))) K
        5: -> 2nd (sub1 (pair false (pair false (pair false (pair true I))))) K
        6: -> sub1 (pair false (pair false (pair false (pair true I)))) (K I) K
        7: -> 2nd (pair false (pair false (pair false (pair true I)))) (K I) K
        8: -> pair false (pair false (pair false (pair true I))) (K I) (K I) K
        9: -> K I false (pair false (pair false (pair true I))) (K I) K
       10: -> I (pair false (pair false (pair true I))) (K I) K
       11: -> pair false (pair false (pair true I)) (K I) K
       12: -> K I false (pair false (pair true I)) K
       13: -> I (pair false (pair true I)) K
       14: -> pair false (pair true I) K
       15: -> K false (pair true I)
       16: -> false
      Value = false
      はい,うまく働いています.
      長いので is_zero (sub1 2) にしておけばよかったですね.
      ski>	

      以上で,自然数の基本的な関数 is_zero, add1, sub1 が出来ました. さらに自由に演算ができることを示すには足し算あたりを書いてみると 良いと思いますが,これは再帰的な定義が必要になってきます. コンビネータによる再帰的な定義能力の説明は次節なのですが, やはり,できることを確認していきたいので,ちょっとズルをして 足し算 add ?x ?y のコンビネータを作ってみます.ズルというのは, じつは,ここで作ったコンビネータのインタープリタは再帰的な定義が 可能になってしまっていたのです.

      足し算を再帰で書くのは,C言語っぽく書くと,

        add(x, y) {
          if is_zero(x)
              y;
          else
              add1(add(sub1(x), y);
        }
      
      ですね.ほぼ,この通りのコンビネータを定義してみます.
        add ?x ?y => (is_zero ?x) ?y (add1 (add (sub1 ?x) ?y))
      
        true  ?x  ?y => ?x
        false ?x ?y => ?y
      
      ここで作ったコンビネータのインタープリタは単にマッチした左辺を 右辺に置き換えているだけなので,これがうまく働いでしまいます. 本当は,コンビネータの式の add の右辺に再度 add が表れるのは反則ですので, これは次節で SKI に置き換えますが,ここではとにかく計算ができるということを 味わいたいので,このままやります.

      さて,この定義を実際に動かすためには,いままで,真偽値の名前としてだけ使っていた, true と false に正しい定義を与えることが必要です.これは K と (K I) なのですが,変換の最中に,K, (K I) に置き換えられても分かりにくいので 上の最後の2行のように,直接,コンビネータの定義を与えておきます.

      では,やってみましょう.

      まず,上の定義を追加します.
      ski> add ?x ?y => (is_zero ?x) ?y (add1 (add (sub1 ?x) ?y))
        Rule of 'add ?x ?y' is defined.
      ski> true  ?x  ?y => ?x
        Rule of 'true ?x ?y' is defined.
      ski> false ?x ?y => ?y
        Rule of 'false ?x ?y' is defined.
      
      現在のコンビネータの定義は次のようになっています
      ski> :s
       Definition of combinator(s)
          S ?X ?Y ?Z => ?X ?Z (?Y ?Z)
          K ?X ?Y => ?X
          I ?X => ?X
          pair ?x ?y ?which => ?which ?x ?y
          1st ?pair => ?pair K
          2nd ?pair => ?pair (K I)
          is_zero ?n => 1st ?n
          add1 ?n => pair false ?n
          sub1 ?n => 2nd ?n
          add ?x ?y => is_zero ?x ?y (add1 (add (sub1 ?x) ?y))
          true ?x ?y => ?x
          false ?x ?y => ?y
       Definition of identifier(s)
          0 := pair true I
          1 := add1 (pair true I)
          2 := add1 (add1 (pair true I))
          3 := add1 (add1 (add1 (pair true I)))
       End
      
      :o は,変換過程を1つのコンビネータのルールの適用ごとでなく,
      全部を一通り適用したごとに表示するモードにします.
      ski> :o
      one step mode = false
      
      一番基本的なケースは第1引数が 0 の場合です.
      ski> add 0 1
      Evaluation of add (pair true I) (add1 (pair true I))
        0: -> is_zero (pair true I) (pair false (pair true I)) (add1 (add (sub1 (pair true I)) (pair false (pair true I))))
        1: -> 1st (pair true I) (pair false (pair true I)) (pair false (is_zero (2nd (pair true I)) (pair false (pair true I)) (add1 (add (sub1 (2nd (pair true I))) (pair false (pair true I))))))
        2: -> pair true I K (pair false (pair true I)) (pair false (1st (pair true I (K I)) (pair false (pair true I)) (pair false (is_zero (2nd (pair true I (K I))) (pair false (pair true I)) (add1 (add (sub1 (2nd (pair true I (K I)))) (pair false (pair true I))))))))
        3: -> K true I (pair false (pair true I)) (pair false (K I true I K (pair false (pair true I)) (pair false (1st (K I true I (K I)) (pair false (pair true I)) (pair false (is_zero (2nd (K I true I (K I))) (pair false (pair true I)) (add1 (add (sub1 (2nd (K I true I (K I)))) (pair false (pair true I))))))))))
        4: -> pair false (pair true I)
      Value = pair false (pair true I)
      false の個数は1個なのでこれは 1 のコンビネータ表現です.
      
      次は第1引数が1の場合をやってみます.
      ski> add 1 2
      Evaluation of add (add1 (pair true I)) (add1 (add1 (pair true I)))
        0: -> is_zero (pair false (pair true I)) (pair false (add1 (pair true I))) (add1 (add (sub1 (pair false (pair true I))) (pair false (add1 (pair true I)))))
        1: -> 1st (pair false (pair true I)) (pair false (pair false (pair true I))) (pair false (is_zero (2nd (pair false (pair true I))) (pair false (add1 (pair true I))) (add1 (add (sub1 (2nd (pair false (pair true I)))) (pair false (add1 (pair true I)))))))
        2: -> pair false (pair true I) K (pair false (pair false (pair true I))) (pair false (1st (pair false (pair true I) (K I)) (pair false (pair false (pair true I))) (pair false (is_zero (2nd (pair false (pair true I) (K I))) (pair false (add1 (pair true I))) (add1 (add (sub1 (2nd (pair false (pair true I) (K I)))) (pair false (add1 (pair true I)))))))))
        3: -> K false (pair true I) (pair false (pair false (pair true I))) (pair false (K I false (pair true I) K (pair false (pair false (pair true I))) (pair false (1st (K I false (pair true I) (K I)) (pair false (pair false (pair true I))) (pair false (is_zero (2nd (K I false (pair true I) (K I))) (pair false (add1 (pair true I))) (add1 (add (sub1 (2nd (K I false (pair true I) (K I)))) (pair false (add1 (pair true I)))))))))))
        4: -> pair false (K true I (pair false (pair false (pair true I))) (pair false (K I true I K (pair false (pair false (pair true I))) (pair false (1st (K I true I (K I)) (pair false (pair false (pair true I))) (pair false (is_zero (2nd (K I true I (K I))) (pair false (add1 (pair true I))) (add1 (add (sub1 (2nd (K I true I (K I)))) (pair false (add1 (pair true I))))))))))))
        5: -> pair false (pair false (pair false (pair true I)))
      Value = pair false (pair false (pair false (pair true I)))
      はい,false の数が3個ですから確かに 1+2 が計算できています.
      
      最後に,2+3 をやってみます.
      ski> add 2 3
      Evaluation of add (add1 (add1 (pair true I))) (add1 (add1 (add1 (pair true I))))
        0: -> is_zero (pair false (add1 (pair true I))) (pair false (add1 (add1 (pair true I)))) (add1 (add (sub1 (pair false (add1 (pair true I)))) (pair false (add1 (add1 (pair true I))))))
        1: -> 1st (pair false (pair false (pair true I))) (pair false (pair false (add1 (pair true I)))) (pair false (is_zero (2nd (pair false (add1 (pair true I)))) (pair false (add1 (add1 (pair true I)))) (add1 (add (sub1 (2nd (pair false (add1 (pair true I))))) (pair false (add1 (add1 (pair true I))))))))
        2: -> pair false (pair false (pair true I)) K (pair false (pair false (pair false (pair true I)))) (pair false (1st (pair false (pair false (pair true I)) (K I)) (pair false (pair false (add1 (pair true I)))) (pair false (is_zero (2nd (pair false (add1 (pair true I)) (K I))) (pair false (add1 (add1 (pair true I)))) (add1 (add (sub1 (2nd (pair false (add1 (pair true I)) (K I)))) (pair false (add1 (add1 (pair true I))))))))))
        3: -> K false (pair false (pair true I)) (pair false (pair false (pair false (pair true I)))) (pair false (K I false (pair false (pair true I)) K (pair false (pair false (pair false (pair true I)))) (pair false (1st (K I false (pair false (pair true I)) (K I)) (pair false (pair false (add1 (pair true I)))) (pair false (is_zero (2nd (K I false (add1 (pair true I)) (K I))) (pair false (add1 (add1 (pair true I)))) (add1 (add (sub1 (2nd (K I false (add1 (pair true I)) (K I)))) (pair false (add1 (add1 (pair true I))))))))))))
        4: -> pair false (K false (pair true I) (pair false (pair false (pair false (pair true I)))) (pair false (K I false (pair true I) K (pair false (pair false (pair false (pair true I)))) (pair false (1st (pair false (pair true I) (K I) (K I)) (pair false (pair false (add1 (pair true I)))) (pair false (is_zero (2nd (add1 (pair true I) (K I) (K I))) (pair false (add1 (add1 (pair true I)))) (add1 (add (sub1 (2nd (add1 (pair true I) (K I) (K I)))) (pair false (add1 (add1 (pair true I)))))))))))))
        5: -> pair false (pair false (K true I (pair false (pair false (pair false (pair true I)))) (pair false (K I false (pair true I) (K I) K (pair false (pair false (pair false (pair true I)))) (pair false (1st (pair false (pair true I) (K I) (K I) (K I)) (pair false (pair false (add1 (pair true I)))) (pair false (is_zero (2nd (add1 (pair true I) (K I) (K I) (K I))) (pair false (add1 (add1 (pair true I)))) (add1 (add (sub1 (2nd (add1 (pair true I) (K I) (K I) (K I)))) (pair false (add1 (add1 (pair true I))))))))))))))
        6: -> pair false (pair false (pair false (pair false (pair false (pair true I)))))
      Value = pair false (pair false (pair false (pair false (pair false (pair true I)))))
      はい,無事,false の数が 2+3 = 5 個になりました.
      ski>
      

      ちょっと,まとめておきましょう.

      ここで新たに導入したコンビネータは,

      • pair は,ヴィオレ(V)という名前がついたコンビネータで,

        pair ?x ?y ?z => ?z ?x ?y

        という働きをし,S, K, I で定義できる(実現例の一つは上に示した).

      • T を T ?x ?y => ?y ?x という機能を持ったコンビネータとしておきます. これは, T = S (K (S I)) K とすれば,S, K, I で実現できます. この T を使えば,以下のように 1st と 2nd が作れます.

      • 1st = T K
        2nd = T (K I)

      • is_zero = 1st = T K
        add1 = pair false = V false
        sub1 = 2nd = T (K I)

      • true = K
        false = (K I)

      以上で,再帰メカニズム以外は S, K, I で実現できることが分かりました.

      最後に,巻末にあげたバーレントレクトの入門書と微妙に違う表現方法をとりました. それは,0 を I とせず, pair true I としたところですが,これは,途中まで, true = K, false = (K I) の表現を使わずに,true, false の字ずらで表示したかった からです.0 を I とすると,true, false を K と (K I) に戻さないときは, is_zero がちょっと面倒になります.特に私は新たな方法を提案するつもりはないので, ものの本を読むときに,そちらの流儀に従ってください.

    2. チャーチ流の自然数の表現方法に関して

      ここではチャーチ流の自然数の表現方法に関する基礎的な知識をいくつか述べます. しかし,私もあまり知らないので,これについては深入りはしません.ご興味の ある方は成書で調べてください.

      自然数 n の表現をλ式 λf.λx.f(f ...(f x)...) で表現します.ここに f は x に n 回適用してあります.

      つまり,数 n とは関数 f とデータ x をとって,x に f を n 回適用する 高階関数と思うのです.

      注意:この表現方法については,自然数同士の 同等性の確認が,片方からもう一方へのリダクションによってのみでは 確認できないこともありそうです.二つの同等性は,関数としての同等性で

      n1 と n2 は任意の f と x に対して n1 f x = n2 f x であるとき,
      かつ,その時に限り等しい

      といった定義になりそうです.

      この方法による自然数 n のコンビネータによる表現を X_n と書くことにし,コンビネータ B を

      B ?x ?y ?z => ?x (?y ?z)

      となるものとします(このコンビネータは再帰のところでももう一度でてきます). そうすると, この手法の自然数の表現 X_0, X_1, X_2, X_3, ... は次のように求まります.

      • X_0 f x = x = (K I) f x

      • X_1 f x = f x = I f x

      • X_2 f x = f (f x) = S B I f x
        (S B I f x = (B f) (I f) x = B f f x = f (f x)

      • X_3 f x = f (f (f x)) = f ([2] f x) = (S B [2]) f x
        (S B X_2 f x = (B f) (X_2 f) x = f (X_2 f) x))

        ・・・

      ということで

      X_0 = K I, X_1 = I, X_2 = (S B) I, X_3 = (S B) [2] = (S B) (S B I), ...

      になります.

      つまり,+ 1 をとる操作が (S B) ですね.

      この表現は足し算や掛け算が簡単に書けます.

      1. 足し算は (B S) (B B)
        B ?x ?y ?z => ?x (?y ?z) と定義した上でインタープリタで

        (B S) (B B) X_n X_m f x を実行してみましょう.

        ski> (B S) (B B) X_n X_m f x
        Evaluation of B S (B B) X_n X_m f x
          0: -> S (B B X_n) X_m f x
          1: -> B B X_n f (X_m f) x
          2: -> B (X_n f) (X_m f) x
          3: -> X_n f (X_m f x)
        Value = X_n f (X_m f x)	

        x に f を m 回適用した結果に,続いて,f を n 回適用した形になっていますので, f を x に n + m 回適用したことになります.

      2. 掛け算は B
        ski> B X_n X_m f x
        Evaluation of B X_n X_m f x
          0: -> X_n (X_m f) x
        Value = X_n (X_m f) x

        こちらはf を m 回適用する関数 (X_m f) を n 回適用する訳ですから, f を n*m 回適用することになる訳です.


        上記2つは参考文献にあるスタンフォードの哲学辞典の "Combinatory Logic" に直接コンビネータの式として載っていました.以下は,そのような コンビネータの式が見つからなかったので,主に,λ式での記述などをもとに 考えたことを書きます.

      3. 0 の判定は X_n λx.false true で可能です
        ここに true=K, false=(K I) とします.
        これを関数の形に書き直すと,λn.(n λx.false true) ですから,コンビネータの 式でこれを満たすものとしては

        S (S I (K (K false))) (K true)

        があります.

      4. 1 以上の自然数から1 引く関数は難しいらしい
        これについてはコンビネータの式まで落とす力は私にはありませんので,考え方だけ 示しておきます.考え方自身は簡単です.

        自然数 n の表現 X_n は,関数 f とデータ x をとって,x に f を n 回適用して返す 関数ですが,最初の1回を適用しないように工夫すれば,f を n-1 回適用する関数, すなわち,X_(n-1) が出来ます.

        この方法には関数を使うもの,pair を使うものなどいろいろあるようですが,ここでは pair を使う方法を示します.ここで pair は先にバーレントレクトの亜流の自然数表現を 説明した時出てきたものです. 1st (pair x y) = x, 2nd (pair x y) = y という 性質をもったコンビネータです.

        X_(n-1) の動作
          与えられた関数とデータを f と x とします.

        1. x2 = pair false x

        2. f2 = λu.(if 1st u = false then (pair true (2nd u))

          else (pair true (f 2nd u)) end)

        3. result = X_n f1 x2

        4. return (2nd result)

        つまり,最初に第1成分を false,第2成分を x にしたペア x2 を作り, f2 は第1成分が false なら true と第2成分を pair にしたものを返し, そうでなければ,第2成分に f を適用し,それを第2成分,第1成分は true の pair を返します.そうして,X_n を使って,f2 を x2 に n 回適用すると, 最初の1回だけ,f の適用がないので,f が n-1 回適用された結果を 第2成分に持つデータができます.最後に,その第2成分を返せばよいわけです.

      この節のはじめでも注意として述べましたが,このような,1を減ずる方法を 導入すると,この表現方法では,自然数の同等性の 判定が形の上からだけではやりにくいと思われます.

    
    
  6. コンビネータによる再帰の実現方法

    上の自然数の表現のところでは,足し算 add ?x ?y を,今のインタープリタの抜け穴を 使って,

    add ?x ?y => (is_zero ?x) ?y (add1 (add (sub1 ?x) ?y))

    と,再帰的に定義しました.これは,S, K, I のコンビネータだけで定義できるでしょうか? この節では,この方法を述べます.なお,is_zero, add1, sub1 は,S, K, I で実現できることを 示していますので,このまま使います.

    これを S, K, I で表すときの困難は,右辺に add が含まれていることで,その add を この定義式で置き換えても,再度 add が入ってしまい,きりがないことです. しかし,これは add を別のコンビネータの引数にすることで解決できます. 一段,メタな関数を考えるわけです.

    meta_add ?f ?x ?y => (is_zero ?x) ?y (add1 (?f (sub1 ?x) ?y))

    この式はコンビネータの定義として書いてありますが,これは S, K, I だけで同じ ことをするコンビネータの式を書くことができます(とても長いですが).そうすれば, 次のようなコンビネータ

    execute ?g ?x ?y => ?g ?g ?x ?y

    という変換を行うコンビネータを使って,

    execute meta_add 数1 数2

    と呼び出すことにより,execute で meta_add が二つにコピーされ,meta_add の 中でも,meta_add を呼ぶということができます.ここで,meta_add は名前でなく, 上で書いた meta_add の右辺に展開されるコンビネータの式を表しています.

    上の execute が S, K, I で実現できることを示しておきましょう.

    一応,上の二つをインタープリタにコピー&ペーストして実際に要求通りの式に なっていることを確認しておきましょう.is_zero,add1, sub1 が変換されてしまわない ように,:reset コマンドで,定義を最初の状態に戻しておいてください.あるいは ruby に抜けてプログラムを読み直して,再度,top を起動するのでも良いです.

    :reset で定義を最初の状態に戻します.
    ski> :reset
      Id(s) and Rules return to originals
    
    execute をコピペして,名前 execute に設定します.
    ski> execute :=  (S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K K)) ((S I) I)))) (K I)))))) (K (K I))
    identifier execute is defined. Use :s for check
    
    execute g x y を計算してみましょう.
    ski> execute g x y
    Evaluation of S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S I I))) (K I))))) (K (K I)) g x y
      0: -> S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S I I))) (K I)))) g (K (K I) g) x y
      1: -> K S g (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) (S I I))) (K I))) g) (K (K I) g) x y
      2: -> K S g (K (S (K S)) g (S (K (S (K K))) (S (S (K S) (S (K K) (S I I))) (K I)) g)) (K (K I) g) x y
      3: -> K S g (K (S (K S)) g (K (S (K K)) g (S (S (K S) (S (K K) (S I I))) (K I) g))) (K (K I) g) x y
      4: -> K S g (K (S (K S)) g (K (S (K K)) g (S (K S) (S (K K) (S I I)) g (K I g)))) (K (K I) g) x y
      5: -> K S g (K (S (K S)) g (K (S (K K)) g (K S g (S (K K) (S I I) g) (K I g)))) (K (K I) g) x y
      6: -> K S g (K (S (K S)) g (K (S (K K)) g (K S g (K K g (S I I g)) (K I g)))) (K (K I) g) x y
      7: -> K S g (K (S (K S)) g (K (S (K K)) g (K S g (K K g (I g (I g))) (K I g)))) (K (K I) g) x y
      8: -> S (S (K S) (S (K K) (S (K (I g (I g))) I))) (K I) x y
      9: -> S (K S) (S (K K) (S (K (I g (I g))) I)) x (K I x) y
     10: -> K S x (S (K K) (S (K (I g (I g))) I) x) (K I x) y
     11: -> K S x (K K x (S (K (I g (I g))) I x)) (K I x) y
     12: -> K S x (K K x (K (I g (I g)) x (I x))) (K I x) y
     13: -> S (K (I g (I g) (I x))) I y
     14: -> K (I g (I g) (I x)) y (I y)
     15: -> I g (I g) (I x) (I y)
     16: -> g g x y
    Value = g g x y
    はい,たしかに g が自分自身を最初の引数として呼び出される形式ができました.
    
    次は meta_add をコピペします.
    ski> meta_add := (S (K (S ((S (K S)) ((S ((S (K S)) ((S (K K)) ((S (K is_zero)) I)))) (K I)))))) ((S (K (S (K (S (K add1)))))) ((S ((S (K S)) ((S (K (S (K S)))) ((S (K (S (K K)))) ((S ((S (K S)) ((S (K K)) I))) (K ((S (K sub1)) I))))))) (K (K I))))
    identifier meta_add is defined. Use :s for check
    
    meta_add g x y を求めてみましょう.
    ski> meta_add g x y
    Evaluation of S (K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I))))) (S (K (S (K (S (K add1))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K sub1) I)))))) (K (K I)))) g x y
      0: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (S (K (S (K (S (K add1))))) (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K sub1) I)))))) (K (K I))) g) x y
      1: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (S (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K sub1) I)))))) (K (K I)) g)) x y
      2: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (S (K S) (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K sub1) I))))) g (K (K I) g))) x y
      3: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (K S g (S (K (S (K S))) (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K sub1) I)))) g) (K (K I) g))) x y
      4: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (K S g (K (S (K S)) g (S (K (S (K K))) (S (S (K S) (S (K K) I)) (K (S (K sub1) I))) g)) (K (K I) g))) x y
      5: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (K S g (K (S (K S)) g (K (S (K K)) g (S (S (K S) (S (K K) I)) (K (S (K sub1) I)) g))) (K (K I) g))) x y
      6: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (K S g (K (S (K S)) g (K (S (K K)) g (S (K S) (S (K K) I) g (K (S (K sub1) I) g)))) (K (K I) g))) x y
      7: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (K S g (K (S (K S)) g (K (S (K K)) g (K S g (S (K K) I g) (K (S (K sub1) I) g)))) (K (K I) g))) x y
      8: -> K (S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)))) g (K (S (K (S (K add1)))) g (K S g (K (S (K S)) g (K (S (K K)) g (K S g (K K g (I g)) (K (S (K sub1) I) g)))) (K (K I) g))) x y
      9: -> S (S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I))) (S (K (S (K add1))) (S (S (K S) (S (K K) (S (K (I g)) (S (K sub1) I)))) (K I))) x y
     10: -> S (K S) (S (S (K S) (S (K K) (S (K is_zero) I))) (K I)) x (S (K (S (K add1))) (S (S (K S) (S (K K) (S (K (I g)) (S (K sub1) I)))) (K I)) x) y
     11: -> K S x (S (S (K S) (S (K K) (S (K is_zero) I))) (K I) x) (K (S (K add1)) x (S (S (K S) (S (K K) (S (K (I g)) (S (K sub1) I)))) (K I) x)) y
     12: -> K S x (S (K S) (S (K K) (S (K is_zero) I)) x (K I x)) (K (S (K add1)) x (S (K S) (S (K K) (S (K (I g)) (S (K sub1) I))) x (K I x))) y
     13: -> K S x (K S x (S (K K) (S (K is_zero) I) x) (K I x)) (K (S (K add1)) x (K S x (S (K K) (S (K (I g)) (S (K sub1) I)) x) (K I x))) y
     14: -> K S x (K S x (K K x (S (K is_zero) I x)) (K I x)) (K (S (K add1)) x (K S x (K K x (S (K (I g)) (S (K sub1) I) x)) (K I x))) y
     15: -> K S x (K S x (K K x (K is_zero x (I x))) (K I x)) (K (S (K add1)) x (K S x (K K x (K (I g) x (S (K sub1) I x))) (K I x))) y
     16: -> K S x (K S x (K K x (K is_zero x (I x))) (K I x)) (K (S (K add1)) x (K S x (K K x (K (I g) x (K sub1 x (I x)))) (K I x))) y
     17: -> S (S (K (is_zero (I x))) I) (S (K add1) (S (K (I g (sub1 (I x)))) I)) y
     18: -> S (K (is_zero (I x))) I y (S (K add1) (S (K (I g (sub1 (I x)))) I) y)
     19: -> K (is_zero (I x)) y (I y) (K add1 y (S (K (I g (sub1 (I x)))) I y))
     20: -> K (is_zero (I x)) y (I y) (K add1 y (K (I g (sub1 (I x))) y (I y)))
     21: -> is_zero (I x) (I y) (add1 (I g (sub1 (I x)) (I y)))
     22: -> is_zero x y (add1 (g (sub1 x) y))
    Value = is_zero x y (add1 (g (sub1 x) y))
    はい,確かに要求された再帰的な定義になりました.
    ski>
    

    以上で execute と meta_add のチェックが終わりましたが,これらはそれぞれ コンビネータ論理(Combinatory Logic) のお話 で述べた,λ式から SKI コンビネータへの変換ツールで求めています.人間の手で 「うーん」と唸りながら求めたら,もう少し短いものが見つかるかもしれません.

    最後に,再帰の話題として,いくつかのコンビネータと不動点のお話を簡単にして 終わりにします.

    F を何らかのコンビネータの式だとします.このとき,コンビネータの式 Exp が

    Exp -> F Exp

    を満たすとき,Exp を F の不動点(fixed point)と言います. 不動点は非常に重要です.例えば,先ほどの meta_add の不動点は,

    Exp = meta_add Exp

    ですから

    meta_add Exp x y -> Exp x y

    となり,実は,(大雑把に言って)この Exp が求める足し算を行うコンビネータの 式 add になります.

    不動点は,もし,次のような二つのコンビネータが存在すれば,常に存在することが 示されます.

    これら二つが存在するとき,コンビネータの式 F に対する不動点が,

    Exp = (B F M) (B F M)

    で求められます.なぜなら,

    Exp = (B F M) (B F M)

    = B F M (B F M) /* 括弧の表し方を優先度に合わせただけ */

    = F (M (B F M)) /* B を適用 */

    = F ((B F M) (B F M)) /* M を適用 */

    ということで,Exp = (B F M) (B F M) が F の不動点であることがわかります. いやあ,世の中の人はよくこんなもの思いつきますね.

    以上で,このページの説明は終わりです.あとは, 参考文献に挙げたようなきちんと書いてある文献で 勉強してください.

プログラムリスト

利用には,「簡単な演算子順位法によるパーサー in Ruby」の パーサーの掲載リスト(Version 0.96 2019.02.24 以降)が必要です. 詳細は,「ちょっと動かしてみる」「Simple SKI Interpreter の機能の説明」 を見てください.それと,上のパーサーへのリンクは,そちらのページのローディングに 時間がかかると,きちんとプログラムリストのところに位置づけられないことがあります. そのような場合はもう一度リンクをクリックしなおしてみてください.

# Simple SKI Combinator Interpreter
#   by Akihiko Koga
#   Ver. 0.55  2019.02.26

$sop_ops[:"=>"]  = ["=>",  4000, :xfy]
$sop_ops[:":="]  = [":=",  4000, :xfy]
$sop_ops[:":di"] = [":di", 4000, :fy]
$sop_ops[:":dr"] = [":dr", 4000, :fy]
$sop_ops[:":lim"] = [":lim", 4000, :fy]
$sop_ops[:":p"] = [":p", 4000, :fy]
$sop_ops[:":load"] = [":load", 4000, :fy]

$ski_rules = {}
[
  "(S ?X ?Y ?Z) => (?X ?Z) (?Y ?Z)",
  "(K ?X ?Y)    => ?X",
  "(I ?X)       => ?X",
].map {|rule| x = sop_parse(rule); $ski_rules[x[1]] = x[2]}

$ski_table = {}

$ski_initial = [$ski_rules.clone, $ski_table.clone]

$ski_limit = 40 # limit of reduction steps
$ski_one_step  = true
$ski_apply_symbol = ".."

$ski_opening = "Welcome to Simple SKI Interpreter
commands are
    :q to quit
    :s to show definition identifiers and rules
    :o to toggle one step mode
    :di, :dr to delete an identifier or a rule
    :lim NNN to set limit number of translation
    Identifier := Exp to define an identifier
    Head => Body to define a rule
    Other input is evaluated as an combinator exp\n"

$ski_commands = sop_new_commands( {
  ":clear" => lambda {|input, code|
    $ski_table = {}
    $ski_rules = {}
    printf("  Id(s) and Rules cleared\n")},
  ":reset" => lambda {|input, code|
    $ski_rules = $ski_initial[0].clone
    $ski_table = $ski_initial[1].clone
    printf("  Id(s) and Rules return to originals\n")},
  ":ci" => lambda {|input, code| $ski_table = {}
    printf("  Id(s) cleared\n")},
  ":cr" => lambda {|input, code| $ski_rules = {}
    printf("  Rules(s) cleared\n")},
  ":s" => lambda {|input, code|
    printf("  Definition of combinator(s)\n")
    $ski_rules.each {|u|
      printf("    "); sop_print(u[0], false); printf(" => "); sop_print(u[1]);
    }
    printf("  Definition of identifier(s)\n")
    $ski_table.each {|u|
      printf("     %s := ", u[0]); sop_print(u[1]);
    }
    printf("  End\n")},
  ":o" => sop_gen_toggle("$ski_one_step"),
  :":=" => lambda {|input, code|
    $ski_table[code[1]] = ski_expand(code[2])
    printf("  Identifier %s is defined.\n", code[1])},
  :"=>" => lambda {|input, code|
    $ski_rules[code[1]] = ski_expand(code[2])
    printf("  Rule of '"); sop_print(code[1], false)
    printf("' is defined.\n")},
  :":dr" => lambda {|input, code|
    cname = ski_leftmost(code[1])
    dlist = $ski_rules.select {|x| ski_leftmost(x) == cname}
    dlist.each {|rule|
      printf("  Del "); sop_print(rule[0], false); printf(" => ")
      sop_print(rule[1])
      $ski_rules.delete(rule[0])
    }},
  :":di" => lambda {|input, code|
    $ski_table.delete(code[1])
    sop_print(code[1], false); printf(" is deleted\n")},
  :":p" => lambda {|input, code|
    printf("    ")
    sop_print_tree2(ski_expand(code[1]), 4, $stdout, $ski_apply_symbol)
    printf("\n")},
  :":lim" => lambda {|input, code|
    $ski_limit = code[1].to_i
    printf("  limit set to %d\n", $ski_limit)},
  :":load" => lambda {|inout, code|
    sop_load(code[1].gsub("\"", ""), $ski_commands)},
  :else => lambda {|input, code|
    y = ski_expand(code)
    printf("Evaluation of "); sop_print(y);
    $ski_limit.times {|i|
      y2 = ski_reduce1(y, $ski_one_step)
      if y2 == y then
        break
      end
      printf("%3d: -> ", i); sop_print(y2);
      y = y2
    }
    printf("Value = "); sop_print(y);
  },
})

def top
  sop_top($ski_opening, "Bye\n", "ski> ", $ski_commands)
end

def ski_expand(exp)
  ski_subst(exp, $ski_table)
end

def ski_reduce1(exp, once = false)
  $ski_rules.each {|r|
    exp2 = ski_apply_rule(exp, r)
    if once && (exp2 != exp) then
      return exp2
    end
    exp = exp2
  }
  exp
end

def ski_apply_rule(exp, rule)
  # rule ::= [left, right]
  env = ski_match(exp, rule[0])
  if (env != nil) 
    ski_subst(rule[1], env)
  elsif exp.class != Array then
    exp
  else
    exp.map {|x| ski_apply_rule(x, rule)}
  end
end

def ski_varp(exp)
  exp.class == String && exp[0] == "?"
end

def ski_match(exp, pat)
  if exp == pat then []
  elsif ski_varp(pat) then [[pat, exp]]
  elsif pat.class != Array then nil
  elsif exp.length != pat.length then nil
  else
    env = []
    exp.length.times {|i|
      env2 = ski_match(exp[i], pat[i])
      if env2 == nil then
        return nil
      end
      env = env2 + env
    }
    return env
  end
end

def ski_subst(exp, env)
  if exp.class == Array then exp.map {|x| ski_subst(x, env)}
  else
    if (env.class == Array)
      v = env.assoc(exp)
    else
      if env[exp] then
        v = [:"dummy", env[exp]]
      else
        v = nil
      end
    end
    if v == nil then exp else v[1] end
  end
end

def ski_leftmost(exp)
  while exp.class == Array && exp[0] == :"#apply#" do
    exp = exp[1]
  end
  exp
end

プログラムの変更履歴

上が最近です.

  1. 2019.02.26
    Ver. 0.55 2019.02.26
    簡単な演算子順位法によるパーサー in Ruby の Ver. 0.96 にあわせてプログラムの スリム化.
    :load コマンドの追加.
    :clear, :ci, :cr コマンドの追加.
    :p コマンドの追加
    :dr はコンビネータの名前だけ見るようにした.
    :reset コマンドの追加.

  2. 2019.02.11
    Ver. 0.50 2019.02.11 初出


補足事項

  1. 本プログラムの扱いは,簡単な演算子順位法によるパーサー in Ruby の注意事項に書いてあることと同様とします.


参考文献

コンビネータ論理のまとまった本は少ない思います.

  1. レイモンド・M・スマリヤン : スマリヤン数理論理学講義 下巻, 田中 一之 (監修, 翻訳), 川辺 治之 (翻訳) , 2018
    数少ないまとまった本の一つだと思います.たぶん.

  2. 某勉強会のスライド
    検索語「川辺 治之 コンビネータ論理 PDF」でぐぐると,某勉強会で川辺さんが作られた スライドが見つかると思います.50 スライドくらいで,コンビネータの定義から, 計算可能性,停止性の判定ができないことなどが説明されています.

  3. コンビネータ論理(Combinatory Logic) のお話 - λ式から SKI を使った式への変換のトレース -
    このページと同じレベルにある私のページです.コンビネータの基礎的なことと, コンビネータとλ式の関係を書きました.特にラムダ式からコンビネータの式への 変換方法を書きましたので,「ちょっと動かしてみる」の中にある問題はその知識を 使うと原理的には解くことができます.

  4. Wikipedia の「コンビネータ論理」の項目
  5. Wikipedia の「SKIコンビネータ計算」の項目
  6. Wikipedia の「B,C,K,Wシステム」の項目

  7. Stanford Encyclopedia of Philosophy "Combinatory Logic"
    スタンフォードの哲学辞典の "Combinatory Logic" です.結構,まとまった 内容が書かれています.私のように貧乏で高い本を買えない人はこれで勉強するのでも 一通り勉強できると思います.

  8. Henk Barendregt, Erik Barendsen : Introduction to Lambda Calculus, Revised edition Decenber 1998, March 2000, 53 pages
    たぶん,著者名とタイトルに PDF を加えてぐぐるといくつかの年のものが 見つかると思います.一応,λ計算についての入門書ですが,コンビネータも 一部にでてきますし,自然数の表現と再帰関数の説明は結構分かりやすいです.


計算機(主にソフトウェア)の話題 へ

圏論を勉強しよう へ
束論を勉強しよう へ
半群論を勉強しよう へ
ホームページトップ(Top of My Homepage)