Line 1: Error: Invalid Blog('by Esehara' )

または私は如何にして心配するのを止めてバグを愛するようになったか

>> Zanmemo

あと何かあれは 「esehara あっと じーめーる」 か @esehara まで

Racket(Lisp)で簡単なラムダ簡約機作った

街の風景

f:id:nisemono_san:20160531155716j:plain

はじめに

こないだ、知人の「会」という曖昧なことが行なわれ、そこに参加していたら、酔っぱらったtakano32さんが「Rubyでラムダ簡約機作っていて、これ凄く革新的だと思うんですけど、誰もスターを付けてくれないんですよ」とクダを巻いていだ。見てみると、やっていることはとても楽しそうで、ただ最終コミットが5年前なのが惜しく、よし、どうせなら自分でも簡単なラムダ簡約機を作ってみようと思ったのが今回の記事の経緯である。

ラムダってそもそも何よ

過去のブログにも書いだけれども、改めて説明するならば、無名の関数というのが良いだろうか。例えば、ある変数をそのまま返す関数として、{id(x) = x}を定義できる。しかし、これが使い捨てである場合、関数に対してわざわざ名前を付けていくのは苦難である(プログラミングでも良くあることだと思う)。だから、「名前の付いた関数」から「関数」を切りはなし、関数それ自体をあらわすもの、と考えるといいと思う。例えば、先の例であるならば、{\lambda_x.x}と書くことができる。

さて、そこで一つの疑問が出てくる。ラムダ計算の対象とは一体なんなのか、ということだ。ここで、ラムダ項という式を導入する。この式は三つの規則によってなりたっている。

ここで、任意のラムダ項であるMを導入する。まず最初に、この任意のラムダ項はxといったような変数を取る(1)。まだ、{\lambda_x.M}といったように、ラムダを構成することができる(2)。また、別のラムダ式Nを導入し、(M N)といった形で関数適用した場合、それもまたラムダ式となる(3)。

具体的に考えてみよう。例えば、先ほどの{\lambda_x.x}の場合、規則(2)により、{\lambda_x.M}に直しる。ここに出るMxだが、xは規則(1)により、ラムダ項になる。従って{\lambda_x.x}はラムダ項になる。

ラムダを簡約する

上記の内容をなんとなく理解して頂けたと仮定して、例えば、{(\lambda_x.xx)M}という項があった場合、これがなんとなく{M(M)}になりそうだということがわかる。また、{(\lambda_x.xx)(\lambda_y.y)}{(\lambda_y.y)(\lambda_y.y)}になり、{(\lambda_y.y)}となる。このように、式を簡単にしていく簡約を、β簡約という。(もうすこし正確に言うと、ラムダ項の変数に代入して簡約することになるっぽいんだけど、それは省略する)誤解せず言ってしまえば、ラムダ項に関数適用が行なわれた場合に、変数を次次と起きかえた式にしていく感じで理解している(というか、そういう実装にしている)。

実装

実装はあいかわず、リストを利用してRacketで行なう。S式に直した場合、以下のような表記とする。

'((& x (dot x)) N)

これにはちょっとした裏話があって、実はdotは可読性のためにいらないのではないか、という問題は浮上しているのだけれど、怠惰のため、ほっといている。

まず最初に、先ほど関数適用したラムダ項に起きかえるという話をした(こういうβ簡約で起きかえられるところをβレディックスというらしい)。従って、これらのノードを辿り、置換していくようなコードが必要になる。そんな都合のいいコードなんて多分標準ではなかろう、と思ったので、簡単にそういう役割をするコードを書く。先にテストを見せたあとに、内容を出そうと思う。

