第 １ ３ 章 プ ロ グ ラ ム の 実 行 過 程
１ ． ル ー ル の 分 類
ル ー ル は 、 一 般 に
＜ ヘ ッ ド ＞ ＜ 条 件 部 ＞ ‑‑> ＜ ボ デ ィ ＞.
の 形 で 表 す こ と が で き る 。 ＜ 条 件 部 ＞ は な い 場 合 も あ る 。 よ っ て 、 条 件 部 の 有 無 か ら ル ー ル を ２ 種 類 に 分 類 で き る 。
・ 条 件 部 が あ る ル ー ル ・ 条 件 部 が な い ル ー ル
ま た 、 ル ー ル 中 に 出 現 す る 変 数 に 注 目 し 、 ヘ ッ ド に は 用 い ら れ て い な い 変 数 が 、 条 件 部 や ボ デ ィ に 出 現 し て い る か 否 か を 判 断 す る と 、 ル ー ル を 2種 類 に 分 類 す る こ と が で き る 。 こ の よ う に 条 件 部 や ボ デ ィ に の み 出 現 す る 変 数 を中 間 変 数と い う 。
・ 中 間 変 数 が あ る ル ー ル
・ 中 間 変 数 が な い ル ー ル
こ れ ら の 組 み 合 わ せ に よ り 、 ル ー ル は 次 の ４ 種 類 に 分 類 さ れ る 。
・ 条 件 部 が な く 、 中 間 変 数 が な い ル ー ル
・ 条 件 部 が あ り 、 中 間 変 数 が な い ル ー ル
・ 条 件 部 が な く 、 中 間 変 数 が あ る ル ー ル
・ 条 件 部 が あ り 、 中 間 変 数 が あ る ル ー ル
ル ー ル の 意 味 を 次 節 で こ の ４ 種 類 に 分 け て 説 明 す る 。
２ ． ル ー ル の 意 味
ル ー ル と は 、 直 感 的 に は 質 問 の 確 定 節 を 書 き 換 え る 規 則 で あ る 。 １ つ の 書 き 換 え は １ つ の ア ト ム を ア ト ム 列 （ ０ 個 以 上 、 任 意 個 ） に 直 す こ と で あ る 。 こ の ア ト ム と ア ト ム 列 の ペ ア を書 き 換 え ペ アと 呼 ぶ 。 書 き 換 え は 簡 単 化 で あ る こ と が 多 い の で 、 そ の 場 合 に は簡 単 化 ペ アと も 呼 ぶ 。 ル ー ル の 意 味 は 、 そ の ル ー ル に よ っ て 可 能 な 書 き 換 え ペ ア （ 簡 単 化 ペ ア ） 全 体 の 集 合 で あ る 。 こ の こ と に つ い て 、 例 を 用 い て 説 明 し よ う 。
(1) 条 件 部 が な く 、 中 間 変 数 が な い ル ー ル
リ ス ト の 最 後 の 要 素 を 求 め る た め に 、 以 下 の ル ー ル を 用 い る こ と が で き る 。
(last (*A *B￨*X) *Y) ‑‑> (last (*B￨*X) *Y).
こ の ル ー ル を 例 と し て 、 条 件 部 が な く 、 中 間 変 数 が な い ル ー ル の 意 味 を 説 明 す る 。 例 え ば 変 数 *A、*B、*X、*Y に 対 し て 、 そ れ ぞ れ １ 、 ２ 、(３)、*Z を 代 入 す る と 、 ル ー ル は 次 の よ う に 具 体 化 さ れ る 。
(last (1 2 3) *Ｚ ) ‑‑>(last (2 3) *Ｚ ).
こ の ル ー ル か ら 、 次 の 簡 単 化 ペ ア を 得 る こ と が で き る 。
(last (1 2 3) *Ｚ ) ⇒ (last (2 3) *Ｚ ).
こ れ は ア ト ム (last (1 2 3) *Ｚ ) を 、 ア ト ム (last (2 3) *X) に 置 き 換 え て よ い こ と を 意 味 す る 。 同 様 に 代 入｛ *A/ａ , *Ｂ /ｂ , *Ｘ /(c d e), *Y/*Ｚ ｝を 行 う と 、 ル ー ル は 具 体 化 さ れ て 次 の 簡 単 化 ペ ア を 得 る 。
(last (a b c d e) *Ｚ ) ⇒ (last (b c d e) *Ｚ ).
こ の よ う に 、 ル ー ル に い ろ い ろ な 代 入 を 施 す こ と に よ り 、 さ ま ざ ま な 簡 単 化 ペ ア が 得 ら れ る 。 上 記 の ル ー ル の 意 味 と は 、 そ の よ う に し て 得 ら れ る 簡 単 化 ペ ア 全 体 の 集 合 で あ る 。
(2) 条 件 部 が あ り 、 中 間 変 数 が な い ル ー ル
リ ス ト の 要 素 の 最 大 値 を 求 め る た め に 、 以 下 の ル ー ル を 用 い る こ と が で き る 。
(maxlist (*A *B￨*X) *Y),{(> *A *B)} ‑‑> (maxlist (*A￨*X) *Y).
こ の ル ー ル を 例 と し て 、条 件 部 が あ り 、中 間 変 数 が な い ル ー ル の 意 味 を 説 明 す る 。変 数 *A、
*B、*X、*Y に 対 し て 、そ れ ぞ れ ５ 、３ 、(7 2 1)、*Z を 代 入 す る と 、ル ー ル は 次 の よ う に 具 体 化 さ れ る 。
(maxlist (5 3 7 2 1) *Ｚ ),{(> 5 3)} ‑‑> (maxlist (5 7 2 1) *Ｚ ).
条 件 部 (> 5 3) が 真 で あ る の で 、 次 の 簡 単 化 ペ ア を 得 る こ と が で き る 。 (maxlist (5 3 7 2 1) *Ｚ ) ⇒ (maxlist (5 7 2 1) *Ｚ ).
一 方 、こ の ル ー ル の 変 数 に 対 し て 、代 入{ *A/4, *B/9, *X/(5 8 3), *Y/*Z}を 行 う と 、 ル ー ル は 次 の よ う に 具 体 化 さ れ る 。
(maxlist (4 9 5 8 3) *Ｚ ),{(> 4 9)} ‑‑> (maxlist (9 5 8 3) *Ｚ ).
し か し 、 条 件 部 (> 4 9) が 偽 の た め に 、 簡 単 化 ペ ア は 得 ら れ な い 。
上 記 の ル ー ル の 意 味 と は 、 ル ー ル に 代 入 を 施 し 、 条 件 部 が 真 の と き に 作 ら れ る 簡 単 化 ペ ア 全 体 の 集 合 で あ る 。
(3) 条 件 部 が な く 、 中 間 変 数 が あ る ル ー ル
リ ス ト の 長 さ を 求 め る た め に 、 以 下 の ル ー ル を 用 い る こ と が で き る 。
(length (*A￨*X) *Y) ‑‑> (length *X *Y2),(:= *Y1 (+ 1 *Y2)).
こ の ル ー ル を 例 と し て 、 条 件 部 が な く 、 中 間 変 数 が あ る ル ー ル の 意 味 を 説 明 す る 。 こ の ル ー ル の 変 数 に 対 し て 、 代 入{*A/2, *X/(3 5 1 6), *Y/*Y1, *Y1/*Y2} を 行 う と 、 ル ー ル は 具 体 化 さ れ 、 次 の よ う な 簡 単 化 ペ ア が 得 ら れ る 。
(length (2 3 5 1 6) *Y) ⇒ (length (3 5 1 6) *Y1),(:= *Y (+ 1 *Y1)).
*Y1 は ３ ５ １ ６ の 長 さ を 保 持 し 、 後 の １ を 足 す 計 算 に 渡 す た め に 使 わ れ る の で 、 変 数 で な け れ ば な ら な い 。ま た 、そ れ が 他 の 変 数 、例 え ば*Yと 同 じ も の で あ る と 、明 ら か に 矛 盾 が 生 じ て し ま う の で 、 他 の 変 数 と 重 複 し な い 変 数 を 使 う 必 要 が あ る 。
こ こ で 重 要 な の は 、ヘ ッ ド に 出 現 す る 変 数 に は 、任 意 の 項 を 代 入 で き る が 、中 間 変 数（ こ の ル ー ル で は *Y1 の こ と で あ る ） に は 変 数 し か 代 入 で き な い と い う こ と で あ る 。 例 え ば 、 代 入｛ *A/ａ , *X/(ｂ ｃ ), *Y/*Ｚ , *Y1/3｝を 行 う と 、 ル ー ル は 次 の よ う に 具 体 化 さ れ る 。
(length (a b c) *Ｚ ) ‑‑> (length (b c) 3),(:= *Ｚ (+ 1 3)).
し か し 、 こ れ は 「 誤 っ た 具 体 化 」 な の で 、 簡 単 化 ペ ア を 得 る こ と は で き な い 。
上 記 の ル ー ル の 意 味 は 、「 中 間 変 数 に は 、（ 他 の 変 数 と 重 複 し な い ） 変 数 し か 代 入 で き な い 」 と い う 制 限 の も と で 得 ら れ る 簡 単 化 ペ ア 全 体 の 集 合 で あ る 。
(4) 条 件 部 が あ り 、 中 間 変 数 が あ る ル ー ル
リ ス ト か ら 偶 数 の 要 素 の 出 現 回 数 を 求 め る た め に 、以 下 の ル ー ル を 用 い る こ と が で き る 。
(even̲appear (*A￨*X) *Y),{(even *A)} ‑‑> (even̲appear *X *Y1),(:= *Y (+ 1 *Y1)).
こ こ で 、 条 件 部 を 計 算 す る た め の ル ー ル は 次 の よ う に 与 え ら れ て い る も の と す る 。
(even *A) ‑‑> (:= *M (mod *A 2)),(== *M 0).
こ の ル ー ル を 例 と し て 、 条 件 部 が あ り 、 中 間 変 数 が あ る ル ー ル の 意 味 を 説 明 す る 。 例 え ば 代 入{*A/2, *X/(3 5 8), *Y1/*Z1, *Y/*Z}を 行 う 。*Z は 中 間 変 数 な の で 、 他 に 出 現 し な い 変 数 し か 代 入 で き な い こ と に 注 意 し な さ い 。 こ の 代 入 に よ っ て ル ー ル は 次 の よ う に 具 体 化 さ れ る 。
(even̲appear (2 3 5 8) *Z),{(even 2)} ‑‑> (even̲appear (3 5 8) *Z1),(:= *Z (+ 1 *Z1)).
こ の 条 件 部 (even 2) は 上 記 の ル ー ル で 計 算 さ れ て 真 と な る の で 、 次 の 簡 単 化 ペ ア を 得 る こ と が で き る 。
(even̲appear (2 3 5 8) *Z) ⇒ (even̲appear (3 5 8) *Z1),(:= *Z (+ 1 *Z1)).
３ ． プ ロ グ ラ ム の 実 行 過 程
質 問 を 入 力 し た と き 、 計 算 機 の 中 で は ど の よ う な 計 算 が な さ れ る の だ ろ う か 。 本 章 で は 質 問 と ル ー ル 集 合 と が 作 り 出 す 計 算 の 過 程 に つ い て 説 明 す る 。
(1) yes−no判 定 問 題
(even 2) が 真 で あ る こ と を 判 定 す る た め に 、 次 の よ う な 計 算 を 行 う 。 最 初 に 、
(ans) <‑‑ (even 2). と い う 節 を 考 え る 。 こ の 節 の 意 味 は 、「 ２ が 偶 数 で あ る な ら ば 、 そ れ は 答 で あ る 」 と い う こ と で あ る 。
こ の ans節 を ル ー ル に よ っ て 次 の よ う に 簡 単 化 す る 。
(ans) <‑‑ (even 2).
(ans) <‑‑ (:= *M (mod 2 2)),(== *M 0).
(ans) <‑‑ (== 0 0).
(ans) <‑‑.
最 後 に 得 ら れ た 節 は 、「 無 条 件 で 、そ れ は 答 で あ る 」と 読 め る 。し た が っ て 、(even 2) は 、 正 し い こ と が わ か る 。こ の よ う に yes、no を 判 定 す る 問 題 は 、問 題 に 相 当 す る ans 節 を 作 り 、 ル ー ル で 変 更 す る こ と に よ っ て 解 決 さ れ る 。 こ の 問 題 の 簡 単 化 に は 、
簡 単 化 ペ ア ：(even 2) ⇒ (:= *M (mod 2 2)),(== *M 0).
が 使 わ れ て い る 。
(2) ボ デ ィ ア ト ム 列 の サ イ ズ が １ 以 下 で あ る 実 行 列
例 題 と し て リ ス ト の 最 後 の 要 素 を 求 め る 問 題 を 考 え る 。 こ の 問 題 を 解 く プ ロ グ ラ ム を 以 下 の ２ つ の ル ー ル で 構 成 し た と す る 。
(last (*A *B￨*X) *Z) ‑‑> (last (*B￨*X) *Z). ･･････ ル ー ル A (last (*A) *Z) ‑‑> (= *Z *A). ･･････ ル ー ル B
質 問（ last (1 2 3 4 5) *Y）を 入 力 す る と 、 シ ス テ ム の 内 部 に は 、 最 初 に 以 下 の よ う な ans 節 が 作 ら れ る 。最 初 に 記 述 さ れ る ans 節 を初 期 ans 節と 呼 ぶ 。こ の 初 期 ans 節 が ル ー ル で 次 々 に 変 形 さ れ て い く 。
(ans *Y) <‑‑ (last (1 2 3 4 5) *Y).
こ の ans 節 の 意 味 は 、（ １ ２ ３ ４ ５ ） と い う リ ス ト の 最 後 が Y で あ る な ら ば 、Y は 答 で あ る と い う 意 味 で あ る 。 最 初 に ボ デ ィ の 先 頭 に あ る ア ト ム (last (1 2 3 4 5) *Y) が 選 ば れ る 。 こ の ア ト ム に マ ッ チ す る ヘ ッ ド を 持 つ ル ー ル は ル ー ル A で あ る 。 ル ー ル A に 対 し て 、 代 入{*A/1, *B/2, *X/(3 4 5), *Z/*Y} を 行 う と 、
(last (1 2￨(3 4 5)) *Y) ⇒ (last (2￨(3 4 5)) *Y).
と い う 簡 単 化 ペ ア が 得 ら れ る 。そ の 簡 単 化 ペ ア に よ っ て 初 期 ans 節 は 、新 し い ans 節 に 書 き 換 え ら れ る 。
(ans *Y) <‑‑ (last (2 3 4 5) *Y).
次 に 、(last (2 3 4 5) *Y) が 選 ば れ 、 再 び ル ー ル A が 使 わ れ る 。
代 入 ＝｛ *A/2, *B/3, *X/(4 5), *Z/*Y｝
簡 単 化 ペ ア ：(last (2 3￨(4 5)) *Y) ⇒ (last (3￨(4 5)) *Y).
そ の 結 果 ans 節 は 、 以 下 の よ う に 書 き 換 え ら れ る. (ans *Y) <‑‑ (last (3 4 5) *Y).
さ ら に 、 リ ス ト の 長 さ が １ に な る ま で 、 同 様 に ル ー ル の 適 用 が 繰 り 返 さ れ る 。
(ans *Y) <‑‑ (last (4 5) *Y).
(ans *Y) <‑‑ (last (5) *Y).
そ し て 、 リ ス ト の 長 さ が １ に な っ た と き 、 ル ー ル B が 適 用 さ れ る 。 簡 単 化 ペ ア ：(last (5) *Y) ⇒ (= *Y 5).
こ の 簡 単 化 ペ ア に よ っ て 、ans 節 は 次 の よ う に 書 き 換 え ら れ る.
(ans *Y) <‑‑ (= *Y 5).
こ こ で ア ト ム (= *Y 5) が 選 ば れ る 。 ＝ は 組 み 込 み 述 語 な の で 、 こ の ＝ ア ト ム の 計 算 は 、 シ ス テ ム で あ ら か じ め 決 め ら れ た 手 順 で 行 わ れ る 。す な わ ち*Y に ５ が 代 入 さ れ 、ア ト ム (=
*Y 5) は 消 滅 す る 。 こ の と き ans ア ト ム 中 の*Y も ５ と な る 。 こ う し て 、ans節 は 次 の よ う に な る 。
(ans 5) <‑‑ .
こ れ は 、 求 め る 答 え が ５ で あ る こ と が わ か る 。
(3) ボ デ ィ ア ト ム 列 の サ イ ズ が 変 化 す る 実 行 列
リ ス ト の 長 さ を 求 め る ル ー ル は 以 下 の よ う に 表 さ れ る 。
(length ( ) *Y) ‑‑> (= *Y 0). ･･････ ル ー ル A (length (*A￨*X) *Y) ‑‑> (length *X *Z),(:= *Y (+ 1 *Z)). ･･････ ル ー ル B 質 問 (length (a b c) *Z) を 入 力 す る と 、 以 下 の よ う な ans 節 が 作 ら れ る 。
(ans *Z) <‑‑ (length (a b c) *Z).
最 初 に (length (a b c) *Z) が 選 ば れ る 。 こ の ア ト ム に マ ッ チ す る ヘ ッ ド を 持 つ ル ー ル は ル ー ル B で あ る 。 代 入{*A/ａ , *X/(b c), *Y/*Y, *Z/*Y1} を 行 う と 、 次 の 簡 単 化 ペ ア が 得 ら れ る 。
(length (a￨(b c)) *Y) ⇒ (length (b c) *Y1),(:= *Y (+ 1 *Y1)).
そ の 結 果 、ans 節 は 以 下 の よ う に 書 き 換 え ら れ る.
(ans *Y) <‑‑ (length (b c) *Y1),(:= *Y (+ 1 *Y1)).
以 下 同 様 に し て 、ans節 が 書 き 換 え ら れ る 。
(ans *Y) <‑‑ (length (c) *Y2),(:= *Y1 (+ 1 *Y2)), (:= *Y (+ 1 *Y1)).
(ans *Y) <‑‑ (length ( ) *Y3),(:= *Y2 (+ 1 *Y3)),(:= *Y1 (+ 1 *Y2)),(:= *Y (+ 1 *Y1)).
こ こ で 選 択 さ れ た ア ト ム (length ( ) *Y1) は ル ー ル A に マ ッ チ す る 。 簡 単 化 ペ ア ：(length ( ) *Y3) ⇒ (= *Y3 0).
そ の 結 果 、ans 節 は 以 下 の よ う に 書 き 換 え ら れ る 。
(ans *Y) <‑‑ (= *Y3 0), (:= *Y2 (+ 1 *Y3)) ,(:= *Y1 (+ 1 *Y2)), (:= *Y (+ 1 *Y1)).
こ の よ う に ボ デ ィ の 先 頭 の ア ト ム が 書 き 換 え ら れ る こ と に よ り 、 ボ デ ィ の 残 り の ア ト ム は ど ん ど ん た ま っ て ゆ く 。 こ こ で は (:= *Yi (+ 1 *Yj )) の 形 の ア ト ム が 蓄 え ら れ る 。 本 節 で は 蓄 え ら れ た ア ト ム を 下 線 で 示 し て い る 。
上 記 の ans 節 で は 、ボ デ ィ の 述 語 は 全 て 組 み 込 み 述 語 と な る 。組 み 込 み 述 語 を 持 つ ア ト ム は 計 算 さ れ て 消 滅 す る の で 、 こ こ か ら は ボ デ ィ ア ト ム の 数 は 順 次 減 少 し て い く 。
(ans *Y) <‑‑ (:= *Y2 (+ 1 0)) ,(:= *Y1 (+ 1 *Y2)), (:= *Y (+ 1 *Y1)).
(ans *Y) <‑‑ (:= *Y1 (+ 1 1)), (:= *Y (+ 1 *Y1)).
(ans *Y) <‑‑ (:= *Y (+ 1 2)).
最 後 に (:= *Y (+ 1 2)) を 計 算 し 、*Y＝3 と な り ansア ト ム の*Yも 3と な っ て 、 ア ト ム (:= *Y (+ 1 2)) は 消 滅 す る 。 そ の 結 果 、 次 の ans 節 が 得 ら れ る 。
(ans 3) <‑‑.
４ ． ル ー ル の 意 味 と 実 行 過 程
ル ー ル は 意 味 を 決 定 し 、 そ の 意 味 に し た が っ て 実 行 さ れ る 。 こ の 全 体 像 を も う 一 度 別 の 例 で 確 認 す る 。 例 え ば リ ス ト の 要 素 の 最 大 値 を 求 め る ル ー ル は 以 下 の よ う に 表 す こ と が で き る 。
(maxlist (*A) *Z) ‑‑> (= *Z *A). ･･･ ル ー ル A (maxlist (*A *B￨*X) *Z),{(> *A *B)} ‑‑> (maxlist (*A￨*X) *Z). ･･･ ル ー ル B (maxlist (*A *B￨*X) *Z),{(<= *A *B)} ‑‑> (maxlist (*B￨*X) *Z). ･･･ ル ー ル C
そ れ ぞ れ の ル ー ル か ら 作 ら れ る 簡 単 化 ペ ア の 例 を 列 挙 す る 。
・ ル ー ル A
A1 (maxlist (6) *Y) ⇒ (= *Y 6).
A2 (maxlist (3) *Y) ⇒ (= *Y 3).
A3 (maxlist (10) *Y) ⇒ (= *Y 10).
A4 (maxlist (7) *Y) ⇒ (= *Y 7).
A5 (maxlist (8) *Y) ⇒ (= *Y 8).
・ ル ー ル B
B1 (maxlist (7 5) *Y) ⇒ (maxlist (7) *Y).
B2 (maxlist (8 4 3 2 5) *Y) ⇒ (maxlist (8 3 2 5) *Y).
B3 (maxlist (6 1 3) *Y) ⇒ (maxlist (6 3) *Y).
B4 (maxlist (8 7 4 9) *Y) ⇒ (maxlist (8 4 9) *Y).
B5 (maxlist (5 2 4) *Y) ⇒ (maxlist (5 4) *Y).
・ ル ー ル C
C1 (maxlist (8 9 4 2 3) *Y) ⇒ (maxlist (9 4 2 3) *Y).
C2 (maxlist (6 6 8) *Y) ⇒ (maxlist (6 8) *Y).
C3 (maxlist (2 4 7 5) *Y) ⇒ (maxlist (4 7 5) *Y).
C4 (maxlist (1 3) *Y) ⇒ (maxlist (3) *Y).
C5 (maxlist (4 7 5) *Y) ⇒ (maxlist (7 5) *Y).
質 問 (maxlist (2 4 7 5) *Y) と い う 質 問 を 入 力 す る と 、 上 記 の 簡 単 化 ペ ア の い く つ か に よ っ て 次 の よ う な 計 算 が 起 こ る 。
(ans *Z) <‑‑ (maxlist (2 4 7 5) *Y).
↓ 簡 単 化 ペ ア C３ が 適 用
(ans *Y) <‑‑ (maxlist (4 7 5) *Y).
↓ 簡 単 化 ペ ア C５ が 適 用 (ans *Y) <‑‑ (maxlist (7 5) *Y).
↓ 簡 単 化 ペ ア B1 が 適 用 (ans *Y) <‑‑ (maxlist (7) *Y).
↓ 簡 単 化 ペ ア A4 が 適 用 (ans *Y) <‑‑ (= *Y 7).
↓ 組 み 込 み ル ー ル に よ る 処 理 (ans 7) <‑‑ .
