コンビネータ論理(Combinatory Logic) のお話

λ式から SKI を使った式への変換のトレース

by Akihiko Koga
13th Sep 2018 (Update)
20th July 2018 (First)
計算機(主にソフトウェア)の話題 へ
ホームページトップへ戻る

目次

1. 概要

一か月ほど前(2018年6月20日(水)),とある勉強会でコンビネータ論理を教えてもらった. その勉強会は,
SKI のコンビネータで帰納的関数が表現できることを示して, コンビネータ論理の真な等式の集合は計算可能でないことを示す
という内容だったのだが, その予習として Wikipedia などを調べて,コンビネータの式のインタープリタと ラムダ式からSKIを使った式への変換機能を Ruby で組んでみた.そのとき作ったλ式から SKI コンビネータの式への変換プログラムは変換の過程(トレース)を出すようにしていたのだが, その出力が結構分かりやすいと思ったので,ここにいくつかログを載せておく.

補足: 簡単なコンビネータのインタープリタを提供することにした.詳しくは SKIコンビネータ AGAIN を参照されたい.あちらはコンビネータの理屈はあまり書いてなく, ただ動かしてみて遊ぶというものなので, こちらで勉強して,あちらで実際に動かしてみると言うのが良いと思う. 2019.02.11 (月)

2. 予備知識

