入れ子のかっこ

前回のブログの点記法の続きである. とりあえず練習をしよう. 私の手元のPaul Rosenbloom, The Elements of Mathematical Logic (Dover 1950)に点記法の論理式が沢山出てくる. それでテストしてみた. まずSchemeでBoole値が0と1のnot, or, impを定義する.

(define (not p) (- 1 p))
(define (or p q) (quotient (+ p q 2) 3))
(define (imp p q) (or (not p) q))

テストをするには, mapが便利.

(map not '(0 1)) => (1 0)
(map or '(0 0 1 1) (0 1 0 1)) => (0 1 1 1)
(map imp '(0 0 1 1) '(0 1 0 1)) => (1 1 0 1)

上の本では, 沢山並ぶ -> には特にかっこを(点で)示さない. -> はleft associativeであって, (p -> q -> r) は ((p -> q) -> r) なのだ.

ではやってみよう.

I4 p -> .q -> r. -> .p -> q -> .p -> r
かっこに変えると
((p -> (q -> r)) -> ((p -> q) -> (p -> r)))
Schemeの定義は
(define (i4 p q r)
 (imp (imp p (imp q r)) (imp (imp p q) (imp p r))))
実行
(map i4 '(0 0 0 0 1 1 1 1) '(0 0 1 1 0 0 1 1)
    '(0 1 0 1 0 1 0 1))
=> (1 1 1 1 1 1 1 1)

もう1つ.

T2 q -> r -> .p -> q -> .p -> r
かっこに変えると
((q -> r) -> ((p -> q) -> (p -> r)))
Schemeの定義は
(define (t2 p q r)
 (imp (imp q r) (imp (imp p q) (imp p r))))
実行
(map t2 '(0 0 0 0 1 1 1 1) '(0 0 1 1 0 0 1 1)
    '(0 1 0 1 0 1 0 1))
=> (1 1 1 1 1 1 1 1)

とうまくいく.

かっこ記法と点記法の変換だが, まずかっこから点へは, すべての2項演算子をかっこでくくることにし, つまり

<primary>==<letter>|(<expression>)
<expression>==<primary>|<expression>*<expression>

だけとする. expressionの例は a, a * b, (a * b) * c, ...など.

expression * expression を点記法にするには, expression' lp * rp expression とする. expression'はexpressionを点記法に変えたものである. lpとrpは, 左右のexpressionをひとまとまりにする点である. lpは左のexpression'で使った最大の右点の数より多く, rpは右のexpressionで使った最大の左点の数より多くなければならない. 従って, 下請けの変換は, expression'を返すと同時に, 自分の使った右点, 左点を返すことにする.

letterの場合は, letterの他に, 右点,左点として, 0,0を返す.

* の場合は, 左の式を変換て置き, その右点+1の左点を置き, 演算子を置き, 右の式を変換し, その左点+1の右点を置き, 右の式を置く. また自分で使った左点, 右点も返す.

(define (dotconv exp)
(display (list exp))
(if (symbol? exp) (list '(0 0) exp)
(let* ((l (dotconv (car exp)))
       (r (dotconv (caddr exp)))
       (op (cadr exp))
       (rlp (+ (cadar l) 1))
       (le (cadr l))
       (lrp (+ (cadar r) 1))
       (re (cadr r)))
       (list (list rlp lrp)(list le rlp op lrp re)))))


(dotconv 'a) => ((0 0) a)
(dotconv '(a * b)) => ((1 1) (a 1 * 1 b))
(dotconv '((a * b) * c)) => ((2 1) ((a 1 * 1 b) 2 * 1 c))
(dotconv '((a * b) * (c * d))) => 
   ((2 2) ((a 1 * 1 b) 2 * 2 (c 1 * 1 d)))

この後は ((a 1 * 1 b) 2 * 2 (c 1 * 1 d)) を a * b . * . c * d にしたい. flattenし, 整数はそれ引く1の点を出力する.

(flatten '((a 1 * 1 b) 2 * 2 (c 1 * 1 d))) => (a 1 * 1 b 2 * 2 c 1 * 1 d)

(define (convstream l)
 (apply string-append (apply append
  (map (lambda (x)
   (list (if (number? x) (make-string (- x 1) #\.)
             (symbol->string x)) " "))
       (flatten l)))))

(convstream '((a 1 * 1 b) 2 * 2 (c 1 * 1 d)))

(define (par->dot exp) (convstream (cdr (dotconv exp))))

(par->dot 'a) => "a "
(par->dot '(a * b)) => "a  *  b "
(par->dot '((a * b) * c)) => "a  *  b . *  c "
(par->dot '((a * b) * (c * d))) => "a  *  b . * . c  *  d "

一方, 私の考えた逆変換はこうだ.

1.(((a * b) * (c * d)) * ((e * f) * (g * h)))
2."a * b . * . c * d .. * .. e * f . * . g * h "

                       1 1 1 1 1 1 1 1 1 1 2 2 2 2 2 2 2 2 2
   0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8
3.(a 0 * 0 b 1 * 1 c 0 * 0 d 2 * 2 e 0 * 0 f 1 * 1 g 0 * 0 h)
4.29
5.((-1 5) (-1 13) (15 21) (23 29) (15 29) (7 13))
6.(< < < a * b > * < c * d > > * < < e * f > * < g * h > > >)
7.(((a * b) * (c * d)) * ((e * f) * (g * h)))

上の例で, 1. は元のかっこ記法の式. 2. はそれを点記法にしたもの. 逆変換はここから始まる. まず各演算子に左点と右点があるものとし, 3のように変換する. その上の2行は, 各要素の位置を示す. 0から28まであるから, lengthをとると, 4. のように, 29.

位置 1,5,9,..のように, 4を法として1の位置は左点. 3の位置は右点である. さらに, 演算子は2(mod 4), 変数は0(mod 4)である.

次に各右点>0にはこの右方にある相棒の左点を探し, また左点>0にはこの左方にある右点を探し, 対にする. 上の例では 5. が対のリストである. この読み方は, 5の位置の左点を越える右点は, 左方にはないので, -1とし, (-1 5)とする. 13の位置の左点も同じ. 21の位置の左点は, 15の位置の右点の方が大きいので, スコープはここまでとなり, (15 21)が出来る. 3. と5. の情報から, 6. を作るのだが, (-1 5)のような対があれば, -1に左かっこ, 5に右かっこを置く. この挿入で, 位置がずれると困るから, 挿入は番号の多い右端から行う. 右かっこと左かっこの区別は, 4を法とした剰余の1か3で決る. まだこの段階は記号列であるが, 通常のかっこを記号として挿入すると, 分かり難いから, 角かっこを使っている. 出来たのは6. である.後は, 入れ子の式の読込みルーチンを書けばよい. それにより, 7. が得られる.

(define (iconv s)  ;2. -> 3.
 (define (char->symbol c)
  (string->symbol (list->string (list c))))
 (define (reads n s)
  (cond ((null? s) s)
        ((char=? (car s) #\Space) (reads n (cdr s)))
        ((char=? (car s) #\.) (reads (+ n 1) (cdr s)))
        (else (cons n
          (cons (char->symbol (car s)) (reads 0 (cdr s)))))))
 (let ((ss (string->list s)))
   (cons (char->symbol (car ss)) (reads 0 (cdr ss)))))

(define (makepair s)  ;3. -> 5.
 (let ((len (length s)) (ps '()))
  (do ((i 3  (+ i 4))) ((>= i len))
   (let ((r (list-ref s i)) (k len))
    (do ((j (- len 4) (- j 4))) ((< j i))
     (let ((l (list-ref s j)))
      (if (< r l) (set! k j))))
    (if (> (- k i) 2) (set! ps (cons (list i k) ps)))))
  (do ((i (- len 4) (- i 4))) ((< i 0))
   (let ((l (list-ref s i)) (k -1))
    (do ((j 3 (+ j 4))) ((> j i))
     (let ((r (list-ref s j)))
      (if (> r l) (set! k j))))
    (if (> (- i k) 2) (set! ps (cons (list k i) ps)))))
  ps))

(define (makestr ps s len)   ;5. 3. (length 3) -> 6.
 (define (insert l n a)
  (if (<=  n 0) (cons a l)
   (cons (car l) (insert (cdr l) (- n 1) a))))
 (set! ps (sort (apply append ps) >))
 (for-each (lambda (x) (set! s (insert s x
   (if (= (modulo x 4) 3) '< '>))))  ps)
 (append '(<) (filter symbol? s) '(>)))

(define (str->sexp str) (define i 0)  ;6. -> 7.
 (define (getch) (let ((ch (list-ref str i)))
   (set! i (+ i 1)) ch))
 (define (read) (let ((ch (getch)))
  (cond ((eq? ch '<) (readtail))
        ((eq? ch '>) '())
        (else ch))))
 (define (readtail) (let ((x (read)))
  (if (null? x) x (cons x (readtail)))))
 (read))