Ex. 4.62
next-to のまねをして定義してみる
① 単一要素リストの last は、そのリスト自体である。 ② x が z 内で last である。ならば、x は (cons v z) 内で last である。
rule に直してみる
① (rule (last-pair (?x) (?x)))
② (rule (last-pair (?v . ?z) ?x)
(last-pair ?z ?x))
実行結果
;;; Query input: (last-pair (3) ?x) ;;; Query results: (last-pair (3) (3)) ;;; Query input: (last-pair (1 2 3) ?x) ;;; Query results: (last-pair (1 2 3) (3)) ;;; Query input: (last-pair (2 ?x) (3)) ;;; Query results: (last-pair (2 3) (3)) ;;; Query input: (last-pair ?x (3)) 無限ループ → どこをどう無限ループしているのか？ 詳しく見ていないが、 「②の本体 last-pair 評価 → last-pair と②の結論部のユニファイ → ②の本体 last-pair 評価 → ・・・ 」 というループに入っている。と思う ②の本体と②の結論部のユニファイが failed になればこのループは止まるが、failed にならないのであろう
公理的定義を行うとき、定義としてどういう性質を採用するのか。決まった方法はない。問題ごとにカットアンドトライで決めるしかない。また、同値な定義が何種類もあったりすると思われる。この問題くらいなら問題ないが、おおきな問題だと定義の選択は非常に難しいと思われる。