定理証明手習い (82) 式の置き換え

(find-focus-at-direction dir e) 式eの、dirで指定された部分式

dirがeの適切な位置を示しているかはまったく気にしてない模様
'Qって指定されたけどそもそもeはifじゃないとか
'3って指定されたけど引数が2個しかないとか
そういうの

ところで、関数型プログラミングの関数に動詞が使われてるのはちょっと雰囲気に合わない気が

するんですがどうでしょうか

> (find-fucus-at-direction 'Q '(cons 'a 'b))
'a

(rewrite-focus-at-direction dir e1 e2) 式eの、dirで指定された部分式をe2に置き換える

(focus-is-at-direction? dir e) dirが、式eの正しい部分式を指しているか

たぶんこれでいったんチェックしてからfind-focus-at-directionを使うんだな
関数名は「指定された方向にフォーカスがあるか？」って読めるけどちょっと違う気がする
この場合、自分が違っているとしか思えないけど

(focus-is-at-path? path e) pathが、式eの正しい部分式を指しているか

pathはdirのリスト

(find-focus-at-path path e) 式eの、pathで指定された部分式

(rewrite-focus-at-path path e1 e2) 式eの、pathで指定された部分式をe2に置き換える

少しややこしい

pathが'()じゃないときのこの部分

(rewrite-focus-at-direction
  (car path) e1
  (rewrite-focus-at-path
    (cdr path)
    (find-focus-at-direction (car path) e1)
    e2))

e1の、(car path)が指す部分式を、
e1の、(car path)が指す部分式の(cdr path)が指す部分式をe2で置き換えた式で
置き換える

(cons 'a (cons 'b 'c))の(2 1)が指す部分式を'dで置き換えるとするなら

(cons 'a (cons 'b 'c))の2が指す部分式、つまり(cons 'b 'c)を、
(cons 'b 'c)の(1)が指す部分式、つまり'bを'dで置き換えた式、つまり(cons 'd 'c)で
置き換える

で(cons 'a (cons 'd 'c))ができる、と
理解した

kb84tkhrのブログ