(check-equal? (replace-node '(a b c) 'a 'N) '(N b c))
(check-equal? (replace-node '(a b (a b c) c) 'b 'M) '(a M (a M c) c)) 

途中でリストが出てくることを踏まえて書いたコードが下の通りになる。

(define (replace-node body param-name replace)
  (replace-node-process body '() param-name replace))

(define (replace-node-process list-process result param-name replace)
  (cond [(null? list-process) result]
        [(list? (car list-process))
         (let ([list-result 
                (list (replace-node (car list-process) param-name replace))])
           (replace-node-process (cdr list-process)
                                 (append result list-result)
                                 param-name replace))]
        [else (let* ([target (car list-process)]
                     [result-symbol
                      (if (symbol=? param-name target) replace target)])
                (replace-node-process (cdr list-process)
                                      (append result (list result-symbol))
                                      param-name replace))]))

あいかわず随分汚ないコード。ポイントとしては、リストが出てきたときには、新しくreplace-node-processを呼んでいるくらいだと思う。

とりあえず、リスト内のある要素を全て置換することはできたとして、ではこれをどうやって適用させていくか、ということになる。

ラムダの簡約にはそれなりの戦略があるのだが、ここでは素朴な戦略を取ろう。素朴な戦略とは、ラムダの後ろに並んでいる引数を一つずつ適用し、その結果を返すという方法である。現状出てきている式は、「ラムダ項→適用するラムダ項」の順番に並んでいる(これは、実は正しい簡約とは言えないのだが、のちほど説明する)ので、決めうちで、前者と後者を「適応するラムダ項」と「適応されるラムダ項」に分ける。

(define (beta1-> l-term)
  (if (or (not (lambda-type? (car l-term)))
          (null? (car l-term)))
      (raise
       (string-append "This form is already beta nomal form:" (list->string l-term)))
      (apply->lambda (car l-term) (cdr l-term))))

(define (lambda-type? l) (symbol=? '& (car l)))

lambda-type?は、そのリストがラムダの形をしているかどうかである。現状としては、先頭に&があるかどうかだけをチェックしている。

(define (lambda-type? l) (symbol=? '& (car l)))

「適用されるラムダ項」と「適用するラムダ項」を受けとったら、今度は、「適用されるラムダ項」がどういう構造になっているかを調べ、置換してやればよい。

(define (apply->lambda l-term params)
  (if (null? params) l-term
      (let* ([param-name (second l-term)]
             [body       (third  l-term)])
        (filter (lambda (x)
                  (or (not (symbol? x))
                      (not (symbol=? 'dot x))))
                (append (replace-node body param-name (car params)) (cdr params))))))

「適用されるラムダ項」のパラメータにあたる部分(& x (dot x))の二番目のxまでは、適用により捨ててよいが、何が何に変換されるかは覚えておいたほうがよい。なので、letで名前付けをおこなってわかりやすくしている。

さて、これを組みあわせると、大体下のような簡単なラムダ式ならば、簡約が可能になる:

  ;; beta-reduction step by step check

  ;; (λx.x) N -- beta1 -> N
  (check-equal? (beta1-> '((& x (dot x)) N)) '(N))

  ;; (λx.x(xy)N -- beta1 -> N(Ny)
  (check-equal? (beta1-> '((& x (dot x (x y))) N)) '(N (N y)))

  ;; (λx.(λy.yx)z)v -- beta1 --> (λy.yu)z -- beta1 --> (zu)
  (check-equal? (beta1-> '((& x ((& y (dot y x)) z)) u)) '((& y (dot y u)) z))
  (check-equal? (beta1-> (beta1-> '((& x ((& y (dot y x)) z)) u))) '(z u))

  ;; (λx.y)N -- beta1 --> y
  (check-equal? (beta1-> '((& x (dot y)) N)) '(y))

  ;; (λx.xx)(λx.xx) -- beta1 --> (λx.xx)(λx.xx)
  (check-equal? (beta1->
                 '((& x (dot x x)) (& x (dot x x))))
                 '((& x (dot x x)) (& x (dot x x)))) 

  ;; (λx.xxy)(λx.xxy) -- beta1 --> (λx.xxy)(λ.xxy)y
  (check-equal? (beta1->
                 '((& x (dot x x y)) (& x (dot x x y))))
                 '((& x (dot x x y)) (& x (dot x x y)) y))
  
  ;; (λx.xxy)(λx.xxy)y -- beta1 --> (λx.xxy)(λ.xxy)yy
  (check-equal? (beta1->
                 '((& x (dot x x y)) (& x (dot x x y)) y))
                 '((& x (dot x x y)) (& x (dot x x y)) y y))

問題点

先ほども言ったように、この実装自体にはちょっとした問題点がある。それは最初が{\lambda_x.M}の形でなければ簡約してくれないことである。簡約を考える場合、最初のラムダ項が簡約できなくても、別のラムダ項が簡約できることもあるはずだ。とするならば、そのノードを探し、そこは簡約するといった戦略は必要になるとは思うのだが、プロトタイプで作ったために、そこのあたりは考慮に入れていない。また、このような簡約についても規則があり、その規則自体も追いきれてないので、表面的な解説にとどまっている。

まとめ

というわけで、知人のライブラリに影響されて、一晩でえいやと作ってしまった。こういうのが手癖で作れるのは本当に面白いし、人から刺激を受けて自分もやってみよう、と思うのはとてもいいことだと思った。機会があれば、もうすこしラムダ計算について勉強し、ライブラリに手をくわえていきたい。

ちなみに、ソースコードはここに置いています

参考になりそうな文献

論理と計算のしくみ

論理と計算のしくみ

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)