SKI コンビネータの定義などいくつかの予備知識を書いておく.
  1. SKI コンビネータの定義
    S, K, I のコンビネータは,それらを使った式の中で,それぞれ次の等式の左から右へと 表現を変換する機能を持っている.コンビネータの式は括弧を省略すると左から 括ることになっているらしい.コンビネータは次の引数1個に作用する.複数の引数を 持った関数を表現したいときには,いわゆる,カーリー化で対応する.つまり, f が 二つの値の組 (x, y) に適用される関数を意図している場合には, (f x) y のように2段階で適用するのだ(まず,(f x) で y の領域に作用する関数ができると考えて,(f x) y で,それを y に作用させると考える).

    変換式は何段階かの適用の形で表現される場合が多い.若干,先ばしることになるが, ((S x) y) z という形が現れたら,それを (x z) (y z) に置き換えてよいなどである.

    コンビネータの間の空白は普通書かないらしい.ここでは,私が予習でコンビネータの インタープリタを作ったときの都合で,普通省略される括弧も空白も書くことが多い.

  2. λ式
    SKI のコンビネータ式で遊んでみる前に,λ式について説明しておく.大雑把に いうとλ式は数学的表現において関数を明示して表す式である.例えば,x2 + y2 という式があったとき,これはある x と y という値があって, そのときの x2 + y2 という値を表しているのか,あるいは,x と y をとって, x2 + y2 を返す関数を表しているのか,あいまいである(つまり, 単なる値なのか,あるいは,関数なのか,関数の時はどれがパラメータなのかが 曖昧である).λ式では, もし,これが関数である場合は,関数の引数を明示して,λx.λy.(x2+ y2) と 書く.λは単に,次に書く文字がパラメータだということを表す記号である.ここでもコンビネータと同じように引数は1個として,複数書きたいときは何段階か 重ねて書く(もちろん, λ(x, y).(x2+ y2) というように直積をパラメータにするという拡張を許すと いうこともできるが,ここでは簡単に1引数だけにしておく).こういう関数を 明示的に書く記法をλ記法,そのように書かれた式をλ式という.これは数学一般では あまり使われておらず,文脈により,同じ表現が関数や値として解釈されている. 私は,数学一般にも導入したらよいと思うのだが,あまり使っている人を見ない.

    次に,少し形式的にλ式を定義しておく.

    ラムダ式の集合Λ
    可算無限個の変数記号の集合 V が与えられているとする.このとき,λ式を次のように 定義する.

    1. x ∈ V のとき,x はラムダ式である.
    2. Exp がラムダ式で,x ∈ V ならば (λx.Exp) はλ式である.
    3. Exp1 と Exp2 がラムダ式なら, (Exp1 Exp2) はラムダ式である.
    4. 上記3つの方法で作られたものだけがラムダ式である

    括弧は省略することができて,その場合はコンビネータと同様左から結合される. 例えば, (λx.f x y) u v は ((λx.((f x) y)) u) v) を表す.

    λ式の作り方のルール2 は関数を作るルールで,ルール 3 は関数の適用を表している. 従って,意図としては,例えば

    (λx.f x) (g y) = f (g y)

    のように,左辺の意味は,一番目の式のλで指定された変数のところに, 2番目の式を代入した式を表している.こういう左辺から右辺への変換を β変換と言う.λ式の意味は,こういうβ変換を繰り返していって, もう変換できない式になったら,それがもとの式の意味であるとする.β変換の とき,λの次の変数名が複数の式の間で同名で不都合が起きることがある. それを避けるために,λ式の計算では,λx.Exp は,x を別の名前,例えば,yを 用意し,Exp の中の x も全部 y に変えたものを Exp' としたとき,ラムダ式 λx.Exp を λy.Exp' に変えてよいというルールがある.このルールを α変換という.このα変換も,Exp で使われている別の変数名と 被ってしまってはいけないなどの細かなルールがあるのだが,ここではそこまで 詳しく述べない.λ式の計算では,このα変換とβ変換の繰り返しを計算と みなすのである.こんなシンプルな計算規則で,λ計算はチューリングマシンと 同等の計算能力がある.つまり,コンピュータと同等である.まったく不思議な 話だと思う.

    先のコンビネータ S, K, I は次のようにλ式で表される.


    まあ,定義そのままだ.ちなみに,λx.λy.λz. などλの列は,λxyz. のように 省略されることがある.

  3. SKI の式に慣れる
    ここでは,SKI のコンビネータの式に慣れるとともに,λ式との関係のいくつかに 触れておこうと思う.
    1. I = λx.x ... again
      I が ((S K) K) と同じ機能であることは先に天下り式に述べたが,今度は, これを何とか導き出してみよう.まあ,S, K の中では有望そうなのは S なので, 求めるものは (S Exp1 Exp2) の形だと仮定してみよう.そうすると

      (S Exp1 Exp2) x = (Exp1 x) (Exp2 x)

      これが x になるようにするには,Exp1 を K にすればよい.Exp2 が何でも

      (K x) (Exp2 x) = x

      になってしまう.ということで, S K K, S K S, S K (K K), ... これらはみんな I と同じ機能のコンビネータ式である.

    2. false
      コンビネータ K が if true then x else y のような意味を持っていることは, K の定義の時に述べた.では,if false then x else y に対応するコンビネータの 式は作れるだろうか?

      つまり,(A x) y = y となるコンビネータ A を S, K, I の組み合わせで作れる だろうかという問題である.それには,コンビネータ S について,

      ((S u) x) y) = (u y) (x y)

      であることと,K のもう一つの機能,つまり,第1引数を抱え込んで何が与えられても それを返すという機能に着目すれば,u を K と置けばよい.つまり,

      ((S K) x) y => (K y) (x y) => y

      で,(S K) が false として要求される機能を持つ式である.

      もう一通り,この false に相当する SKI コンビネータ式の求め方を書いておく. この false はλ式で書くと,

      false = λx.λy.y

      である.この中の式 λy.y は, I である.したがって,

      false = λx.I

      となる.これは何が来ようと I を返す関数なので,K の説明の2番目の機能から,

      false = K I = K (S K K)

      とも書ける.

    3. not
      not の後ろには true と false しか来ないとする.not は true に対して false を返し, false に対しては true を返すコンビネータの式である.コンビネータとλ式を混ぜて書くと,

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

      言い換えれば

      not x = (x false) true

      である.not の後ろに与えられた x を前の方の (x false) にもっていく必要がある. このようなことが出来るコンビネータとしては,S があった.

      (S Something λu.true) x = (Something x) ((λu.true) x)

      = (Something x) true

      λu.true は定数関数だから,(K true) とやればよい. 後は,

      Something x = x false

      になる Something を求めればよい.これも S を 使えば,

      Something x = (S I λu.false) x = (I x) ((λu. false) x) = x false

      まとめると

      not = S (S I (K false)) (K true) = S (S I (K (K I))) (K K)

      となる.せっかく,インタープリタを作ったので,not を実行させてみよう.

      SKI> not
       =>     (S ((S I) (K (K I)))) (K K)      # not   の定義
      SKI> true
       =>     K                                # true  の定義
      SKI> false
       =>     K I                              # false の定義
      SKI> not true                            # not true を評価
       =>     ((S ((S I) (K (K I)))) (K K)) K
       =>     (((S I) (K (K I))) K) ((K K) K)  # KがSにより2つの式に取り込まれた
       =>     ((I K) ((K (K I)) K)) K
       =>     (K (K I)) K
       =>     K I                              # K I = false になった
      SKI> not false                           # not false の評価
       =>     ((S ((S I) (K (K I)))) (K K)) (K I)
       =>     (((S I) (K (K I))) (K I)) ((K K) (K I))
       =>     ((I (K I)) ((K (K I)) (K I))) K
       =>     ((K I) (K I)) K
       =>     I K
       =>     K                                # true = K になった

      以上,ちょっと長かったが,引数の分配機能を持つ S と定数関数を作る K を うまく組み合わせることで望む機能を持つコンビネータ式ができた.

    4. or x y
      これは分かるだろうか?2つの if 文の組み合わせで考えれば良い.

      or x y = if x then true else (if y then true else false)

      である.後ろの if 文は,y が true, false だけのときは I で良い.(or x) は,x = true のときは,y に何が来ても true を返し,x = false の時は,y を返す関数を表す式,つまり,(x (K true) I) を返せばよい.

      or x = x (K true) I = (S (λu.(u (K true))) (K I)) x

      λu.(u (K true)) = S I (K (K true))

      ということで,

      or = (S (λu.(u (K true))) (K I)) = (S (S I (K (K true))) (K I)) これもインタープリタでいくつか実行結果を確かめておこう.もう,あまり詳細を 追って行くことに意味はないかもしれないので,結果の確認と,もしかしたら 興味のある部分のトレースのためである.

      SKI> :let or=(S (S I (K (K true))) (K I))      # or を定義
      SKI> or true false
       =>     (((S ((S I) (K (K K)))) (K I)) K) (K I)
       =>     ((((S I) (K (K K))) K) ((K I) K)) (K I)
       =>     (((I K) ((K (K K)) K)) I) (K I)
       =>     ((K (K K)) I) (K I)
       =>     (K K) (K I)
       =>     K                                      # or true false = K = true
      SKI> or false true
       =>     (((S ((S I) (K (K K)))) (K I)) (K I)) K
       =>     ((((S I) (K (K K))) (K I)) ((K I) (K I))) K
       =>     (((I (K I)) ((K (K K)) (K I))) I) K
       =>     (((K I) (K K)) I) K
       =>     (I I) K
       =>     I K
       =>     K                                      # or false true = K = true
      SKI> or false false
       =>     (((S ((S I) (K (K K)))) (K I)) (K I)) (K I)
       =>     ((((S I) (K (K K))) (K I)) ((K I) (K I))) (K I)
       =>     (((I (K I)) ((K (K K)) (K I))) I) (K I)
       =>     (((K I) (K K)) I) (K I)
       =>     (I I) (K I)
       =>     I (K I)
       =>     K I                                    # or false false = K I = false

    5. exchange x y = y x
      二つの引数を交換するコンビネータである.これを作るためには,S が引数を 二つの関数に分配,K が定数関数を作れることを思い出すと,y の前までの式 (exchange x) までが,((S I) (K x)) に評価されれば良い.

      ((S I) (K x)) y = (I y) ((K x) y) = y x

      また,S の分配機能と K の定数関数を作る機能を考えれば,

      exchange x = (S (K (S I)) K) x = ((K (S I)) x) (K x) = ((S I) (K x))

      と出来た.まとめると

      exchange = (S (K (S I)) K)

      である.

    6. M x = x x
      最後に,重要なコンビネータ M を作ってみる.一つの式を二つに増やす訳だが, これは不動点(与えられたコンビネータ式 F に対して,X = F X となるようなコンビネータ式 X)と いうものを作るときに役に立つ.

      引数を2つの関数に分配する S を使って出来そうな 感じがする.で,その分配される関数を恒等関数 I にしてしまえば良い訳だ.

      (S I I) x = (I x) (I x) = x x

      ということで出来た.(S I I) に (S I I) を適用すると,

      (S I I) (S I I) = (S I I) (S I I)

      と,まったく同じものができるため,止まらなくなる.

      このように S, K, I のコンビネータを組み合わせて色々な機能のコンビネータ式を 作ることができる.ここではブール値 true, false をある形にきめて,論理演算, not や or を作ってみたが,一般に,自然数の形を決めて,再帰関数の機能を 持つコンビネータ式を作ることができる.これらに興味のある人は後ろにあげた 参考文献などを参照してほしい.

  4. ラムダ式からSKIコンビネータの式への変換規則
    λ式に何ができるかというと,
    1. 関数適用 (Exp1 Exp2)
      Exp1 が,λx.Exp の形をしているときは,Exp2 を Exp の中の x に ばらまくことができる.

      x を Exp2 の中の色々なところに書くことに寄って, Exp2 をそこに代入できる機構は便利なのだが,変数名をうまく定めないと 違う意味で同じ名前が現れて紛らわしい.これは実際にプログラミング言語の 実装のときも問題になる.一方,コンビネータの方はパラメータを使わず, S で複数の箇所にばらまく.これは望みの場所に持っていくのに苦労は するが,パラメータ名の衝突の心配がない.ラムダ式とコンビネータ論理は このような長所・短所がある.

      この引数を Exp1 にこの λx の構造がないときは単に 関数適用したという事実を表しているだけである.

    2. 関数抽象化 λx.Exp
      これは,x をもらって,Exp を返す関数を作る機能を提供するが, Exp の中に x が現れなければ,単に定数 Exp を返す関数である. x が現れても,それが別のλx に束縛されていれば,ここでの x とは 無関係なので定数と思って良い.例えば,λx.(λx.x) は,何か引数を 受け取ると,定数関数 λx.x を返す関数である.

      Exp に x が現れる一番簡単な形は,λx.x でこれは恒等関数, コンビネータで言えば I である.

      その他の場合としては,Exp が関数適用の形になっている場合と,さらに 他のλyが現れる場合である.

    一方,SKI コンビネータで何ができるかというと,

    1. 関数適用 (Exp1 Exp2)
      [これは,SKI というよりコンビネータ論理の元々の機構]
    2. S コンビネータによる引数の分配
      (S Exp1 Exp2) Exp3 = (Exp1 Exp3) (Exp2 Exp3)

    3. K コンビネータによる定数関数の実現
      (K Exp) x = Exp

    4. I コンビネータによる恒等関数の実現(これはおまけ)

    さて,いよいよ,λ式から SKI コンビネータ式への変換ルールを述べる.これは λ式の構造に従って,ルールを与える.順番は上と逆になるが,λx.Exp の形の ラムダ式から変換ルールを与えていく.以下で,trans(Exp) はλ式 Exp を コンビネータの式に変換した結果を表すとする.
    1. λx.Exp の形のλ式
      1. Exp に x が現れないとき(正確には,Exp に x がフリーに現れないとき)
        (これは x が Exp の中で現れても,λx.(...x...) のように別のλx に 束縛されている場合も含む.こういう,別のλで束縛されていない 現れ方をしているとき「変数 x は式 Exp の中で フリーに(自由に)現れる」という)
        この時は,すでに何度も見たように,K の定数関数を作る機能を使って

        K trans(Exp)

        とすればよい.ここで trans(Exp) は,λ式 Exp を SKI のコンビネータ式に 変換した結果である(すでにこのことは言ったのだが,重要なことなので もう一度言う).ルールとして書いておくと,

        x が Exp でフリーに現れない場合(Exp が x に依存しないとき)

        trans(λx.Exp) = (K trans(Exp))

      2. Exp が x のとき(つまり λx.x)
        このときは,I に変えればよい.ルールとしては

        trans(λx.x) = I

      3. Exp がλy.Exp1 の形のとき(Exp1 には x はフリーに現れる)
        全体のλ式の形は,λx.λy.Exp1 である.これは,λy.Exp1 を SKI の式に変換したものの中に現れる x に,与えられた引数を分配する 式と考えられる.したがって,ルールと しては,

        trans(λx.λy.Exp1) = trans(λx.trans(λy.Exp1))

        となる.

      4. Exp が (Exp1 Exp2) の形のとき(つまりλx.(Exp1 Exp2) の変換)
        これは

        (λx.(Exp1 Exp2) Exp = (λx.Exp1 Exp) (λx.Exp2 Exp)

        であることを考えれば,S を使った式に変換できることが容易に分かると 思う.

        trans(λx.(Exp1 Exp2)) = (S trans(λx.Exp1) trans(λx.Exp2)

        である.

    2. (Exp1 Exp2) の形のとき
      この場合は,

      (trans(Exp1) trans(Exp2))

      に置き換えればよい.ルールとしては

      trans((Exp1 Exp2)) = (trans(Exp1) trans(Exp2))

      である.

    3. 束縛されていない変数の場合
      完全にフリーな変数が現れない場合は,このケースは出てこないが, 一応ルールを与えておく.これはこのままにしておけばよい.

      trans(v) = v

    本当は変換の例題を与えるべきなのかもしれないが,次の変換トレースのところで しっかり変換を追って行くことにして,ここはこれで終わる.

3. λ式から SKI コンビネータ式への変換のトレース

ここでは Ruby で作成した SKI コンビネータ式のインタープリタ&ラムダ式からの SKI コンビネータ式への変換ツールのログを見ながら,コンビネータとλ式との 関係を見ていく.

3.1 Simple SKI Interpreter ことはじめ

まず,Ruby の対話型インタープリタ irb を起動し,SKI インタープリタを読みこんで, それを起動する.

C:\> irb
irb(main):001:0> load "ski.rb"
=> true
irb(main):002:0> top

    +-------------------------------------------------+
    |        Welcome to Simple SKI Interpreter        |
    |                                                 |
    |               written by Akihiko Koga           |
    |               Ver. 0.51 June 19th, 2018         |
    +-------------------------------------------------+

Please type a combinator expression or a command (:help for help)
SKI>

雰囲気も出したいので,起動する部分から表示した.見事に CUI (Character-based User Interface) のツールである.

ここに適当に SKI コンビネータで書いた式を入力すると,SKI の 定義に従って計算していく(つまり, S, K, I の定義を適用していく).

まず,S, K, I の定義を思い出すために,それぞれの定義そのものの変換をさせてみた. このツールはコンビネータ式を読み込むと,それを次々にコンビネータの定義に従って変換して いき,その過程を => でつないで表示していく.

SKI> S x y z
 =>     ((S x) y) z
 =>     (x z) (y z)
SKI> K x y
 =>     (K x) y
 =>     x
SKI> I x
 =>     I x
 =>     x

少し複雑なものをやってみよう.

SKI> S K K x
 =>     ((S K) K) x
 =>     (K x) (K x)
 =>     x
SKI> S K I x
 =>     ((S K) I) x
 =>     (K x) (I x)
 =>     x
SKI> exchange
 =>     (S (K (S I))) K
SKI> exchange x y
 =>     (((S (K (S I))) K) x) y
 =>     (((K (S I)) x) (K x)) y
 =>     ((S I) (K x)) y
 =>     (I y) ((K x) y)
 =>     y x
SKI> S I I x
 =>     ((S I) I) x
 =>     (I x) (I x)
 =>     x x
SKI> (S I I) (S I I)
 =>     ((S I) I) ((S I) I)
 =>     (I ((S I) I)) (I ((S I) I))
 =>     ((S I) I) ((S I) I)
*** Cycle detected

まず,最初のS K K だが,これは I と同じ機能を持つことを準備のところで述べた. 実際に, (S K K) x とやってみると,確かに x になる.この3番目の K は他に変えても, I のままである.例えば,(S K K) x の代わりに (S K I) x とやっても,結果は x になる.

このシステムは,コンビネータの式に名前をつけることができる.名前 exchange は, (S (K (S I))) K と定義してある.これも準備のところで述べた rxchange x y = y x を満たす コンビネータの式である.実際にやってみると期待通りの結果が得られる.

次は引数を2倍にする S I I を実行してみる.確かに (S I I) x = x x となっている. これを自分自身に適用すると,(S I I) = (S I I) = ... となり,無限ループに陥る. このシステムはこういう簡単なケースだけは Cycle detected とメッセージを出して止まるように している.

3.2 ラムダ式から SKI コンビネータ式への変換トレース

では,いよいよλ式を SKI コンビネータの式に変換したログを見てみよう.このシステムでは コマンド

:l2c -d xxx = λ式

で与えられた式を SKI コンビネータの式に変換して結果を xxx に覚えておく.-d は, 変換の過程のトレースを表示するという意味である.これが無いと,結果だけが表示される. また,表示する文字は通常の ASCII キャラクタだけに限りたかったので, λx.E を x.E と表記してある.慣れるまで違和感があるかもしれないがご容赦いただきたい.

では,最初から少し高度なものを.x を x x に変える式を求めてみよう.これは ラムダ式で書くと,

λx.(x x)

である.我々の記法では,

x.(x x)

である.

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

"<-" は,その右辺の式が変換対象として入ってきたことを表している."->" は逆に 変換結果を表している.また,2行目の右側に表示されている

t(u.(A B)) = (S t(u.A) t(u.B))

は,変換したとき使ったルールを表している.ここで, t(...) は,... を SKI の式に変換するという意味である.つまり,このルールは

λu.(A, B) を (S t(λu.A) t(λu.B)) に変換する

というルールを表している.意味的には,A と B をそれぞれが引数を取れるように,λu.A と λu.B の 形にしてそれぞれ SKI の式に変換し,コンビネータ S を使って,変換結果の後ろに 引数が来た時,それぞれの SKI の式に分配するという式である.この例では λu は,λx で (A B) は (x x) だから,どちらも λx.x になり,その変換が3行目と5行目で要求されどちらも,4行目と6行目で I の結果を得ている.これらの部分式の変換を組み合わせて,最終的な答えが7行目に表示されている.結果は期待通り S I I となった.

次は,準備のところで説明した false に変換されるラムダ式を SKI の式に 変換してみる. false は

false x y = y

となる式でラムダ式で書くと(今後次第に,ツールに合わせてλを省略することが多くなってくる)

x.y.x (λx.λy.y を表す)

である.こちらは期待通り,K I になっている.λy.y には x は現れないので,λx.λy.y は, K を使って,K t(λy.y) とやればよい.つまり結果は K I である.

その後の,x.y.x は true = K に対応するλ式なのだが,変換のルール通りにやってしまうと, K が得られずに,かなり大きな式になる.一般にλ基の連鎖,λx.λy. は2重の変換を要求されるので 結果が大きくなりがちである.

SKI> :l2c -d xxx=x.y.y
    <- x.y.y   [ t(u.A) = K t(A)  :when u not free in A ]
    |   <- y.y   [ t(u.u) = I ]
    |   -> I   [ t(u.u) = I ]
    -> K I   [ t(u.A) = K t(A)  :when u not free in A ]
  => K I
SKI> :l2c -d xxx=x.y.x
    <- x.y.x   [ t(u.v.A) = t(u.t(v.A))  :when u free in v.A ]
    |   <- y.x   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   <- x   [ t(u) = u ]
    |   |   -> x   [ t(u) = u ]
    |   -> K x   [ t(u.A) = K t(A)  :when u not free in A ]
    |   <- x.(K x)   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    |   |   <- x.K   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   |   <- K   [ t(u) = u ]
    |   |   |   -> K   [ t(u) = u ]
    |   |   -> K K   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   <- x.x   [ t(u.u) = I ]
    |   |   -> I   [ t(u.u) = I ]
    |   -> (S (K K)) I   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    -> (S (K K)) I   [ t(u.v.A) = t(u.t(v.A))  :when u free in v.A ]
  => (S (K K)) I

次のは,2つの引数を交換する exchange だが,こちらも結果が

(S (K (S I))) ((S (K K)) I)

と,かなり大きくなっている. 準備の時に述べた exchange は,

(S (K (S I))) K

である.下の方の検算, xxx u v の評価を見ると,確かに v u とひっくり返された結果がでている.

SKI> :l2c -d xxx=x.y.(y x)
    <- x.y.(y x)   [ t(u.v.A) = t(u.t(v.A))  :when u free in v.A ]
    |   <- y.(y x)   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    |   |   <- y.y   [ t(u.u) = I ]
    |   |   -> I   [ t(u.u) = I ]
    |   |   <- y.x   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   |   <- x   [ t(u) = u ]
    |   |   |   -> x   [ t(u) = u ]
    |   |   -> K x   [ t(u.A) = K t(A)  :when u not free in A ]
    |   -> (S I) (K x)   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    |   <- x.((S I) (K x))   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    |   |   <- x.(S I)   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   |   <- S I   [ t(A B) = t(A) t(B) ]
    |   |   |   |   <- S   [ t(u) = u ]
    |   |   |   |   -> S   [ t(u) = u ]
    |   |   |   |   <- I   [ t(u) = u ]
    |   |   |   |   -> I   [ t(u) = u ]
    |   |   |   -> S I   [ t(A B) = t(A) t(B) ]
    |   |   -> K (S I)   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   <- x.(K x)   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    |   |   |   <- x.K   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   |   |   <- K   [ t(u) = u ]
    |   |   |   |   -> K   [ t(u) = u ]
    |   |   |   -> K K   [ t(u.A) = K t(A)  :when u not free in A ]
    |   |   |   <- x.x   [ t(u.u) = I ]
    |   |   |   -> I   [ t(u.u) = I ]
    |   |   -> (S (K K)) I   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    |   -> (S (K (S I))) ((S (K K)) I)   [ t(u.(A B)) = (S t(u.A) t(u.B)) ]
    -> (S (K (S I))) ((S (K K)) I)   [ t(u.v.A) = t(u.t(v.A))  :when u free in v.A ]
  => (S (K (S I))) ((S (K K)) I)
SKI> xxx u v
 =>     (((S (K (S I))) ((S (K K)) I)) u) v
 =>     (((K (S I)) u) (((S (K K)) I) u)) v
 =>     ((S I) (((K K) u) (I u))) v
 =>     (I v) ((((K K) u) (I u)) v)
 =>     v ((K u) v)
 =>     v u

最後に,Y コンビネータ,

Y = λf.((λx.(f (x x))) (λx.(f (x x))))

の SKI コンビネータ式を求めてみる.結果は結構大きな式になる. こちらは Y g を評価すると

Y g => g (Y g) => g (g (Y g)) => ...

と止まらなくなってしまうはずである.一応,変換回数に制限を設けているので, 次のログでは50回目に諦めてとまっている.その間,g を前にいくつもつけるような動作を 行っている.

SKI> :l2c Y=f.((x.(f (x x))) (x.(f (x x))))
  => (S ((S ((S (K S)) ((S (K K)) I))) (K ((S I) I)))) ((S ((S (K S)) 
((S (K K)) I))) (K ((S I) I)))
SKI> Y g
 =>     ((S ((S ((S (K S)) ((S (K K)) I))) (K ((S I) I)))) ((S ((S (K S))
((S (K K)) I))) (K ((S I) I)))) g
 =>     (((S ((S (K S)) ((S (K K)) I))) (K ((S I) I))) g) (((S ((S (K S)) 
((S (K K)) I))) (K ((S I) I))) g)
 =>     ((((S (K S)) ((S (K K)) I)) g) ((K ((S I) I)) g)) ((((S (K S)) 
((S (K K)) I)) g) ((K ((S I) I)) g))
 =>     ((((K S) g) (((S (K K)) I) g)) ((S I) I)) ((((K S) g) 
(((S (K K)) I) g)) ((S I) I))
 =>     ((S (((K K) g) (I g))) ((S I) I)) ((S (((K K) g) (I g))) ((S I) I))
 =>     ((((K K) g) (I g)) ((S (((K K) g) (I g))) ((S I) I))) (((S I) I) 
((S (((K K) g) (I g))) ((S I) I)))
 =>     ((K g) ((S (K g)) ((S I) I))) ((I ((S (((K K) g) (I g))) ((S I) I))) 
(I ((S (((K K) g) (I g))) ((S I) I))))
 =>     g (((S (((K K) g) (I g))) ((S I) I)) ((S (((K K) g) (I g))) ((S I) I)))
 =>     g (((((K K) g) (I g)) ((S (((K K) g) (I g))) ((S I) I))) (((S I) I) 
((S (((K K) g) (I g))) ((S I) I))))
 =>     g (((K g) ((S (K g)) ((S I) I))) ((I ((S (((K K) g) (I g))) ((S I) I))) 
(I ((S (((K K) g) (I g))) ((S I) I)))))
 =>     g (g (((S (((K K) g) (I g))) ((S I) I)) ((S (((K K) g) (I g))) ((S I) I))))
    ...
 =>     g (g (g (g (g (g (g (g (g (g (g (g (g (g (g (((S (((K K) g) (I g))) 
((S I) I)) ((S (((K K) g) (I g))) ((S I) I)))))))))))))))))
*** Limit(50) exceeded

変換の例ではないが,このインタープリタは SKI のほかに組み込みのコンビネータとして 次のようなものを持っている.

SKI> :r
  Rules for system combinators
  -------------------------------------
   1.  (I x)  =>  x
   2.  ((K x) y)  =>  x
   3.  (((S x) y) z)  =>  ((x z) (y z))
   4.  (((C f) x) y)  =>  ((f y) x)
   5.  (((B f) g) x)  =>  (f (g x))
   6.  (M x)  =>  (x x)
   7.  ((T x) y)  =>  (y x)
   8.  (((R x) y) z)  =>  ((y z) x)
   9.  (((V x) y) z)  =>  ((z x) y)
  10.  ((W x) y)  =>  ((x y) y)
  11.  (X x)  =>  ((x S) K)
  12.  (Y0 f)  =>  (f (Y0 f))
  13.  ((Z g) v)  =>  ((g (Z g)) v)

Y0 や Z は不動点コンビネータである.

また,予めいくつかのコンビネータの式に名前をつけている. 次の Y10 や Y2 は,不動点コンビネータの機能を持っているものだが, 自動でラムダ式 Y から変換したものに比べてずいぶん短い.

SKI> :ls
  Current definitions
  -------------------------------------
   1.  exchange = S (K (S I)) K
   2.  demo = exchange x y
   3.  sii = S I I
   4.  omega = sii
   5.  aa = omega a
   6.  Omega = omega omega
   7.  Y10 = S (K (S I I)) (S (S (K S) K) (K (S I I)))
   8.  Y2 = S S K (S (K (S S (S (S S K)))) K)
   9.  true = K
  10.  false = K I
  11.  not = V false true
  12.  and = R false
  13.  or = T true
  14.  imply = T true
  15.  equiv = C S not
  16.  zero = I
  17.  suc = V false
  18.  eq_zero = T true
  19.  pre = T false
  20.  test1 = eq_zero (pre (suc zero))
  21.  test2 = eq_zero (suc zero)

確かに, Y10 g とやると

SKI> Y10 g
 =>     ((S (K ((S I) I))) ((S ((S (K S)) K)) (K ((S I) I)))) g
 =>     ((K ((S I) I)) g) (((S ((S (K S)) K)) (K ((S I) I))) g)
 =>     ((S I) I) ((((S (K S)) K) g) ((K ((S I) I)) g))
 =>     (I ((((S (K S)) K) g) ((K ((S I) I)) g))) (I ((((S (K S)) K) g) ((K ((S I) I)) g)))
 =>     ((((S (K S)) K) g) ((K ((S I) I)) g)) ((((S (K S)) K) g) ((K ((S I) I)) g))
 =>     ((((K S) g) (K g)) ((S I) I)) ((((K S) g) (K g)) ((S I) I))
 =>     ((S (K g)) ((S I) I)) ((S (K g)) ((S I) I))
 =>     ((K g) ((S (K g)) ((S I) I))) (((S I) I) ((S (K g)) ((S I) I)))
 =>     g ((I ((S (K g)) ((S I) I))) (I ((S (K g)) ((S I) I))))
 =>     g (((S (K g)) ((S I) I)) ((S (K g)) ((S I) I)))
 =>     g (((K g) ((S (K g)) ((S I) I))) (((S I) I) ((S (K g)) ((S I) I))))
 =>     g (g ((I ((S (K g)) ((S I) I))) (I ((S (K g)) ((S I) I)))))
 =>     g (g (((S (K g)) ((S I) I)) ((S (K g)) ((S I) I))))
 =>     g (g (((K g) ((S (K g)) ((S I) I))) (((S I) I) ((S (K g)) ((S I) I)))))
 =>     g (g (g ((I ((S (K g)) ((S I) I))) (I ((S (K g)) ((S I) I))))))
 =>     g (g (g (((S (K g)) ((S I) I)) ((S (K g)) ((S I) I)))))
 =>     g (g (g (((K g) ((S (K g)) ((S I) I))) (((S I) I) ((S (K g)) ((S I) I))))))
    ...
*** Limit(50) exceeded

と,g を次々に前に付けていく動作を行う.


3.3 補足的な話題

(もう少しなにか面白そうなことがあったら,ここに書くかもしれません.)

4.まとめ

今回は,SKI のインタープリタとλ式から SKI コンビネータ式への変換ツールを Ruby で 書いてみた.

コンビネータの式は簡単な機能のものでもすぐ大きくなっていくので実行や変換を 追って行っても,サイズが大きくなるとすぐ人間の理解の限界を超えてしまう. たぶん,自分でこういうツールを作ってみるのがよい勉強になるんだろうなと思った. 今回のプログラムは Ruby で空行やコメントも入れて,668 行である.お勉強を兼ねて 作ってみるのに手ごろな大きさである.

参考文献

以下の文献が参考になると思う.直接リンクが張ってないものは著者名とタイトルをコピーして 検索エンジンで検索見て欲しい.
    Wikipedia
    まず,Wikipedia が良い参考資料となる.日本語,英語の以下の項目を以下の項目を 通して読むと結構な情報量になる.

  1. コンビネータ論理 - Wikipedia
  2. SKIコンビネータ計算 - Wikipedia
  3. B,C,K,Wシステム - Wikipedia
  4. ラムダ計算 - Wikipedia
  5. 不動点コンビネータ - Wikipedia
  6. Combinatory logic - Wikipedia
  7. Lambda calculus - Wikipedia
    and so on

    Stanford Encyclopedia of Philosophy
    論理学,集合論など,数学基礎論っぽいテーマはここにもたくさん書いてあり, 私はよく活用させていただいている.

  8. Combinatory Logic

    レクチャーノートや教科書など(オンラインで参照可能なもの)
    λ計算とコンビネータ論理の両方を含むテキストとしては次のようなものがある.

  9. Jean-Lous Krivine : LAMBDA-CALCULUS TYPES AND MODELS, translated from french by R Cori, 1993

おまけ:C言語で不動点演算子の真似事をする方法

次のプログラムは明示的には再帰呼び出しをしないで,再帰の機構を 使って階乗を定義している. main() の中で,fact の g に fact 自身をバインディングしているのがミソですね.

#include <stdio.h>

int fact(int n, int (*g)()) {
    if (n == 0)
        return 1;
    else
        return n*(*g)(n-1, g);
}

int main(void) {
    int ret;

    ret = fact(10, fact); /* gにfactをバインディング */
    printf("fact(10) = %d\n", ret);
    return 0;
}


おまけ:Simple SKI Interpreter のその他の機能

SKI インタープリタにはいろいろな機能を組み込んだ.コンビネータ論理のを 始めて学ぶときに役に立ちそうなものもあるのでいくつかを紹介する.

:help とやると,全機能がリストアップされる.この中で,:let コマンドは コンビネータの式に名前をつける機能で少しずつ複雑な式を定義していくとき 便利である.:l2c (lambda expression to combinator expression)は,本文の 中でも述べたように,λ式をコンビネータの式に変換するコマンドであり, 変換過程をトレースできるようになっている.

本文では紹介しなかったプリティプリントモードの設定コマンド :pp という ものがあり,これが初心者がコンビネータの式の計算過程を理解するのに役に立つのでは 無いかと思うので紹介する.

SKI> :help
    Commands
    --------------------------------------------------
     :let   ... :let <NAME> = <COMBINATOR EXPRESSION>
                sets <COMBINATOR EXPRESSION> to <NAME>
     :list  ... shows <NAME>s currently defined
     :del   ... :del <NAME>
                deletes the definition of <NAME>
     :clear ... clears all <NAME>s
     :l2c   ... :l2c [-d] <NAME> = <LAMBDA TERM>
                converts <LAMBDA TERM> to an expression of S, K, I and
                sets it to <NAME>. Write x.E for Lx.E where L means lambda.
                Lx is right associative while applications are left
                associative, e.g., x.y.(x y x) means Lx.(Ly.((x y) x))
                -d shows the process of the translation.
     :limit ... :limit [N]
                sets limit to stop infinite loop (default=50)
     :pp    ... toggles pretty print mode (default = false).
     :rule  ... shows the rules for system combinators S, K, I, ...
     :load  ... :load <FILE>
                change input from spefified <FILE>.
     :pause ... :pause some message
                waits for hitting Enter key.
     :help  ... shows this message
     :quit  ... quits SKI Interpreter

     Expression beginning with a character other than ':' is evaluated
     as a combinator expression.  When you omit parentheses, expressions
     are combined left to right, for example, T1 T2 T3 T4 is interpreted
     as (((T1 T2) T3) T4).  You can use <NAME> as a part of input.
     <NAME>s are replaced by the strings you set to them.

プリティプリントモードは通常 false になっているが,これをtrue にすることにより, コンビネータの式を計算する過程が簡易ツリー表示されるようになっている.

次のログでは最初に :pp でプリティプリントモードに入り,二つの引数を交換する コンビネータの式 exchange = (S K (S I))) K を表示している.自分の経験だが, 最初にコンビネータの式を見たときは,括弧だけでは,それがどのような構造をしているのか イメージしにくかった.ここでの簡易ツリー表示は左が木(ツリー)の根で右が葉っぱで ある.(S (K (S I))) K は根の最初の子供が (S (K (S I))) で,二番目の子供が K と 読む.コンビネータの式は二分木である.

SKI> :pp
pp mode is set to true
SKI> exchange
 =>     (S (K (S I))) K

        +--+--S
        |  `--+--K
        |     `--+--S
        |        `--I
        `--K

SKI> exchange x y
 =>     (((S (K (S I))) K) x) y

        +--+--+--+--S
        |  |  |  `--+--K
        |  |  |     `--+--S
        |  |  |        `--I
        |  |  `--K
        |  `--x
        `--y

 =>     (((K (S I)) x) (K x)) y

        +--+--+--+--K
        |  |  |  `--+--S
        |  |  |     `--I
        |  |  `--x
        |  `--+--K
        |     `--x
        `--y

 =>     ((S I) (K x)) y

        +--+--+--S
        |  |  `--I
        |  `--+--K
        |     `--x
        `--y

 =>     (I y) ((K x) y)

        +--+--I
        |  `--y
        `--+--+--K
           |  `--x
           `--y

 =>     y x

        +--y
        `--x

一応,主要なコンビネータの式を簡易ツリー表示しておこう.以下では,SKI 以外の コンビネータも出てくるので,ここでの定義をまず列挙しておく.

  Rules for system combinators
  -------------------------------------
   1.  (I x)  =>  x
   2.  ((K x) y)  =>  x
   3.  (((S x) y) z)  =>  ((x z) (y z))
   4.  (((C f) x) y)  =>  ((f y) x)
   5.  (((B f) g) x)  =>  (f (g x))
   6.  (M x)  =>  (x x)
   7.  ((T x) y)  =>  (y x)
   8.  (((R x) y) z)  =>  ((y z) x)
   9.  (((V x) y) z)  =>  ((z x) y)
  10.  ((W x) y)  =>  ((x y) y)
  11.  (X x)  =>  ((x S) K)
  12.  (Y0 f)  =>  (f (Y0 f))
  13.  ((Z g) v)  =>  ((g (Z g)) v)

これらの定義のもとに,いくつかのコンビネータの式の簡易ツリー表示や 計算過程を示す.

SKI> true
 =>     K

        K

SKI> false
 =>     K I

        +--K
        `--I

SKI> not
 =>     (V (K I)) K

        +--+--V
        |  `--+--K
        |     `--I
        `--K

SKI> not true
 =>     ((V (K I)) K) K

        +--+--+--V
        |  |  `--+--K
        |  |     `--I
        |  `--K
        `--K

 =>     (K (K I)) K

        +--+--K
        |  `--+--K
        |     `--I
        `--K

 =>     K I

        +--K
        `--I

SKI> or
 =>     T K

        +--T
        `--K

SKI> or false true
 =>     ((T K) (K I)) K

        +--+--+--T
        |  |  `--K
        |  `--+--K
        |     `--I
        `--K

 =>     ((K I) K) K

        +--+--+--K
        |  |  `--I
        |  `--K
        `--K

 =>     I K

        +--I
        `--K

 =>     K

        K

SKI> sii sii
 =>     ((S I) I) ((S I) I)

        +--+--+--S
        |  |  `--I
        |  `--I
        `--+--+--S
           |  `--I
           `--I

 =>     (I ((S I) I)) (I ((S I) I))

        +--+--I
        |  `--+--+--S
        |     |  `--I
        |     `--I
        `--+--I
           `--+--+--S
              |  `--I
              `--I

 =>     ((S I) I) ((S I) I)

        +--+--+--S
        |  |  `--I
        |  `--I
        `--+--+--S
           |  `--I
           `--I


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

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