Ex. 4.61
next-to ルールを 「AならばB」の書き方にして、公理的定義にしてみる。
① x next y in (x (cons y u)) ② x next y in z ならば x next y in (cons v z)
となる。①はリストの先頭のペアは隣接しているという性質を表す。②は、x, y が z 内で隣接してるなら、x, y は(cons v z)内でも隣接しているという性質を表す。リストの中のリストに入り込むような性質の記述はない。
なので
(?x next-to ?y in (1 (2 3) 4))
の出力は
1 next (2 3) (2 3) next 4
である。
(?x next-to 1 in (2 1 3 1))
の出力は
2 next 1 3 next 1
である。
ところで、この問題になんか意味ある?