Ex. 4.68
まず簡単な手書き実験で reverse の性質を探ってみる。ヒントの append 云々を考慮して、、、
1. (reverse ()) = () とか 2. (reverse a) = a とか 3. (reverse (a)) = (a) とか 4. (reverse (a b) = (b a)とか 5. (reverse (a b c)) = (c b a)とか 6. (reverse (append (a b) (c))) = (append (c) (reverse (a b))) とか 7. (reverse (append (a b) (c d))) = (append (reverse (c d)) (reverse (a b))) とか 8. (reverse (cons a (b c))) = (append (reverse (b c)) (a)) とか ...
6.と7.と8.は、append の定義で使った cons と append の交換可能性に似ている。
また6.と7.と8.は、結局どれも同じ性質を表しているような気がする、、、ただ 7. は rule の実装のせいで無限ループしてしまう。
4.と5.は要素数をN個にしようとすると結局 6.、7.、8.になりそうな予感。
1.と2.と3.は初期値としてどれでもいいような、、、ただ空リストとか、リストでないものの reverse というのも意味がないかも。とまあこのへんは趣味。
ということで、3.と6.を採用して、reverse の公理的定義を作ってみる。
①単一要素のリスト(a)について、(reverse (a)) = (a) である。 ②単一要素のリスト(c)と任意のリスト x について、 (reverse (append x (c))) = (append (c) (reverse x))である。
②はこのままだと rule 形式にできないので、また中間変数を導入して言い換える。
②単一要素のリスト(c)と任意のリスト x, z, v, w について、 (append x (c)) = z かつ (reverse x) = v かつ (append (c) v) = w ならば (reverse z) = w である。
この①と②をrule形式になおす。
①(rule (reverse (?a) (?a)))
②(rule (reverse ?z ?w)
(and (append-to-form ?x (?c) ?z)
(reverse ?x ?v)
(append-to-form (?c) ?v ?w)))
実行してみる。順方向のreverse
;;; Query input: (reverse (1 2 3) ?) ;;; Query results: (reverse (1 2 3) (3 2 1))
ちゃんと動く。
逆方向のreverseは
;;; Query input: (reverse ? (1 2 3)) .....無限ループ
残念ながら無限ループする。
この場合、全変数が未束縛状態で最初の append-to-form の再帰に突入して無限ループしているようだ。
(reverse (1 2 3) ?) も (reverse ? (1 2 3)) もどちらも無限ループしないような定義があればいいのだが、思いつかなかった。
append-to-form は cons を (a . b) と表現できるので、consを使った条件をruleの結論部分におくことができた。このおかけで順方向、逆方向ともに変数束縛できて、再帰が無限ループしないようになっていた。reverseではこんなラッキーな条件がない。append を rule の結論部に書ければいいがそうもいかない。というところで諦めた。
もっと全然違う切り口の定義、例えば2個の reverse の繰り返しとか、なにかあるかもしれない。