SKI コンビネータのことは，以前，ある程度，
SKI コンビネータのことは，以前，ある程度，
で話したのですが，そこでは動くものを提供しませんでした．先ほど，せっかく，
でパーサを作ったので，これを利用して，本当に簡単なコンビネータのインタープリタを
作って遊ぶのも面白いかなと思います．
下の SKI インタープリタを「ちょっと動かしてみる」の部分は， 試みに， Youtube の説明動画も作りました．約 16分の動画です．動作させる方法を読むのが面倒なときは， こちらをどうぞ．
また，コンビネータはラムダ計算と密接な関係があります．ラムダ計算については
動かして遊ぶλ計算の初歩 in Rubyに詳しく書いていますので，ここを読み終わった後，あるいは，途中にでも， ぜひ，行ってみてください．
ここで作って遊ぶのは，コンビネータの式を入力すると，その式のリダクションを行って結果を 表示するインタープリタです．コンビネータとしては最初から3種類，
というコンビネータが組み込まれています．ここで ?X, ?Y, ?Z など ? で始まる名前は どんな式にもマッチするもので，上の式はマッチした式を => の右側の並びに変えるという 意味を持っています．一応，式の読み方としては左から括弧が付きます．つまり，
X Y Z U V という並びがあれば，(((X Y) Z) U) V という意味
です．本などに載っている コンビネータは１文字で途中に空白を挟まずに書けますが，ここでは文字の間は１文字以上の 空白で区切ってください．その代わりに一文字より長い名前のコンビネータが使えます． 途中に括弧が挟まり，アルファベットが続かないところは空白を 入れる必要はありません．
コンビネータの理論では，この３つのコンビネータだけで，帰納的な関数を記述できると いうことが示されます．ここでは実際に動かしてその雰囲気を味わいましょう．
まずはちょっとだけ動かしてみましょう．
対話的に実行できる 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>
とりあえず，簡易インタープリタの動かし方をざっと説明しました． 最後にも書きましたようにこれだけで，実は，結構遊べますので，適当に いじってみてください．
とりあえず，次の機能を持つコンビネータの式を考えてみるというのはどうでしょう．
以上，ヒントでした．
上の問題の中で最後の式は，先ほどの引数を倍にするコンビネータの式 S I I と組み合わされて， コンビネータの式が帰納的関数の能力を持つことに関連してとても重要です．
そのうち，続きを書くと思います．2019.02.11 (月)
一応，上の４つの問題の解をここに書きました．2021.04.24 (土)
一応，一通り，Simple SKI Interpreter の機能の説明をしておきます．
利用のための環境ですが，Ruby の バージョン 2.3 以降と，対話型インタープリタが あれば利用可能と思います．私は Windows で， irb を使っていますが， Linux でも irb は動いているみたいなので本インタープリタを利用可能でしょう． Mac についてはあまり良く知りませんが，irb はあるようですね．android の ruboto などの 環境では，それぞれの ruby の関数は実行可能なのですが，read-eval loop が書けないので 本ページのプログラムをそのまま利用することはできません．
続いて，起動と終了ですが，Ruby の対話型インタープリタ（irb など）に，
を読み込んだ後，以下に掲載した SKI コンビネータインタープリタの掲載リスト を読み込んで，関数 top を呼び出してください．そうすれば，Simple SKI Interpreter に 入ります．終了するためにはコマンド :q を入れて改行を入れてください．Ruby の インタープリタに戻ります．
Simple SKI Interpreter のコマンドは次の4種類に分かれます．
それぞれについて以下に説明します．
どのコンビネータの適用を最初に行うか，式のどの部分に適用するか など，コンビネータの適用戦略についてはいろいろ議論があるところですが， これについては，プログラムで見つかった順ということで，プログラムを 見たり，改造したりしてみてください．
:di 名前
という形で使います．
:dr コンビネータ名
という形で使います．左辺がコンビネータ名のルールが消されます．
次の形で指定されたコンビネータの式を木の形で表示します．
:p コンビネータ式
関数適用は ".." で表示されます．
例：
ski> :p (S x y z => (x z) (y z))
(=> (.. (.. (.. S
x)
y)
z)
(.. (.. x
z)
(.. y
z)))
コンビネータの式が実際にはどのような構造をしているかを調べるために 便利です．入力の中には関数適用だけでなく，"=>" も使うことができます．
本ツールは無限ループ回避のために，変換回数を制限しています． その制限回数を変更します．
:lim 制限回数
という形で使ってください．制限回数の初期値は 40 です．
端末からコマンドを読み込んで実行する代わりに，ファイルからコマンドを 読み込んで実行します．ファイルの中に xxx := 式 などの列を書いておくと いちいち端末から入力しないで便利です．このコマンドは，
:load ファイル名
という形で使います．ファイル名はダブルクォートで囲んでください．
名前 := コンビネータの式
のような式を入植すると，指定されたコンビネータ式を名前で参照することが できるようになります．名前はアルファベットと数字，アンダーバーの 組み合わせの綴りにしてください．ここで定義した名前はコンビネータ式の入力の ときに使うことができるようになります．
M ?X => ?X ?X
とすると，与えられた引数を二つ並べるコンビネータが定義できます． これは S, K, I を使って表すと，S I I に相当するものですね． コンビネータを定義するとき，引数は ? で始まる名前にして全部異なるように してください．つまり，
Comb ?X ?X => S S K ?X
などとしないでください．特にチェックはしていませんので間違えた場合は 上で説明したコマンド :dr で消してから入れなおしてください．
ここではコンビネータ論理の，ほんの基礎部分だけを書いておきます．本格的に説明するのは 私の能力では無理だからです．ご興味のある方は， 参考文献に挙げたコンビネータ論理の成書を当たってみてください．
そこで，去年（2018年），某勉強会に行ったとき，某 KWB 大先生に教えて もらったことをベースに自分流に書いてみます．お金のある人は，ぜひ， 参考文献にある本を買って正確な定義を 調べてみてください．
集合 C の二つの元 x, y に集合 C の元 (xy) が
対応させられているとき，集合 C を
この定義内の (xy) で x と y の間には二項演算子が省略されているとみることが
できますから，この定義は，C には二項演算が定義されていて，Cの要素を
コンビネータというと言っているにすぎません．今日的にはこのように二項演算の
定義された集合は
このような用語を使うと，適用系とはマグマで，その元をコンビネータというという ことですね．
マグマで一番単純なマグマは
計算機屋さんになじみの深いものとしては，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 の要素をコンビネータとよび，それ以外の演算を含んだ式は コンビネータの式と呼ぶことにします．ここらあたりは，このページにローカルな 呼び方なのですが，ご容赦ください．
補足：λ計算の読み物などを読むと，「コンビネータとは，閉じた（即ち， 自由変数を持たない）λ式である」という定義もあります．
まず，それぞれのルールですが，以下の通りです．
I は，S と K で作ることができますし，単純なので説明を省略します．
K は，役割的に考えると，二つの捉え方ができます．一つは真偽値の 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 になりました．ちなみに，-> は「変換される」 を表すことにします．
S ?f ?g ?x => (?f ?x) (?g ?x)
と書けば雰囲気がでるでしょうか．
プログラミング言語やλ計算では，関数はパラメータを持つことができ，実際の 関数呼び出しでそのパラメータにもらった引数の値は，パラメータの名前で 関数の処理の色々な場所に分配され，使われます．このとき，パラメータの名前が 問題になることがしばしばあります．皆さんは，静的なバインディングと動的な バインディングがしばしば，プログラミングのミスを誘発することをご存知でしょう． 古くは LISP で Funarg 問題と呼ばれる問題が発生することもありました． コンビネータ論理ではパラメータがありませんので，この問題が起こりません． その代わり，S のようなコンビネータで，引数をプログラム（あるいはコンビネータの 式）のあちこちに届けてやる必要があります．S はこのメカニズムを提供します．
後の説明にも使いますので，次のλ記法を覚えておいてください．これは， λ計算のごくごく簡単な部分だけです．
λx.E はなにか x をとって，それを E の中の x に 代入したもの E' を返す関数を表す．いま，λx.(E1 E2) という式を別の式 E に適用することを考えます． λ計算の計算メカニズムがかれば，E1 と E2 の中の x が表れるところに E を代入するということができますが，コンビネータ論理にはこのような パラメータのメカニズムはありません．その代わりに，コンビネータ S で E1 と E2 に E を届け，(E1 E) (E2 E) という式を作り，E1, E2 にそれぞれ， E を取り込んで使ってもらうようにすることで，パラメータのメカニズムを 実現しようというものです．例として，(λx.(K x)) (S I) は K (S I) になります．
(S I I) は貰った引数を二つにするコンビネータの式でした．これは，S が x を それ自身を返すコンビネータ I 二つに x を分配している訳です．二つに分配できるなら それをもう一つ使えば３つに分配することも可能です．つまり，(S F I) x が (F x) x ですから F を x を二つに増やすコンビネータ式にしてしまえばよい訳です， これは前の節で出した問題のうちの１つのヒントです．
なぜ重要かと言いますと，この二つを使うことにより
E -> F E
となることを言います．不動点演算子 Fix とは Fix F が F の不動点と なるようなコンビネータのことです．つまり，
(Fix F) -> F (Fix F)
となります．このような Fix を M と B を組み合わせて作ることができます． どうやったら良いでしょう．これはとりあえず，問題にしておきます． → こちらに，「ほぼ答え」があります．
なお，Fix F を Simple SKI Interpreter に入れると止まりません． でも，回数制限がありますから，いくつか試してみると良いでしょう．
これらの演算は 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) を実現すればよいですね
S, K, I がチューリングマシンと同等の能力を持つことを確信するためには，
つまり，再帰関数がこれで記述できることを確信するには，まずは，再帰関数の
計算対象である自然数を模擬する体形を S, K, I で構築しなければなりません．
自然数を表す方法は色々なものがあるようですが，その中で２つの方法が主流だそうです．
それらは，チャーチ（Alonzo Church）流の自然数とバーレンットレクト（Henk Barendregt）と
Barendsen の教科書 Introduction to Lambda Calculus [Barendregt]
に書いてあるものです．ここではまず，後者，バーレンットレクト（Henk Barendregt）らの
教科書に書いてあるものを少し
これは考え方はかなり単純ですが，SKI だけでやっていると，その単純な考え方が
見えてこないことがありますので，まずは，考え方を理解するために，SKI に
こだわらないでやって，あとで，それらが SKI で実現できることをお話します．
まず，準備として，次のような関係をもつコンビネータの集まり
ここで XXX -> YYY は，0回以上の変換で XXX が YYY に変換されることを表すとします．
これはぶっちゃけ，LISP の cons, car, cdr ですね．
これらは，次のようなコンビネータの変換式を定義しておくと実現できます．
K x y -> x ，つまり最初の要素を返し，(K I) x y -> I y -> y， つまり，２番目の要素を返すことを思い出してください．また，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) があって，それを n 個の (pair false -) が取り囲んでいます．木の形で書けば，
です．
この形を理解してしまうと， 0 かどうか調べるコンビネータの式 is_zero， 1 加える add1，1 引く sub1 はすぐできると思います．
一応，確認しましょう．
まず，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 のコンビネータを作ってみます．ズルというのは， じつは，ここで作ったコンビネータのインタープリタは再帰的な定義が 可能になってしまっていたのです．
足し算を再帰で書くのは，Ｃ言語っぽく書くと，
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 は，変換過程を１つのコンビネータのルールの適用ごとでなく，
全部を一通り適用したごとに表示するモードにします．
ski> :o
one step mode = false
一番基本的なケースは第１引数が 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 のコンビネータ表現です．
次は第１引数が１の場合をやってみます．
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 の数が３個ですから確かに 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 ?x ?y ?z => ?z ?x ?y
という働きをし，S, 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 がちょっと面倒になります．特に私は新たな方法を提案するつもりはないので， ものの本を読むときに，そちらの流儀に従ってください．
ここではチャーチ流の自然数の表現方法に関する基礎的な知識をいくつか述べます． しかし，私もあまり知らないので，これについては深入りはしません．ご興味の ある方は成書で調べてください．
自然数 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 = K I, X_1 = I, X_2 = (S B) I, X_3 = (S B) [2] = (S B) (S B I), ...
になります．
つまり，+ 1 をとる操作が (S B) ですね．
この表現は足し算や掛け算が簡単に書けます．
(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 回適用したことになります．
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 回適用することになる訳です．
S (S I (K (K false))) (K true)
があります．
自然数 n の表現 X_n は，関数 f とデータ x をとって，x に f を n 回適用して返す 関数ですが，最初の１回を適用しないように工夫すれば，f を n-1 回適用する関数， すなわち，X_(n-1) が出来ます．
この方法には関数を使うもの，pair を使うものなどいろいろあるようですが，ここでは pair を使う方法を示します．ここで pair は先にバーレントレクトの亜流の自然数表現を 説明した時出てきたものです． 1st (pair x y) = x, 2nd (pair x y) = y という 性質をもったコンビネータです．
つまり，最初に第１成分を false，第2成分を x にしたペア x2 を作り， f2 は第１成分が false なら true と第２成分を pair にしたものを返し， そうでなければ，第２成分に f を適用し，それを第２成分，第１成分は true の pair を返します．そうして，X_n を使って，f2 を x2 に n 回適用すると， 最初の１回だけ，f の適用がないので，f が n-1 回適用された結果を 第２成分に持つデータができます．最後に，その第２成分を返せばよいわけです．X_(n-1) の動作 与えられた関数とデータを f と x とします．
- x2 = pair false x
- f2 = λu.(if 1st u = false then (pair true (2nd u))
else (pair true (f 2nd u)) end)
- result = X_n f1 x2
- return (2nd result)
この節のはじめでも注意として述べましたが，このような，1を減ずる方法を 導入すると，この表現方法では，自然数の同等性の 判定が形の上からだけではやりにくいと思われます．
上の自然数の表現のところでは，足し算 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 で実現できることを示しておきましょう．
一応，上の二つをインタープリタにコピー＆ペーストして実際に要求通りの式に
なっていることを確認しておきましょう．
: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 の
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.56 2022.08.07
# Ver. 0.55 2019.02.26
# Ver. 0.50 2019.02.11
$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
:l2c [-d] [Identifier=]LambdaExp to convert the lambda exp to SKI exp
: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
###############################################################
# lambda expression -> SKI combinator 2022.08.07
$sop_ops[:"."] = [".", 1250, :xfy] # note that it is less than " "
$sop_ops[:":l2c"] = [":l2c", 4500, :fy]
$ski_commands[:":l2c"] = lambda {|input, code|
exp, result, var = nil, nil, []
$verbos_l2c = false
if code[1].class != Array then exp = ski_expand(code[1])
elsif [:"=", :":="].index(code[1][0]) then
if code[1][1].class != Array then var = code[1][1]
elsif code[1][1][0] == :"#apply#" then
$verbos_l2c = true
var = code[1][1][2]
else
printf("Syntax error\n")
exp = :error
end
exp = ski_expand(code[1][2])
elsif code[1][0] == :"#apply#" then
if code[1][1] == [:"-/pre", "d"] then
$verbos_l2c = true
exp = ski_expand(code[1][2])
else
exp = ski_expand(code[1])
end
else
exp = ski_expand(code[1])
end
result = ski_l2c(exp)
if var != [] then $ski_table[var] = result end
sop_print(result)
}
# Lambda term to SK combinator
# Wikipedia Combinator Logic
# T(x) => x
# T((E1 E2))=> (T(E1) T(E2))
# 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.(E1 E2)) => (S T(λx.E1) T(λx.E2))
def ski_l2c (term, depth = 0)
reason = ""
ski_indent_and_print(depth, "<- ", term, reason)
if term.class != Array then
reason = "t(u) = u"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = term
elsif term[0] == :"#apply#" then
# Application
reason = "t(A B) = t(A) t(B)"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = [:"#apply#", ski_l2c(term[1], depth+1), ski_l2c(term[2], depth+1)]
elsif term[0] == :"." then
# [:".", <Var>, <Lambda Term>]
if !ski_is_free_in(term[1], term[2]) then
reason = "t(u.A) = K t(A) :when u not free in A"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = [:"#apply#", "K", ski_l2c(term[2], depth+1)]
elsif term[1] == term[2] then
reason = "t(u.u) = I"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = "I"
elsif term[2][0] == :"." then
reason = "t(u.v.A) = t(u.t(v.A)) :when u free in v.A"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = ski_l2c([:".", term[1], ski_l2c(term[2], depth+1)], depth+1)
else
reason = "t(u.(A B)) = (S t(u.A) t(u.B))"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = [:"#apply#",
[:"#apply#", "S", ski_l2c([:".", term[1], term[2][1]], depth+1)],
ski_l2c([:".", term[1], term[2][2]], depth+1)]
end
else
# general expression ... not supported
reason = "is not a lambda expression"
if $verbos_l2c then printf(" [ %s ]\n", reason) end
result = [:"#apply#", "K", term]
end
ski_indent_and_print(depth, "-> ", result, reason)
result
end
def ski_is_free_in(var, term)
if term.class != Array then
var == term
elsif term[0] == :"#apply#" then
ski_is_free_in(var, term[1]) || ski_is_free_in(var, term[2])
else
# term is [:".", var2, term2]
if var == term[1] then
false
else
ski_is_free_in(var, term[2])
end
end
end
def ski_indent_and_print(depth, symbol, exp, reason)
if $verbos_l2c then
printf(" ")
depth.times { printf("| ") }
printf("%s", symbol)
sop_print(exp, false)
if reason != "" then printf(" [ %s ]\n", reason) end
end
end
上が最近です．
でも，動かないものの話ではつまらないので，実際に，SKI コンビネータの式が動く，こちらの プログラムに，あちらの「ラムダ式から SKI コンビネータ式への変換トレース機能」だけ実現して みました．
ということで，Ver. 0.56 2022.08.08 から，ここのプログラムで，次のコマンドが使えるように なりました．
ラムダ式を SKI のコンビネータの式に変換します．コマンドの書式は次の通りです．
:l2c [-d] [識別子=] ラムダ式与えられたラムダ式を等価な SKI のコンビネータの式に変換します．-d オプションを付けたときは その変換の過程を表示します．「識別子=」が付けられた場合は，変換した結果をその識別子の値として束縛し，入力のとき使えるようにします（:= コマンドと一緒）．= の代わりに := も使えますが，シンタクスをもとのページのものと合わせました．
ラムダ式の書き方は， 「コンビネータ論理（Combinatory Logic） のお話 - λ式から SKI を使った式への変換のトレース - 」 や 動かして遊ぶλ計算の初歩 in Ruby に書いてある書き方に準じます．つまり，ラムダ式からλを取り去った表記です．
例えば，λx.λf.(f (x x)) は x.f.(f (x x)) です．
下のトレースに出てくる
[ t(u.(A B)) = (S t(u.A) t(u.B)) ]などは，ラムダ式から SKI の式へ変換する方法を表します．t(Exp) が，λ式 Exp を SKI コンビネータの式に変換したものを表しています．したがって，この例は，u.(A B) を 変換するときは，コンビネータ S を一番前において，次にu.A を変換したもの（t(u.A)）， そして，u.B を変換したもの（t(u.B)）を置くことを表しています．
ski> :l2c x.(x x)
S I I
ski> :l2c -d x.(x x)
<- x.(x x) [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
| <- x.x [ t(u.u) = I ]
| -> I [ t(u.u) = I ]
| <- x.x [ t(u.u) = I ]
| -> I [ t(u.u) = I ]
-> S I I [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
S I I
ski> :l2c -d xxx=x.(x x)
<- x.(x x) [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
| <- x.x [ t(u.u) = I ]
| -> I [ t(u.u) = I ]
| <- x.x [ t(u.u) = I ]
| -> I [ t(u.u) = I ]
-> S I I [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
S I I
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)
xxx := S I I
End
ski> xxx a
Evaluation of S I I a
0: -> I a (I a)
1: -> a a
Value = a a
ski> :l2c yyy=x.(x x x x)
S (S (S I I) I) I
ski> yyy a
Evaluation of S (S (S I I) I) I a
0: -> S (S I I) I a (I a)
1: -> S I I a (I a) (I a)
2: -> I a (I a) (I a) (I a)
3: -> a a a a
Value = a a a a
コンビネータ論理のまとまった本は少ない思います．
本文中にあげた練習問題の解を書きます．以下，どれも， K が定数関数を作る作用
(K Const) x → Const
があるということと，S f g は，次に与えらえた引数 x を f と g に分配する
(S f g) x → (f x) (g x)
ということを思い出して読んでください．
S (S I I) I x → ((S I I) x) (I x) → (x x) x = x x x
つまり， (S (S I I) I) が一つの解です（解は沢山あるでしょうから）．
一応，インタープリタで確かめます．
ski> (S (S I I) I) x Evaluation of S (S I I) I x 0: -> S I I x (I x) 1: -> I x (I x) (I x) 2: -> x x x Value = x x x
はい，うまく行きました．
F x y → S I (K x) y → (I y) ((K x) y) → y x
となるわけですから．したがって，F = S (K (S I)) K とすれば，
F x = S (K (S I)) K x → ((K (S I)) x) (K x) → (S I) (K x)
となります．従って，一つの答えは
S (K (S I)) K
です．一応，インタープリタで確かめておきます．
ski> S (K (S I)) K x y Evaluation of S (K (S I)) K x y 0: -> K (S I) x (K x) y 1: -> S I (K x) y 2: -> I y (K x y) 3: -> I y x 4: -> y x Value = y x
はい，うまく行きました．
したがって，式 x y z → S (S x y) z に なる式を探せばよいわけです．
それには，式 x y → S (S x y) となれば 良いわけです．
それには，式 x → S (K S) (S x) になれば良いのです．つまり，式を
S (K (S (K S))) S
とすれば良いはずです．インタープリタで確かめてみましょう．
ski> S (K (S (K S))) S x y z u Evaluation of S (K (S (K S))) S x y z u 0: -> K (S (K S)) x (S x) y z u 1: -> S (K S) (S x) y z u 2: -> K S y (S x y) z u 3: -> S (S x y) z u 4: -> S x y u (z u) 5: -> x u (y u) (z u) Value = x u (y u) (z u)
はい，うまく行きました．
ということで，式 x → S (K x) になればよく，式は
S (K S) K
で良いことになります．インタープリタで確かめてみましょう．
ski> S (K S) K x y z Evaluation of S (K S) K x y z 0: -> K S x (K x) y z 1: -> S (K x) y z 2: -> K x z (y z) 3: -> x (y z) Value = x (y z)
はい，うまく行きました．
計算機（主にソフトウェア）の話題 へ
圏論を勉強しよう へ
束論を勉強しよう へ
半群論を勉強しよう へ
ホームページトップ(Top of My Homepage)