ベータ簡約

ラムダ式をSKIコンビネータにバラすプログラムを書いてはみたものの、本当に正しく動いてんのか不安になって、(実際最初は間違ってたし。)逆を行なうプログラムを書いてみた。

(define (construct-S p1 p2 p3 rest)
  (if (not (pair? p1))
        `(,p1 ,p3 ,(if (not (pair? p2)) `(,p2 ,p3) `(,@p2 ,p3)) ,@rest)
        `(,@p1 ,p3 ,(if (not (pair? p2)) `(,p2 ,p3) `(,@p2 ,p3)) ,@rest)))
 
(define expand-combinator-one
(lambda (seq)
    (begin (display "---   ") (display seq) (newline)
        (cond
          ((not (pair? seq)) seq)
          ((eq? (car seq) 'S)
            (if (or (null? (cdr seq)) (null? (cddr seq)) (null? (cdddr seq))) seq
                (let ((p1 (cadr seq))
                          (p2 (caddr seq))
                          (p3 (cadddr seq))
                          (rest (cddddr seq)))
                        (expand-combinator-one (construct-S (expand-combinator-one p1)
                                         (expand-combinator-one p2)
                                         (expand-combinator-one p3)
                                         rest)))))
          ((eq? (car seq) 'K)
            (if (or (null? (cdr seq)) (null? (cddr seq))) seq
                (let ((p1 (cadr seq))
                          (p2 (caddr seq))
                          (rest (cdddr seq)))
                  (let ((expandedK (expand-combinator-one p1)))
                        (cond ((and (null? rest) (not (pair? expandedK))) expandedK)
                                        (else
                                                (expand-combinator-one
                                                  (if (pair? expandedK)
                                                          `(,@expandedK ,@rest)
                                                          `(,expandedK ,@rest)))))))))
          ((eq? (car seq) 'I)
                (expand-combinator-one (cdr seq)))
          ((and (null? (cdr seq)) (symbol? (car seq))) (car seq))
          (else
                (map expand-combinator-one seq))))))
 
 
(define (expand-combinator l)
  (let ((result (expand-combinator-one l)))
        (if (and (pair? result) (null? (cdr result)) (symbol? (car result)))
          (car result)
          result)))

(expand-combinator '(S (K S) K x y z)) => (x (y z))

これを行なうベータ簡約については、何かの本を斜め読みしたとき、簡約戦略(同時に簡約出来る部分があるような式のどこから簡約すんのかとか)がどうのこうので面倒くさいなと思ったような気もする。

上のプログラムは単純にひたすら頭から簡約して、やることなくなったら、途中の式を簡約に行くという単純なシロモノ。
動いてるから気にしない。。。

とはいえ、

S (式1) (式2)
というのを簡約した結果
S (式1') (式2') (式3)
になるような場合に対応出来ない？
そもそもそんなこと起りえない？

うーん？
よくよく見たら、((式1) (式2)) みたいなのに対応してないか。