コンビネータでVM実装:old

[トップ][一覧][最近の更新]

編集中。

尚、内容の正しさは全く保証できません。 「○○は△△です」と言い切りの形で書いてあっても、鵜呑みにしない方が安全です。



概要

「全てのオブジェクトは関数である」という理念の極北とも言うべきunlambda。 そのunlambdaの基本となるS, Kコンビネータだけを用いて、論理的に正しく動作するVMを実装します。

尚、速度や実行コスト等は度外視します。

unlambdaには「難読化」というポリシーも含まれている為、VMの実装にはunlambdaそのものではなく、S式を利用します。具体的にはscheme。

目的

この実装を通じて、コンビネータへの理解を深めるのが目的です。

また、これが最後まで完了した際に、この構築構造を逆に辿り、scheme等のVMから仮想的に「全てのオブジェクトは関数であり、突き詰めていくと最終的にはSとKになる」という構造をユーザに見せる事が出来るとうれしいです。筆者が。

ルール

予習復習

unlambdaのルール

各種の書式や変換

;; まず、行いたい事を仮にschemeの疑似コードで書いてみる
(lambda (a b c)
  (a c b))
↓
↓(カリー化)
↓
(lambda (a)
  (lambda (b)
    (lambda (c)
      ((a c) b))))
↓
↓(λ算法書式)
↓
λa.λb.λc.((a c) b)
↓
↓(unlambda疑似関数書式)
↓
^a^b^c``$a$c$b
↓
↓(unlambda展開)
↓
^a^b^c``$b$c$a
↓
^a^b  ``s``s`k$bi`k$a
↓
^a    ``s``s`ks``s``s`ks``s`kki`ki``s`kk`k$a
↓
(長いので省略)

基礎コンビネータの準備

