ISLispでラムダ計算インタプリタを作った話

久々にLisp

自作のEasy-ISLispは開発終了し、今はメンテナンスモードです。バグ報告もなく穏やかな日々です。でも、たまにはLispを書いておかないと忘れてしまいそうです。そこで、中途半端にしていたラムダ計算のインタプリタを仕上げて動作するようにしました。

内部データ構造

ラムダ式はリストで次のようにしました。

（＾　引数　本体）

変数は1文字のシンボルであらわします。M,Nをラムダ項だとすれば　MNは（M N)というリストであらわします。左結合なのでABCは ((A B) C)となります。

省略記法

^xyz.z は　^x.^y.^z.zの省略記法です。

内部形式は　(^ x (^ y (^ z z))) となります。

パース

Easy-ISLispのライブラリにあるパターンマッチマクロを利用しています。これだとElixir風の記述ができます。パーサを簡潔に書くことができました。cond節で場合分けをするとけっこう複雑になってしまいます。コードは次のようになっています。

(defun parse* (x)
    (pipe x |> (convert <list>) |> (parse nil) ))
 
#|
parse 
 ^x.x -> (^ x x)
 (^x.x)(^y.y) -> ((^ x x)(^ y y))

|#
(defglobal *rest-list* nil)

(defpattern parse
  ((empty _res) _res)
  ;; space skip
  (((#\space :rest _ls) _res) (parse _ls _res))
  (((#\e #\n #\d) _res) 'end)
  (((#\^ _arg #\. :rest _ls) _) (let* ((arg1 (convert _arg <symbol>))
                                       (body (parse _ls nil)))
                                  (parse *rest-list* (list '^ arg1 body))))
  ;; e.g. ^xyz.z shorthand
  (((#\^ _arg :rest _ls) _) (let* ((arg1 (convert _arg <symbol>)))
                               (cons '^ (list arg1 (parse (cons #\^ _ls) nil)))))
  ;; ( )
  (((#\( :rest _ls) _res) (let* ((exp (parse _ls nil)))
                              (if (null _res)
                                  (parse *rest-list* exp)
                                  (parse *rest-list* (cons _res (list exp))))))
  (((#\) :rest _ls) _res)
      (setq *rest-list* _ls)
      _res)
  (((_body :rest _ls) empty) (when (variable-p _body))
             (setq *rest-list* _ls)
             (parse *rest-list* (convert _body <symbol>)))
  (((_body :rest _ls) _res) (when (variable-p _body))
             (setq *rest-list* _ls)
             (parse *rest-list* (cons _res (list (convert _body <symbol>)))))
  (else (print "syntax error")))

readlineを使って文字列としても取り込み、これをキャラクタを要素とするリストに変換します。これをparseは解析しています。Elixir風のパイプ演算子も使えるようにしてあります。

簡約

簡約化、リダクションがラムダインタプリタの肝です。再帰構造になっているのでけっこうめんどくさいです。もっとも左側のラムダ式から順次ベータ変換をしていきます。このベータ変換をした直後にピリオドの後ろの部分を簡約化しておく必要があります。単純な例、　(^x.x)a のようなものですと簡単なのですが、複雑なラムダ式の簡約化はじっくりと考える必要があります。コードは次のようになっています。やはりパターンマッチングを利用しています。

(defpattern reduce
    ((end) (throw 'exit "end"))
    ((_x) (when (atom _x)) _x)
    (((^ _arg _body)) (list '^ _arg (reduce _body)))
    (((_x _y)) (when (atom _x)) (list _x _y))
    (((_x _y)) (when (lambda-p _x)) (print* (list _x _y)) (reduce (beta _x _y)))
    (((_x _y)) (when (consp _x)) (print* (list _x _y)) (beta (reduce _x) _y))
    (else (print "reduce error") 'error)
)
    

(defun beta (x y)
    (if (lambda-p x)
        (let ((arg (cadr x))
              (body (caddr x)))
          (replace arg body y))
        (list x y)))

(defun replace (arg body y)
    (cond ((null body) nil)
          ((and (atom body) (eq arg body)) y)
          ((atom body) body)
          (t (cons (replace arg (car body) y)
                   (replace arg (cdr body) y)))))

  

コンビネータ

S,K,Iと呼ばれているコンビネータも組み込んであります。Yコンビネータも組み込んでいます。ハッカーズニュースで有名なYコンビネータ社はその創業者のグレアムさんが若い頃にYコンビネータに感銘を受けたからだって聞きました。

大文字のS,K,I,Yがでてくると所定のラムダ式に変換するようになっています。これもパターンマッチングを利用しています。

(defpattern combinator
  ((empty) nil)
  ((_x) (when (lambda-p _x)) _x)
  ((I) '(^ x x))
  ((K) '(^ x (^ y x)))
  ((S) '(^ x (^ y (^ z ((x z) (y z))))))
  ((Y) '(^ y ((^ x (^ y (^ x x))) (^ x (^ y (^ x x))))))
  (((_x :rest _xs)) (cons (combinator _x) (combinator _xs)))
  ((_x) _x))

とりまとめ

これらのパーサと簡約化のコードを利用してインタプリタを組み上げています。readlineで文字列として入力を取り込み、パースします。さらにここにコンビネータがあれば置換します。そしてメインの簡約化、reduceに渡します。最後はラムダ式を画面表示するprint*関数に渡します。これをひたすら繰り返しています。

reduce関数は途中の変換過程が見えるようにその過程をプリントしています。

(defun repl ()
  (format (standard-output) "Lambda calculus interpreter ~%")
  (format (standard-output) "To quit enter 'end'~%")
  (repl1))


(defun repl1 ()
  (block repl
    (cond ((catch 'exit
             (for ((s (read*) (read*)))
                  ((equal s 'end) (return-from repl t))
                  (print* (reduce (combinator s))))) t)
          (t (prompt)(repl1)))))

(defun read* ()
  (format (standard-output) "L> ")
  (parse* (read-line)))

SKKコンビネータを簡約化すると下記のようになります。

Easy-ISLisp Ver2.38
> (load "example/lambda.lsp")
T
> (repl)
Lambda calculus interpreter 
To quit enter 'end'
L> SKK
(^X.^Y.^Z.XZ(YZ))(^X.^Y.X)(^X.^Y.X)
(^X.^Y.^Z.XZ(YZ))(^X.^Y.X)
(^X.^Y.X)Z(YZ)
(^X.^Y.X)Z
^Z.Z
L> 

SKKは簡約化されると　^x.xとなります。したがってSKKa は　aとならないといけません。これがなかなかうまくいかなくて考えていました。高橋正子先生の計算論を読み直してました。こういったコードを書くことにより良くラムダ計算のことを理解できます。手計算での簡約化では人間があっさりとα変換、β変換をしてしまうところもコンピューターに教えるのはなかなか骨が折れます。理解が深まります。

反応

完成したので英語版のreddit/lispに投稿してみました。10以上のアップボートをいただきました。世界は広いのでこういうアカデミックなものにも興味をもってくれるLisperがいらっしゃるようです。楽しんでもらえてると嬉しいです。一時は仕事に実用的に使えるなるものでないと、と職業プログラマLisperから言われたものでしたが。グレアムさんの頃のブームも去ってLisp界隈も落ち着いてきたみたいです。

全スースコードはGithubにおいてあります。exampleフォルダのlambda.lspです。テストはlambda-test.lspです。
https://github.com/sasagawa888/eisl

参考文献

「計算論」ー計算可能性とラムダ計算　高橋正子　著　近代科学者