Reasoned Schemer (28) わり算 続き

次はlの右側の0がなくなる例でやってみよう

もう少し圧縮した書き方で

s -> (splito '(0 0 1 0 1) '(1) l h)
  4 -> (splito '(0 1 0 1) '() '() h), l=()
    2 -> h=(1 0 1), l=()
  6 -> (splito '(0 1 0 1) '() ^l h), l=(0 . ^l), (pos ^l)
    2 -> h=(1 0 1), ^l=()

あれ、同じ答え出た、と思ったらひとつ戻って(pos ^l)に不適合なんだな
ややこしい
でも確かに右側の0が消えた
でもでもまだピンと来ていない

ちゃんと頭の0が取れてるし下位ビットは生きている
けどどうやって頭の0が取れてるのかわからなくてまだぽかーんとしている
左から見ていくから、0を消していいか判断するにはいったん一番右まで見る必要があるはずなんだよな
そこがどうも

そのあたりの違いがわかりそうな例にしてみよう
(splito '(1 0 1 0 1) '(1 1) l h)(0が消えないパターン)と
(splito '(1 0 0 0 1) '(1 1) l h)(0が消えるパターン)を比べたらどうか

消えないパターン

s -> (splito '(1 0 1 0 1) '(1 1) l h)
  5 -> (splito '(0 1 0 1) '(1) '() h), l=(1)
    4 -> (splito '(1 0 1) '() '() h), l=(1)
      適合なし
  6 -> (splito '(0 1 0 1) '(1) ^l h), l=(1 . ^l), (pos ^l)
    4 -> (splito '(1 0 1) '() '() h), l=(1 . ^l), ^l=() => (pos ^l)に不適合
    6 -> (splito '(1 0 1) '() ^^l h), l=(1 0 . ^^l), (pos ^^l)
      2 -> h=(0 1), ^^l=(1) => l=(1 0 1)

消えるパターン

s -> (splito '(1 0 0 0 1) '(1 1) l h)
  5 -> (splito '(0 0 0 1) '(1) '() h), l=(1)
    4 -> (splito '(0 0 1) '() '() h), l=(1)
      2 -> h=(0 1), l=(1)
  6 -> (splito '(0 0 0 1) '(1) ^l h), l=(1 . ^l), (pos ^l)
    4 -> (splito '(0 0 1) '() '() h), l=(1 . ^l), ^l=() => (pos ^l)に不適合
    6 -> (splito '(0 0 1) '() ^^l h), l=(1 0 . ^^l), (pos ^^l)
      2 -> h=(0 1), ^^l=() => (pos ^^l)に不適合

消えないときは6行目の条件で進み、
消える場合は4行目、5行目の条件が使われる、て感じ
4行目、5行目がなぜ頭の0を消す動きになるのか