p.269(とp262)の append の定義が分かりにくいので整理する
① 任意のリスト y について、空リストと y を append すると y になる ② 任意のu,v,y,zについてv,yをappendしてzになるなら (cons u v) と y をappend すると(cons u z) になる。
この手の"性質を列挙した定義"を公理的定義という。
公理的定義に出てくる変数には必ず"何である"という説明が必要だが、まず ② はこの説明が不足している。
正しくは
② 任意のリスト若しくは任意の単一オブジェクト u、 (← u は本当になんでもよい) 任意のリスト v,y,z について (← v,y,zはリストに限る) v,y をappendして z になるなら (cons u v) と y をappend すると、(cons u z) になる。
次に ②の長ったらしくて何を言っているかわからない説明部分を整理してみる。
②の説明部分の整理 (append v y) = z ならば (append (cons u v) y) = (cons u z) ... (a)
"ならば"の左辺を右辺に代入すると
②の説明部分の整理 (append (cons u v) y) = (cons u (append v y)) ... (b)
となる。もちろん逆に (b) から (a) も言えるので (a) と (b) は同値である。
結局、z はあってもなくてもよいただの中間変数であることがわかる。
まとめると append の公理的定義は
① 任意のリスト y について、(append '() y) = y
② 任意のリスト若しくは任意の単一オブジェクト u、
任意のリスト v , y について
(append (cons u v) y) = (cons u (append v y))
となる。(①もちょっと整理してみた。意味は同じ)
この定義だと、意味も明白に分かる。②の言わんとすることは cons してから append しても、append してから cons しても結果は同じといっている。つまり append の性質として cons と append の交換可能性を 述べているのである。