つづき

上の続き

というわけで、

(oN oN tr n) (oN oN tr m)  --> (exec_tr tr (m_n_mod3 m n)); (oN oN tr (succ m))

に書き換わらないといけないわけだ。

これは

  let.apply_2nd_3rd = abs x, y do
  end
  let.oN_sub = abs oN, tr, x, _y, z do
    ...
  end

を使って

  let.oN = abs my, tr, n, oM do
    oM(apply_2nd_3rd, oN_sub(my, tr), n)
  end

とするとなぜかうまくいく。

(oN oN tr n) (oN oN tr m)
  --> (oN oN tr m) apply_2nd_3rd (oN_sub oN tr) n
  --> apply_2nd_3rd apply_2nd_3rd (oN_sub oN tr) m (oN_sub oN tr) n
  --> oN_sub oN tr m (oN_sub oN tr) n

まあ、動いていればそれでいい。

というわけで、oN_subの実装は

  let.oN_sub = abs oN, tr, x, _y, z do
    exec_tr(tr, m_n_mod3(x, z))
    oN(oN, tr, succ(x))
  end

ということになる。
残っている問題は (m-n)%3 をどうするかだ。