SとKを用意します(SとKの定義については http://hw001.gate01.com/eggplant/tcf/unlambda/tutorial.html を参照)。

(define (((S f) g) x)
  ((f x) (g x)))
(define ((K x) y) x)

……既にもう難読化に汚染されているような気もしますが、とりあえず先に進みます。

ユーティリティマクロの用意

コンビネータは一筋縄ではいかないので、最適解が見付かるまで、何回も定義を変更しながら試行錯誤を行う事になると思います。

そこで、lambdaを使って、定義を遅延評価(但し結果をキャッシュせずに毎回評価)しつつ実行するマクロを用意します。 また、間にlambdaをかませる事により、評価結果が名前付きで見れる場合があるので、より理解しやすくなる事も期待できます。

(define-macro (define-combinator name body)
  `(define ,name
     (lambda (arg)
       (,body arg))))

ですが、unlambdaでは、入力読み取り関数や継続生成関数等の副作用を持つ関数があるので、それらの関数をlambdaで囲むと問題があります(lambdaで囲む事で内部状態を持ってしまう為)。 これが問題になる場合は、以下の定義を採用し、再定義したくなった時には最初から全部の束縛を再定義するようにします。

(define define-combinator define)

他のコンビネータ

早速、SとKを使って他のコンビネータを定義してみます。

(define-combinator I ((S K) K))
(define-combinator B ((S (K S)) K))

Iについては説明は不要でしょう。

Bは(((B x) y) z) => (x (y z)) になります。

実はこの辺は、アンチョコが以下のサイトにあるので、必要に応じて定義していく予定です。

(define-combinator C ((S ((B B) S)) (K K)))
(define-combinator T (C I))
(define-combinator M ((S I) I))
(define-combinator L ((C B) M))
(define-combinator Y ((S L) L))

条件分岐

http://hw001.gate01.com/eggplant/tcf/unlambda/boolean.html を参考にして、ki-boolを採用します。

(define-combinator KI (K I))

(define-combinator true K)
(define-combinator false KI)

自然数その一(失敗)

まず、自然数とは何なのかを考えます。 筆者と思い付いたのは「秒読みのような、カウントする数値」です。

つまり、5なら、「4 3 2 1 0」(または「5 4 3 2 1」)と、5回カウントできるから5、という定義になります。

自然数を本式に実装する場合は、チャーチ数が良さそうです。

が、チャーチ数だと、コンビネータで表現するのは手間なので、代わりに定数ジェネレータの別名を持つKを使って実装してみます。 つまり、以下のようになります。

(define-combinator zero 'dummy)
(define-combinator one (K zero))
(define-combinator two (K one))
(define-combinator three (K two))
(define-combinator four (K three))
(define-combinator five (K four))

何をzeroに入れるかは、もう少しよく考えます。

この定義より、数の増減は以下のようになります。

(define-combinator plus1 K)
(define-combinator minus1 M)

minus1の時の引数が思い付かないので、とりあえず仮にλa.(a a)にします。つまりM。scheme式に書くなら(lambda (a) (a a))。

この前提で(minus1 zero)を評価すると(zero zero)となるので、ここから、zeroをIにするかfalseにするかを考えます。

とりあえず、zeroにはIを定義するのが良さそうな雰囲気です。

(define-combinator zero I)

もし、(minus1 zero)の結果を他の特定の何か(例外を示すコンビネータとか?)にしたい場合は、zeroではなく、minus1の方を前述のやり方でいじる事にします。

演算その一(失敗)

まず仮に、+3する関数を考えます。

+1が具体的にはλa.(K a)なので、+3はλa.(K (K (K a)))です。

ここから考えると、Yコンビネータと条件分岐を使って実装するのが良さそうです。

schemeで書くなら、

(define plus-n
  (lambda (f)
    (lambda (n)
      (lambda (acc)
        (if (zero? n)
          acc
          ((f (minus1 n)) (plus1 acc)))))))

といった感じです。 要するに、二つの引数を受け取り、片方がゼロになるまで、片方から1を引いてもう片方に1を足す事を繰り返しているだけです。

これならなんとか実装できそうですが、ゼロかどうかを判定する関数がまだありません。 今のところ、trueはK、falseは(K I)、zeroはIなので、比較的簡単に変換できそうな気配です。 しかし……

どうにも、「KとKI」に上手くマッピングする事ができません。

どうやら、ki-boolの欠点は、この「他の値からKとKIに上手くマッピングはできない」というところにあるようです。

つまり、ki-boolを採用するのであれば、「全てを最初からKとKIで構成する」必要があるようです。

更に、前述の(num K)ベースの演算を見ていると、このやり方ではおそらく、「偶数と奇数」は区別できても「ゼロとそれ以外の値」を区別する事はできなさそうです。

ここでチャーチ数をもう一度見直すと、チャーチ数は引数を二つ取るようになっています。 引数を二つずつ渡すようにすれば、この「偶数と奇数」の状態から脱出できるかも知れません。

よって、

  1. 全てを最初からKとKIで構成する
  2. 自然数は二つの引数を取る

この条件で、もう一度、自然数を実装し直してみる事にします。

自然数その二(チャーチ数)

もう一度、自然数の定義から考え直します。

という定義を、先程の演算から思い付きました。

この定義を採用するなら、ki-boolよりも、vi-boolの方が相性が良さそうな気もします。 が、unlambdaのvは、SとKからは生成できなさそうなので、vi-boolの採用は、この定義での実装も失敗した時にします。

これまでの試行錯誤によって、以下の機能が必要な事が分かっています。

この条件で色々と考えていたのですが、どうにも良い解が見付からないので、チャーチ数を実装します。

まずは、ゼロを定義します。

(define-combinator zero KI)       ; λf.λx.x

チャーチ数が一体どのような仕組みになっているのかを調べる為に、一旦unlambda化してみます。

0 = λf.λx.x
  = ^f^x $x
  = ^f   i
  =                                                      `ki

1 = λf.λx.(f x)
  = ^f^x `$f$x
  = ^f   ``s`k$fi
  =                                      ``s``s`ks``s`kki`ki

2 = λf.λx.(f (f x))
  = ^f^x `$f`$f$x
  = ^f   ``s`k$f``s`k$fi
  =                      ``s``s`ks``s`kki``s``s`ks``s`kki`ki

3 = λf.λx.(f (f (f x)))
  = ^f^x `$f`$f`$f$x
  = ^f   ``s`k$f``s`k$f``s`k$fi
  =      ``s``s`ks``s`kki``s``s`ks``s`kki``s``s`ks``s`kki`ki

(以下省略)

どうやら、+1する毎に、前置句として「``s``s`ks``s`kki」が追加されるようです。 つまり、以下のようになるようです。

(define-combinator plus1 (S ((S (K S)) ((S (K K)) I)))) ; `s``s`ks``s`kki

これで数が定義できます。

(define-combinator one   (plus1 zero))
(define-combinator two   (plus1 one))
(define-combinator three (plus1 two))
(define-combinator four  (plus1 three))
(define-combinator five  (plus1 four))

次に、minus1を考えます。

普通に考えるなら、plus1の逆を行う、つまり、「``s``s`ks``s`kki」を除去するという処理が実現できればokです。 が、一体どうすればそれが実現できるか分からないので、minus1を考えるのは先送りにします。 どうしても良い方法が思い付かない場合は「ゼロから順に再帰的にplus1していき、同じ数になったら、一つ前の数を返す」という方法を採用する事にします(数が同じかどうかを判定する部分でまた悩みそうですが)。

演算その二

ここに、ゼロ判定が載っているので、それを定義します。

ISZERO := λ n. n (λ x. FALSE) TRUE
↓
ISZERO := λ n. ((n (K KI)) K)
↓
λabc.c(ab)a か λabc.c(ba)b を探す
↓
無かったので、自前で展開する
↓
^n``$n`k`kik
↓
``s``si``s`kk``s`kk`ki`kk

よって、以下の定義になります。

(define-combinator zero? ((S ((S I) ((S (K K)) ((S (K K)) KI)))) K))

頑張ればもう少し短縮できそうですが、面倒なのでこれで行きます。

足し算掛け算が載っているので、Yを使って自前で実装するのは止めて(というか、今はまだ-1が無いので以前考えた方法は使えない)、実装しておきます。

ここから先はあとで……

ToDo

参考リンク


最終更新 : 2008/02/08 11:07:04 JST