>>970
レスありがとうございます。

＞P154のweight*をよく見ると、(× weight* (first pora)) 2)、というのがあって２倍している。
説明不足でした。意味不明と書いたのは、以下のとおりです。

何かを減らしていくことでgoalに近づくというのは理解できます。
ただ、align関数とは何の関係も無いと思えるweight*関数の説明を
持ち出すことが、align関数のtotal function性(無限ループにはならない関数)
の証明になっているのかがピンときません。
align関数の中でlength*関数やweight*関数を使っているわけではないので。
（もちろん、length*関数、weight*関数それぞれの動作は理解できます。）