$Id: intro_theory.txt,v 1.8 2002/07/29 13:19:37 katsu Exp $ I.この小文の立場 これは、渡邊克宏 が、 「プログラミング言語理論への招待」 二木厚吉監訳, 酒匂寛訳, アスキー出版局, ISBN 4-7561-0317-0 (Bertrand Meyer 原著 原題 "Introduction to the Theory of Programming Languages") を読んで感じたことや気づいた誤り(と思われるもの)を気楽にメモした 読書感想文である。原書を持ってないので、見比べるようなことは全く していない。引用・複写・再配布等は、強く推奨される。最新版は http://katsu.watanabe.name/review/intro_theory.txt にある。 不明のまま残っている点については、原書をお持ちの方はぜひ教えて頂きたい。 その他、御意見御感想等を気軽にお寄せあれ。 なお、原書をお読みになった京都大学の杉山和徳 氏から貴重なコメントをいただいたので、それも織り込んである。 II.凡例 "<" は本文を示し、">" は修正例を示す。修正例は口語だったり冗長だったり するが、正しい修正を示すのは著者・訳者におまかせしたい。 +5L はページの先頭から５行め、-5L はページの最後から5行め、8.1.2章+2L は 8.1.2 章の最初から2行め、3.9.2章-5L は3.9.2 章の 5行前(3.9.2章の最後から 5行ではない)をあらわす。 III. 翻訳の癖 1.「性質」あるいは「特性」という言葉を避けて、ほとんど常に「属性」という 硬い単語を用いている。 2.式を提示した後では、そこが段落の切れ目であるなしに関わらず、必ず段下げが 行なわれてしまっている。通常、p.332 に到って初めてこのことに気がつくと 思われる。(p.140 -9L には例外的に無意味な段下げを避けている事例がある。) 3. ∀X∃Y という X -> Y の関数関係をあらわす時、通常は 「すべての X に対して Y のメンバを関連付ける」 というような日本語を使うが、この本では 「対応する Y のメンバにすべての X を関連付ける」(p.88 -14L) 「Y を任意の X と関連付ける」(p.118 +3L, p.140 -13L) 等の表現を行なっているので注意。このような表現に出くわした時、Y に対して X を割り当てるのだと勘違いしないこと。 4.「いったい我々は何かを定義したのだろうか」という文が数度出てくる。 「いったい我々は何を定義したのだろうか」という意味なのか、それとも 「果たして我々は何かを定義できたのだろうか」という意味なのか曖昧。 再帰に関する文脈では、後者の意味で使われているはずではある。 （「いったいどうしたの？」(普通 What に関する返答が返ってくる)とか、 「どうかしたの？」(普通 Yes/No の返答が返ってくる)とは尋ねるが、 「いったいどうかしたの？」とは尋ねないだろう。） IV. 全体に関する感想 訳者は「オブジェクト指向入門」という Eiffel を題材にしたベストセラー本も 手掛けていますが、そちらよりもむしろこちらの方が重要性は高いし普及した 時の効果も大きいと賢察して、売れないだろうと後込みする編集者を強く 押し切って(訳者には印税は全く入ってこないそうです)翻訳したと聞いています。 これまで、この本のように難しい数学を扱わずに意味論の全体を概観した ものはなく、入門者や大学生の教科書として普及すればよいと思います。 V. 気がついたこと p.15 -8L < Z(ゼット) > Z(ゼッド) Z に詳しい小田君によれば、「Z の FAQ には『ゼッド』と載ってます」 p.29 1.4章最初のパラグラフ < これらの相違は...あらゆる混乱を取り除いてくれるのかと期待されるかも... 相違が、混乱を取り除くとはどういう意味？ 杉山氏によれば、confusion を混乱ではなく混同と訳せばわかりやすかった そうである。 > プログラム言語の世界と数学の世界を明確に分離できる。 p.32 +14L < 論理言語 > 論理型言語 p.35 2.1.4章+3L < given の後には１つ以上のローカル名を定義する。 given の後に現われる定義が複数のローカル名を扱っている場合、 後に現われる定義の中で先立つ定義が参照できる件に言及しなくて よいのか。まあ、p.175 とか p.197 とかの例を読めば自明だが。 p.82 3.8.3章 -2L < Cluase_list > Clause_list p.83 「Clause_list」の列、「ルーチン」のカラム < 連続したルーチン呼び出しを含む。 > 連続したルーチン呼び出しで表現する。 p.83 「Birth」の列、「ルーチン」のカラム < Birth > birth 他の列に合わせて小文字にしたほうがいいと思うが、それ以上の深い意味はない。 p.84 -5L < person("Nikolai", "Rimsky-Korsakov", "Nick") person の short_name(3番めの引数)は Identifier だが、p.83 では Identifier はシングルクオートで囲む約束になっている。だから > person("Nikolai", "Rimsky-Korsakov", 'Nick') でないとまずい。あるいは、Pascal に習って、S (文字列)の具象構文も シングルクオートで囲むことにすべきかもしれない。 p.88 -13L < X の任意の実例個体は対応する集合 Vi のメンバにすべてのタグ ti を < 関連付ける有限関数として考えることができる。 訳の癖 3 参照 p.91 図 横軸に広がる空間(軸の名称)は (A ∪ B ∪ C) か？ p.93 -4L < 最後のエレメントによって > それ以外の残りのエレメントによって p.104 3番めの黒丸 < 集積の規則として、 > 集積の規則に違反しないよう、 p.106 Figure 4-5 の 6行前 < 型 Instruction と Integer_list は個別に定義しなければならない > 型 Instruction と Integer_list は、これとは別に定義しなければならない 現状だと、(文脈を読めない者には、)Instruction と Integer_list の記述を ２つ(別々)にしなければならないという意味にとれる。コードには Instruction や Integer_list の記述が入っていないという意味を強調したい。 p.107 4.2.4章+1L < 任意の特定の > 任意の 日本語として変 p.118 +3L < このような表示...を任意のプログラム p と > 任意のプログラム p に対してこのような表示...を 訳の癖 3 参照 p.120 +1 < MCompound を個別に使用した 個別という意味がわからない。 杉山氏によれば、MCompoundの定義の中で 再び MCompound を使用したという 意味だそうである。 p.120 +1L < 明示的な再帰を避けるための > 明示的な再帰を避けるような p.120 4.5.4章+3 < 状態の概念を操作的関数において明示的にするならば、 > 操作的関数の方は状態の概念を明示的にしたものである一方で、 p.121 4.6章 +8L < 学ぶ > 調べる p.121 -1L < 公式 9章には「公式」という単語は１回も現れないが、本当にこの訳語は正しいのか？ 恐らく整合式のことだと思うけど、この時点だと「式」ぐらいが適当と感じた。 p.124 +2L < このような推論規則の意味は次のことを意味する。 > このような推論規則は、次のことを意味している。 p.125 4.6.3章 -6L < R1 が真の時は > R1 が偽の時は p.127 表の中の 8行目 < FL=<> > F=<> p.128 -1L < IProgram の適用の１つを落せば良い。 適用を落すということの意味がわからない。 > それには、EB の事後条件に残っているレジスタの不要な記述を落し、 > 導出規則の IProgram を１回適用すれば良い。 という意味の文だと思うが正しいか？ p.130 脚注 < 手続き名としての Program > Program というレコード名 p.133 -3L < file へのすべての参照 > register へのすべての参照 p.139 +6L < 高等関数 > 高階関数 p.140 +4L < 作用 確かに application 「作用」と訳す流儀はあるが、 p.28 -11L applicative 適用型 p.150 5.9章 self-application 自己適用 などという訳語(これらの言葉はもちろん lambda calculus の "application" に由来している)の選択と適合しない感じを受ける。また、p.141 +5L や p.148 5.8章 +2L 等の場所に「適用」という言葉が現れている。 p.142 5.5.2章 -3L < "出現(occurs)"とは...仮識別子としてテキストとして存在するだけではない。 > "出現(occurs)"とは...(テキスト中に)仮識別子としてだけ存在するの場合は >含まない。 日本語として変。 p.143 -2L < ラムダ抽象の本体ですでに自由である識別子と、同じ仮識別子を導入する変更は > ラムダ抽象の本体ですでに自由である識別子と同じ仮識別子を導入する変更は、 「と」と「同じ」の間に読点を入れるのは意地悪。 p.148 5.8章 < 契約 ここでの contract という単語は、縮むとか大きさが減じるとかいう意味で 使われているので、「契約」というでは英語の雰囲気を壊している。p.151 +2L 「契約は(その名に反して)実際にこの個数を増大させ」というのも、意味が 全く通じなくなっていると思う。「縮約」「収縮」ではどうか？ 杉山氏によれば、原書では contraction となっていて、これは収縮という 訳語が適当だそうである。 p.151 +2L < その他の場合には、...ものもある。 > 場合によっては、...こともある。 p.152 +6L < 型の言語は非常に単純なので、矢印を使って具体的な記法を維持できる 維持？ > 具体的な記法に矢印を使うことにすると、結合の方向性の約束を定める > などして曖昧さの排除をする必要が出たりするんだけど、それでも > 型の言語は非常に単純だから、複雑になったり扱いにくくなったり > しないよね。だから具象構文は矢印を採用するのがいいねえ。 といった意味でしょう。ひとことでいえば、 > 具体的な記法には矢印を採用すれば十分である。 ぐらいですか？ p.156 -8L < 解決(resolution)メカニズム > 導出(resolution)メカニズム あるいは、導出法、導出原理。 p.140 -14L < 引数が１つの一意な関数...を２つの引数を持つ任意の関数と関連付ける > ２つの引数を持つ任意の関数に対して、引数が１つの一意な関数...を > 関連付ける 訳の癖 3 参照 p.161 typing の定義 < > p161 -9L < { } > {,} p.161 -2L < 型マップの概念はこの性質をうまく表している。 意味がわからなくないか？型マップの概念自体が「この性質」を表すのだろうか？ > 型マップの概念を使うと、この性質(出現の型が、スコープによって異なってる > 状況)をうまく表現できるようになってるよ。 p.163 +1L < 式の妥当性は特定の型マップについてだけ意味を持つため > 式の妥当性は、適当な型マップの存在の元でのみ判定できるので、 p.170 -12L < 狭義性 これは strictness の一般的な訳語なのか？「正格性」「厳格性」というのは 見聞きするが。 p.176 +6L < 表関する > 評価される p.176 +7L < Where_true の "then" の分岐の効果と > Where_true が成立する時すなわち "then" の分岐の効果と p.177 -12L < 元の引数に適用された関数がである！ > 前の引数がそのまま適用された関数がである！ p.177 -9L < いったい我々は何かを定義したのだろうか > 果たして我々は何かを定義できたのであろうか 訳の癖 4 参照 p.185 3番めの黒丸 < その文脈から実際に宣言されたものとして扱われる整数変数で、 > その文脈上で整数変数として実際に宣言されたものとして扱われ、 p.185 4番めの黒丸 言語仕様の variation を語っている部分であることを明確に訳して欲しい。 訳を読み返しても原書の意図(どういう variation があるのか)が伝わって こない。 < j が普通の変数として実際に扱われるならば > j が前項のようなループにローカルな特別な変数じゃなくてループから抜けた > 後でも通常の変数とおんなじく参照できるなら < インクリメントの連続によって獲得された最後の値に等しいかの > 脱出までインクリメントを繰り返した結果に最後に得られる値に等しいかの < ループの本体が少なくとも１回実行されたのであれば、多くの場合、... これは、 ループの本体が少なくとも１回は実行される言語仕様ならば、普通、... ということか？あるいは ループの本体が１回以上実行された後でループを抜けてきた時には、 多くの言語仕様では、... だろうか。原書にあたりたいところ。 また、閉じていない括弧がある。 p.185 5番目の黒丸 追加されたテストはどんなテストだったのだろう？ p.186 17L < コンパイラがデータ構造を生成し、それを使うインタプリタが何の結果も < 生成しない(Graal に入力も出力もない)場合でも、 意味が良くわからない。杉山氏によれば、 > コンパイラが生成した中間コードデータを使って動くインタプリタは、 > 結局何の結果も生成しない(Graal には入出力の機能が備わっていない) > のではあるが、たとえそうであっても、 という意味とのことである。 p.186 -16L < 追跡機能 > トレース機能 今は「追跡」と言う人はいないと思う。 p.186 -6L < リスティング > リスト p.190 +1L どうも日本語が怪しい。 < オブジェクト指向言語をサポートする機能 > オブジェクト指向言語がサポートする機能 もしくは、括弧内を > (情報隠蔽の機能をオブジェクト指向言語が典型例である) とかしてはどうか。 p.191 < 名前同一性 > 名前等価性 構造による「等価性」に対して、名前による「同一性」と、呼び方をわざわざ 変えるのは意地悪。 p.195 -8L < １つ以上の関数の値そのものが有限関数となる。 > 関数の値そのものが、また(有限)関数となり得る。 意味不明で無意味な「１つ以上」。 p.197 [7.3] X.t = Undefinedvar のような代入をした後で X.t を参照したときなど、 given 句で計算された record_val が unknown の値を保持していることが ありえるが、それを考慮していない。given 句の then 部分は、record_val が unknown かどうかで場合分けしなければならない。 p.198 +1L < typemap(v) is Type_map and ... > typemap(v) is Type_name and ... なぜなら、typemap の型は Variable --f--> Type_value であり、Type_value := Simple_type_value | Type_name であるから。 p.198 +11L < まだ値の割り当てられていないレコード変数の値として空の関数Φを充てた もちろん正確には、 何らかの値が割り当てられてることは全く示さないような 中立的なレコード変数の値として、空の関数を採用した というところだろう。どうやら、このあたりのページでは、値の割り当て られていないレコード変数の値が unknown ではなく、空の関数であると勘違い して議論が進められている恐れがある。(例えば、上でも触れた p.197 [7.3]) これが p.199 にはいると、「unknown が生成される」等の正しい記述になる。 p.198 +12L < ([7.2] の initial_value の最初のケース) > ([7.2] の initial_map の最初のケース) p.200 2番目の黒丸 < td を含む > td を含まない td を含んでよいなら、 type A := record a:A end (Needed に A を含む) が許されてしまう。再帰を許さないようにしようというのがこの節の議論。 p.201 7.3章+8L < 配列には束縛がある。 > 配列には添字の範囲に制限がある。 以降、配列に関する話の所で「束縛」というのは、範囲とか、添字の範囲とか 添字の制限とかいう表現ではどうか。 p.202 +6L < この場合、下の Figure 7-1 に示すように、ポインタはポインタ型でない < 型の何らかのフィールドを持つオブジェクトを指す。 実は、解釈が２通りある曖昧な文。しかし、図を見れば意味はわかるので大丈夫。 それよりも、「この場合」といって、T と ^T の対照についての言及になって いるのだが、原書でどういう表現になっていたのか....「ポインタは」とは、 「ポインタという概念は一般に」ではなくて、「この ^T というポインタは」 と読まざるを得ないが？ p.203 +6L < あらゆる種類の これは "all kinds of" の訳？それなら、all には「全部」以外の意味もある。 > いろいろな種類の p.203 +11L < 正式には q を指定していないにもかかわらず 「正式」に違和感はないか？ > 表向きには q を指定しているようには見えないのにもかかわらず p.204 -15L < 入出力をわざわざ正当化する必要はない。 > 入出力の必要性は、ここで改めて説明するには及ばないだろう。 p.204 -4L < コンパイラの作成者には、少なくとも何らかの入出力命令を備えた言語を < 探すという仕事が残されている。 意味がわかりません。 杉山氏によれば、 > （Algol60の場合、元の言語仕様に入出力機構が含まれていないので）その > コンパイラ作成者は、皆 、独自の入出力機構を設計しなければならない。 ということだそうである。 p.205 5番目の黒丸 < 書き出されたすべての位置を消去する Rewrite 命令 > 書き出されたすべての内容を消去する Rewrite 命令 p.207 MRead の定義 < 前のファイルの終りを読もうとする。 杉山氏によれば、 > ファイルの終りを過ぎて読もうとする。 p.213 7.6.6章 variable_value の定義の直後 < この不変表明は > 以前示した不変表明は p.213 -9L < 関数 variable_value(x) は宣言済みの変数に対してだけ適用でき、部分関数 < である。 ２つのレベルの話が混ざっている。(宣言済みの)変数に対して適用できるのは、 型からいっても、 λx. variable_value(x) : Variable -/-> (State -/-> Value) の方。一方部分関数なのは、(dom variable_value でなく) dom variable_value(x) を次の行で示しているのだから、 λσ. λx. variable_value(x)(σ) : State -/-> Value の方。もちろん lambda x. variable_value(x) も部分関数だとは思うが。 < 宣言済みの変数に対してだけ適用でき > 変数 x を宣言している環境での状態に対してだけ適用でき なら話はわかるのだが。 p.217 -6L < 代わりに副作用が生成されることが前提となっていた。 > 代わりに副作用のある命令を用いることが前提となっていた。 p.217 -3L < したがって 意味がよくわからない。直前までは、副作用のある関数呼び出しの必要性を 論じていながら、「したがって」、[7.9] のように(副作用の可能性のある)関数 呼び出しを式と区別しておくべきだといっている。 p.218 7.7.4章 2番目の黒丸 < 本体における曖昧さの原因となるため、仮引数の名前は仮結果と同じ名前で < あってはならない。 どういう曖昧さのことなのか、わからなかった。 杉山氏によれば、 仮引数の名前が仮結果と同じ名前であれば、サブルーチンの本体でその 名前が引用されたとき、実行時に それが 実引数の変数なのか結果の変数 なのかが曖昧になる。 ということだそうである。 p.218 7.7.5章 +2L < 引数については、ルーチンから実「入出力」引数の元の値が得られるが、 「ルーチンから」というのが意味不明。 > 引数については、実「入出力」引数の（元の＝呼出し側での）値を > 呼び出されたルーチン側で参照できるんだけど、 というような意味らしい。 杉山氏によれば、原書では available to the routine とあるそうである。 p.218 -4L < 引数渡しの様式が "値による結果 (value-result)" ここは、引数渡しの形式に関する議論なら、call by value-result のこと だろう。これを、値「による」結果という訳しては、雰囲気が正しく 伝わらない。（辞書の類には「コピー復元呼び」「入出力呼びだし」などと ある。） p.221 +14L < 結果となる仮引数 > 結果となる仮結果 あと、ここの文は、もう少し読みやすくできないか。「ルーチンから返る時の」 なんて省略してもいいのじゃないだろうか。 p.221 7.7.8章 +2L < ルーチンの宣言はすべてのブロックに記述でき、 > ルーチンの宣言はどのブロックに記述してもよく、 p.221 7.7.8章 +4L < 内側で宣言されているルーチンの名前と重複する名前がある場合、 > 外側で... p.222 -6L < Routine_env := Variable -f-> (State -/-> State) > Routine_env := Identifier -f-> (State -/-> State) routine_denotation の型との整合や、p.217 の [7.9] を考えるとこうなる。 p.222 -5L < ルーチンのルーチンの > ルーチンの p.223 MBlock の定義 意味関数 M の添字が抜けている。allocate の位置が変。 > MBlock[b:Block] := λσ. > (record_routines(b.routines); > allocate(b.variables); > MInstruction[b.body]; > deallocate(σ))(σ) p.223 -10L < ルーチンが宣言されているブロックの実行の度に形式的に "再計算 < (recompute)される各ルーチンの表示を持つことはあまり都合が良くない。 「実行の度に、表示を持つ」「実行の度に、再計算される」どっちなのか。 後者だと思うが、その場合は今度は、「再計算されるルーチンの表示を持つ」 という日本語がどうも変だと思う。 > ブロックが実行される度に、そこに含まれるルーチンの表示を再計算して > しまうのは都合が良くない。 という程度でぐらいでいいのでは。 p.223 -7L < 可変の名前 > 変数の名前 p.223 -7L < その関数が typing であり、Type_map を生成する。 > その関数が、Type_map を生成する typing である。 typing が Type_map を生成する点は、ルーチンの表示をどこで計算するか という問題には副次的である。「どこで」に対して「typing である」と 答えることが重要。 p.224 7.7.10 +1L < ルーチンそのものも再帰的であり、したがって、routine_denotation は < ルーチンの本体に適用される MInstruction を使用する。 routine_denotation を見ればわかるが、MInstruction を直接使用していない。 MInstruction を使用しているのは、record_routines である。もちろん、 ここの文でいっているのは f(param) is do ... call f; ... end のようなものがあった時に、 call f の表示は f の表示によって決まる のだが、f の表示の方は、f のブロック全体(そしてそこには call f が 含まれている)がわからないと決まらないということである。よって 次のような書換えが考えられる。 > ルーチンそのものも再帰的であり、したがって、routine_denotation は > MInstruction をルーチン本体に適用した結果によって定まる。 しかしこれでもまだ「再帰的であり、したがって」というのが変だ。ここの ２つの文の論理展開は、 前提A：routine_denotation は MInstruction に依存している。 前提B：ルーチンは再帰的である。 結論：本体に再帰呼び出しが含まれることがあり、その場合逆に MInstruction が routine_denotation に依存している。 ということのはずだから、これを反映した訳にして改訂して欲しい。 p.224 7.7.10章 +12L < 4*i をすべての負でない数と関連付けたり > すべての負でない数 i に対して 4*i を関連付けたり 訳の癖 3 参照。この文の後半も同様。 p.225 -15L < 定義域 Ta を持つタグから値への有限関数として > 定義域が Ta であるようなタグから値への有限関数として p.225 -6L < このような規則があれば、２つの関数の和によって１つの関数を生成する < こともできる。 意味が良くわからない。文字どおり、関数の和をとったものと解釈していいのか？ Eiffel は renaming という「このような規則があ」る言語だが、果たして renaming によって「２つの関数の和によって１つの関数を生成すること」は できるのか？ 杉山氏によれば、 原書には union of two functions とあります。和というよりも 親で 定義されている同じ名前の関数を使って 子 でも 同じ名前の関数を 定義できるという意味では？ とのことである。 p.226 [7.18] の2行下 「(上の呼び出しでは x)」の、挿入されている位置がおかしい。x は主要な対象。 p.227 問題7.8 最初の黒丸 < 可能だろうか？ > ありうるだろうか？ のような気がするが、原書を見ないとわからない。 p.227 問題7.9 < アクセス可能な "メモリ" アドレスの線形集合から使用中の(アクティブな) < 変数群への束縛と各状態を関連付けた。 > 使用中の(アクティブな)変数群から、アクセス可能な "メモリ" > アドレスの線形集合への束縛と、各状態を関連付けた。 訳の癖 3 参照。この文に関しては、「から」という方向性が全く逆で、 癖というより明白な誤りになってしまっている。 p.227 -1L < 内側のブロック > 外側のブロック 同じような間違いが、p.221 7.7.8章 +4L にもあるのだが、もしや Meyer さんが 言う「内側」って、私が思う内側(字下げが深い方が内側)と逆なのだろうか？ p.230 8.1.2章 +2L < または、間接的な呼び出しを含む再帰的な　と、 杉山氏によれば、空白部に当てはまるのは「手続き」だそうである。 p.230 8.1.2章 +4L < 任意の使用可能なルーチンの制御フローには > ルーチンが現実に使い物になるためには、その制御フローには p.230 8.1.3章 +2L < 一体何かを定義したのかどうかはっきりしない。 > 果たして何かを定義できたのかどうかはっきりしない。 訳の癖 4 参照。 p.233 8.2.1章 +1L < この定義は一体何かを定義しているのだろうか > この定義は果たして何かを定義しているのだろうか 訳の癖 4 参照。 p.238 8.4.1章 < 実数解析 > 数値解析 実数解析と言う言葉は世の中で使われていないと思う。 p.238 -11L < 黄金比として知られる (1+root(5)/2) に集中する。 原書では「集中」は何と表現されていたのだろうか？ converge だったら収束かな。文脈を文字どおりに受けとると「集積点」の イメージに近いけど。 p.241 -8L < より高いレベルへの連続的に新しい構成要素を追加する。 > より高いレベルへと連続的に新しい構成要素を追加していく。 p.243 脚注 < より一般的な概念との混同を防ぐために、 > より一般的な概念と混同しないこと。 「安定という語は、混同を防ぐために、集合論的な意味で使用する」という 文の構造は変だと思う。だって、集合論的な意味で使用しない場合、 混同が生ずるどころか混同はあり得ないのだから。「安定という語をここでは 集合論上の性質として使用するから混同するな」だろう。 p.244 Figure 8-2, 8-3 domain を示す「N黒丸」は、ここではただの「N」であるべき。脚注や、 図を見ると、わざわざ 0 から始まると明記してある。 p.244 -2L < (τ(s) という表記は、一見そう見えるように、数学的に正しくないだろう)。 > (τ(s) という表記は、一見正しそうに見えるが、数学的には正しくない > だろう)。 p.246 狭義性の定義 < 次の式が成立する場合にのみこの関数は狭義 (strict) である。 数学の習慣では、「A の時のみ B」というのは、「B ⇒ A」と等しいが、 まさかそういう定義ではあるまい。「A ⇔ B」をいうには、「A の時、また その時に限って」とかいう表現をすることがある。 > 次の式が成立する場合、またその時に限って、この関数は狭義 (strict) > である。 あるいは、 関数が狭義(strict)であるとは、...a,b について... 次の式が成立することである。 というような表現もできよう。 p.246 [8.14] どうして、「xx な場合にのみ yy」という珍しい表記を持ち込んで、普通の 簡単な表現をとらないのか... > 全関数は、個々の引数について狭義ならば、引数すべてを同時に扱っても > 狭義である。 の方がずっとわかりやすいと思う。 p.249 [8.17] の証明 個別引数安定性とは、 個々の引数について安定 ⇒ 引数すべてをひとまとめに考えても安定 ということであると、まず確認しておく。 1行目 < さらに証明すべきは、狭義関数 ... がそれぞれの引数について安定であるか < どうか... これは証明で使う仮定であって、決して「証明すべき」ことではない。 6行目 < したがって、任意の x、y、a、bについて次のことも証明しなければならない。 > 上の仮定の元で、任意の x,y,a,b について次のことを証明する。 p.251 +3L < この場合、どのように "良い" 不動点が τ∞ だろうか 「どのように良い」とはどういう意味なのかよくわからない。文脈からは、 > この場合、τ∞は他の不動点と比べてどのような "良い" 性質があるの > だろうか。 という意味だと想像される。 p.251 8.5.4章 +1L < "もっとも負担の少ない(least committing)" なるほど。ちなみに私だったら > "約束している性質の範囲がもっとも狭い(least committing)" p.252 +2L < 偶数の定数についてのみ定義された値１を持つ定数部分関数 > 偶数の値についてのみ定義されていて、そこでは常に１を返す定数部分関数 p.252 +6L < 関数 δx はδの唯一の不動点である。前述(233ページ)のように、実際には、 < すべての形式の不動点が無限にある。 > 関数 δx だけがδの不動点なわけではない。前述(233ページ)のように、 > 実際にはいろいろな形式の不動点が無限にある。 p.254 +1L < (これは∩が狭義であることを表すもう１つの方法である。) もう１つのといわれても、ここ以前に∩が狭義であることを示してはいない > (これは∩が狭義であることを表す１つの方法である。) とか、 > (これは実は∩が狭義であることを示してもいる。) とかいうことだろうか。 杉山氏によれば、後者のように思われるとのことである。 p.254 8.6.2章 +1L < 代入先だけでなく、代入元も部分集合の集合である関数が必要なため、 < 最初は、前述の理論が適用されないように見える。 代入先とか代入元とは何だろうか。いわんとしているのは、 述語を関数とみなしてその安定性を与えて、前述の定理で見たような、 安定関数の組み合わせを考えたりする(p.255 の λx,y Ψ(x)=ξ(y) の 例みたいに)ことを述語でもやってみたいな。でも、述語に安定という 概念を与えるのは一見無理そうに思えるよね。だって、p.245 の先頭で、 この章では集合というのは実は部分集合の集合ということにする約束で、 [8.16] の安定関数の定義で要求している X --> Y という型も、 部分集合の集合--> 部分集合の集合ということなんだから。述語の 先集合は B だから、これと整合しなくて困ったなあ。 ということだと思う。 p.254 8.6.2章 +10L < 述語πの安定性とは、πがある順序列のすべてのエレメントについて真ならば < πはまたその順序列の union についても真であることを意味する。 順序列→鎖。 真→true。ここで注意すべきなのは、この文と次に続く文が、きれいな対比を なしている点だと思う。 > 述語πの安定性とは、πがある鎖のすべてのエレメントについて true ならば > πはまたその鎖の union についても true であることを意味する。 p.256 +14L < stable subset operation > 安定部分集合操作 p.256 -11L < 部分的な述語[8.21]は安定ではなく、 > 述語 partial[8.21]は安定ではなく、 意味は合ってるかもしれないが、[8.21]を参照していることを尊重しなければ。 Φ∞が全関数であることを、不動点帰納法を使って無理に証明しようとすると、 次のような形式になると主張しているのである。(ただし、直前の文でいって いるように、fi が全部部分関数なので、Φ∞が部分関数であることを証明する 羽目になるのだが) Φは安定な全関数である。 述語 partial[8.21] は安定である。(うそ) 次の２点がいえる。 a) partial(空関数) b) ∀h:partial(h) ⇒ partial(Φ(h)) よって、不動点帰納法によって、 partial(Φ∞) がいえる。おわり。 p.256 -1L < このパターンでは どのパターン？ > これと対比して、公理意味論の方での証明パターンとしては p.257 8.6.3章 +1L < 安定部分集合操作の定理は、引数、すなわち、関数が部分集合でもあるため、 < 汎関数の特殊なケース(関数の集合に対する全関数)への適用が可能である。 > 安定部分集合操作の定理は、特殊なケースとして、汎関数へ適用することも > 可能である。なぜなら、汎関数の引数すなわち関数は、部分集合とみなす > こともできるからである。 p.257 安定汎関数の定理の4 < 非演算数に適用された場合。 > 被演算数に適用された場合。 直前の説明にあわせて、「被演算数」ではなく「引数」としてもいいかも しれない。 p.258 +3L < 互いに疎でない定義域であれば、定義域が一致する関数からアクセス可能 < である。 何がアクセス可能なのか、意味不明。 杉山氏によれば、アクセスは acceptable の誤訳だそうで、 > 互いにNon-disjointな定義域であれば、それらの定義域に関する 関数の > overriding unionは認められる。 とのことである。 p.259 -12L < MInstruction は、loop_functional の不動点である。 > MLoop は、... p.260 [8.23] list の定義 < list := ∪i:N ... > list := ∪n:N ... p.260 -14L < リスト式 List* > リスト式 Instruction* p.261 -2L < (値域ではなく定義域について部分集合関係を考慮したならば、この状況は < 逆転する。) これは誤り。x ⊆ y ならば、任意の b について、(x --> b)⊆(y --> b) である。 a --> b のことをよく b^a(b の a乗)と書くでしょう？多分、 X ⇒ Y の時の (Y ⇒ B) ⇒ (X ⇒ B) という話と混同しているのだろう。 p.262 +5L < 反対に、Bのメンバはそのすべての値が同じjについてのxjに含まれる関数である。 １０回ぐらい読まないと意味がわからなかったので、次のようなのはどうだろうか。 > 反対に、Bのメンバは、値がすべて特定の１個の xj だけに含まれてしまうような > 関数である。 p.263 最初の式の直後 < これらの式の "Sum" を展開し、中間的な "Variables" をなくすと、 > これらの式の和の部分を展開し、中間的な変数を消去すると、 Sum とか Variables とかは構文要素のことではない。「Sum を展開し」とは、 W = v A = v * E から、I = W + A という式を I = v + v * E へと展開することをいっている。「中間的な Variable をなくす」とは、 こうした展開によって、W,Aといった変数が消去されることをいっている。 p.265 1番目の式の直後 < プログラムはまだない。命令は Write に限定されている。 < 式は変数と定数に限定されている。 どうして Write だけが抽象構文の記号で表現されているのだろう？ p.263 +3L でも Variable とか Constant とか表現しているのに。 > Program はまだない。Instruction は Write に限定されている。 > Expression は Variable と Constant に限定されている。 どうようの問題が2番目の式の直後の段落にもある。構文要素の記号による表現が わかりにくいので、Program → プログラムなど自然な意味に置き換えて説明して いるのかもしれないけれども。 p.265 2番目の式のうしろの2行目 < 変数が定数 > 変数か定数 p.265 -3L < 恒等 この文脈が p.257 の安定汎関数の定理のことを直接いっているのなら、「合成」では？ p.266 8.7.1章 +11L < n = 1 > n = 0 < １つの値を貢献するべきである。 > １つの値を貢献するはずである。 p.269 [8.31] 文末のカンマは不要。 p.269 -5L < N × Φ > N ∩ Φ p.269 3番目の黒丸 < これは与えられるものである。 「これ」とは後のものを参照しているので、読んでいて唐突な感じがしないだろうか。 「与えられる」もよくわからないが、空関数の定義として与えられるということだろう。 p.271 -7L < 値として true を生成する。 > 値として true または false を生成する。 もしくは > 値として真偽値を生成する。 p.271 -6L < つまり、p が true を生成する状況で、X/p が X の部分集合である場合、 < X/p に含まれるのは p が適用可能な値だけである。 意味がよくわからない。X/p に含まれるのは、pが適用可能でかつ true を 生成するような要素だと思う。p が適用できて初めて true が生成できるのに、 まずまっさきに true を生成するという話が出てくるのが腑に落ちない。 また、X/p が X の部分集合であるというのは常にそうであり、わざわざ そういう「場合」と断わっているのは何故か？ 杉山氏によれば、 原書での if を「場合」と訳している。「X/p に含まれるのは、 pが適用可能でかつ true を生成するような要素。」 とのことである。 p.273 -5L < ルーチンにあるルーチンが > ルーチンに、あるルーチンが p.275 +1L < ルーチン、または、属性の適用の代入先として使用する場合。 何を使用する場合に何が狭義になるといいたいのか。 > ルーチン呼び出しや属性の参照において、その結果を何らかの変数へ > 代入する場合。 つまり、参照透過性をこわす場合といいたいんだと思う。 p.277 +1L < 束縛が 1 から n である配列、 > 添字の範囲が ... p.277 -14L < このような言語のうちで演算子群を１つだけもち、被狭義意味論ももつのは、 < Algol W と Lisp と C である。 > このような言語のうちで、and や or の演算子として、非狭義な意味を > 持つもの１種類だけを備えているのは、... p.279 順序関係の定義のうち、反対称性の所 < x ≦ y かつ y ≦ z ならば、x = y である。 > y ≦ x ... p.280 +6L < 全的順序 > 全順序 全順序という用語は定着している。また、酒匂さんの話では 二木先生からも「.. 的 ..」という言い方を、こ れから formal コミュニティの中でも極力排していきたい、という 意向を受けました。 ということだったと思う。 p.281 -14L 他、p.282, p.288 など < iff iff = if and only if = 同値だということは、英語で高等教育を受けた 人には常識なのだろうが、 学部あるいは大学院の入門レベルの理論計算機科学の教科書として 用いられることを想定している。(p.7 はじめに) ならば、日本で読まれる訳本には説明があってもよいのではないか。 p.282 [8.37] 「直積順序と呼ばれる関係≦の元にある」のところの、「≦」の添字は 「X×Y」が正しい。 p.284 8.8.8章 < 上限 > 上界 upper bound → 上界 least upper bound → 上限 or 最小上界 というのは、ゆるがない数学用語。upper bound を上限と訳したのでは 混乱が生じる。 p.285 +8L < これが可能なのは、関数の集合Aという非常に特殊な場合だけである。 > これが可能なのは、関数の集合Aに上限が存在するという非常に特殊な場合 > だけである。 (できれば上限は上界に直しておきたい) p.285 [8.43]のところの例の4行目 < XにおけるR-{1}と、Aにおける1よりも小さいすべての数の集合を < 挙げることができる > XをR-{1}とし、Aを1よりも小さいすべての数の集合とした場合が挙げられる。 p.287 3番目の黒丸 < Xが有限な場合、すなわち、Xの順序が平坦順序...である場合 > Xが有限な場合、もしくは、... 有限だからといって平坦順序になるはずがない。 p.287 -5L < 限界(limit) > 極限(limit) 定着している数学用語。 p.288 8.8.12章 < 帰納的閉集合 帰納的閉集合とは一般的な数学用語ではないと思うが、いかにも何か特定の 種類の閉集合のこと(帰納的順序集合というものは存在する)をいっている ように感じさせてよくない。 「他の順序関係から副次的に派生して定義される閉集合」ということだろう。 帰納順序集合(任意の全部分集合が上に有界であるような集合)とは無関係 だよね。 p.288 [8.48] < 帰納的順序において閉じている > 直積順序において閉じている 帰納的順序などという(数学の)用語はないと思うし、少なくともこの本では 説明されていない。「X×Yに先だって存在するX,Yの上で定義されている順序 関係を元に、新しい順序関係を構築しましたよ」という気持ちが「帰納」という 言葉なのだと思う。これをそのまま「帰納」と書かれても読む人にはわからない。 p.288 [8.48] の証明 誤植が複数(x,y を定義せずに使うなど)含まれている。言葉遣いもおかしい。 以下のような証明ではどうか。 X×Y における任意の鎖 p は以下のようにおける。 p := <>i=1,∞ 直積順序の定義から、 x := i=1,∞ y := i=1,∞ は、それぞれ X, Y における鎖になっている。ここで、 を考えると、明らかにこれは p の最小上限になっている。ところが、 X, Y は閉集合だから、lub x, lub y は各々 X, Y の要素である。よって p の最小上限 は X×Y の要素である。おわり。 最小上限は、本当は「上限」or「最小上界」と書きたいところ。 p.289 +2L < 最初の場合の b < b' への制約は いっていることはわかるが、「場合」という表現は変。 > iff の右側に最初にあらわれている、b < b' という制約は p.290 +13L < 最初に、xab は両方の鎖 xa ≦ xab と xb ≦ xab の上限である。 > 最初に、xa ≦ xab と xb ≦ xab であることから、xab は > 両方の鎖の上限である。 p.290 +14L < xi ∈ A であるような任意の i について、... < ... 整数 j と k が存在する。したがって、xa は B の鎖の上限であり、 ここは変。i,j,k 3つも持ち出して余計なことをいっている。 > 任意の xj∈B について、xk∈A となるようなk(>j)が存在し、 > xj ≦ xk ≦ xa である。したがって、xa は B の鎖の上限でもあり、 p.290 +16L < ちなみに、xa は元の鎖の上限であることがわかっており 「わかっており」では、とぼけているような奇妙な印象を受ける。 わかっているで済まさずに「示す」のが証明であろう。元々の意図としては 「xa が元の鎖の上限であることは自明であり」といったところだろうか。 面倒くさがらずに説明するとしても一言ですむ。 > ちなみに、xa は A の鎖、B の鎖両方の上限であったから、 > 元の鎖 x の上限でもあり、 p.290 +18L < A∪B の任意の鎖は A、または、B のいずれかに属する有限個数のエレメントを < 持つ 「持つ」ことじゃなくて、有限個「しかもたない」ことをいいたい。 > A∪B の任意の鎖は、A のエレメントを高々有限個しか持っていないか、 > または B のエレメントを高々有限個しか持っていないかのどちらかである。 p.290 [8.52] 定義 関数との混同を避けるため、⇒ の代りに ⊃ を使う約束だったはず。(2.2章) 厳格には、あれは Metanot の世界の約束であったが、現実にいままでは Metanot の外の世界でも ⊃ の記号を使ってきた(例: p255 [8.22])のである。 p.291 連続関数の定義の直後 < 最小上限と一致する > 最小上限を保存する p.292 -1L 証明終りの印を文字と重ならないようにしたい。 p.293 -5L < 完全半順序(最小順序を持つ閉順序) > 最小要素 p.295 問題8.4 < 構造帰納法と構造帰納法 > 構造帰納法 p.296 問題8.9 < τが最小メンバ(cpo)を持つ閉集合 X に関する > τが最小メンバを持つ閉集合(cpo) X に関する p.301 9.2.6章 +1L < 推論規則は、新しい定理を他の定理から派生するための機構である。 派生の代りに導出という言葉を使いたいところだが、「導出規則」と 衝突するから派生でもやむをえないだろう。しかし、一旦派生と決めた ならば、一貫して派生という言葉を使ったほうがいいと思う。p.318, p.354 などに、派生の意味で導出という用語が使われているように思う。 p.301 -9L < 肯定式(modus ponens) 「肯定式」という用語は使われているだろうか。「分離規則」というのは よく聞くが。 p.305 +1L < セオリーがモデルを持っている場合、１つ以上のモデルを持っている > 複数のモデルを持っている ここでの意図は「２つ以上」のはず。 p.305 -8L < 完全さ > 完全性 健全「性」の一方でなぜに完全「さ」？それに「ゲーデルの不完全さ定理」 では格好がつかない。 p.305 -3L < したがって、... 完全であることがわかる。 > また、...完全である。 健全性の話と完全性の話は独立。 p.306 +1L < この場合はそうではない。 これでは意図が伝わらないと思う。知識のない人が普通に読めば、 「この場合」というのが何か特別な条件下のことをいっているように とれてしまう。 直前の文で健全性の方の話を考えていた時には、まっとうな セオリーはすべて健全なものであるとしたわけだ。じゃあ、 完全性の方も、おんなじようにまっとうなセオリーは完全であると 期待してよいかというと、残念ながら完全性の場合(=この場合) にはそういったことは一般にいえないんだねえ。 という展開(健全性と完全性の対照)がわかるような訳にしてほしい。例えば > 健全性に対してこちらは必ずしも期待できない。 p.306 9.3章 +1L < 始めて > 初めて p.306 -9L < 矢印は右側と結び付く。 「右側と結び付く」というのは、一般に通じて、曖昧さを生じない言葉 だろうか。 > 矢印には右結合性があるものとする。 の方が（通じないことがあったとしても）曖昧さを生じなくていい気がするが。 p.309 E.2 < x:N→N + y:N→N + z:N→N + x:N | z: N > x:N→N + y:N→N + z:N→N | z: N IApplication 規則は、束縛が正確に一致することを要求するから、現状では E7 が導出できない。 p.313 -1L < t は束縛が 1 と n の配列 > t は添字の範囲が 1 から n までの配列 p.314 +4L < 条件を単に表現できない > 条件を全く表現できない p.315 9.5.3 +7L < この値は P が満たされていて、かつ Q が満たされていれば、 < その時に限り真である。 これでは論理積に読めてしまわないか？ > この値は、P が満たされている時には同時に Q も満たされていれば、 > またその時に限り真である。 p.316 9.6.2章 +3L < というものだった。 > というものである。 p.317 -1L < {x > 1} x := x + x {y > 1} > {x > 1} y := x + x {y > 1} p.318 9.6.4章 +1L < ある範囲で導出規則と似た言語から独立したある推論規則はいくつかの < 証明において役に立つ。 翻訳プログラムの出力のようで美しくない。 > 次に示す推論規則も、導出規則と同様に言語から独立したものだが、 > 証明上役立つ場面が多いものである。 p.318 9.6.4章 +2L < ２つの事後条件を導出できる場合、 導出→派生という用語を使わなくてよいのか？ p.321 [9.11]の直後の行 < すると、置換の合成の規則...によってQ[x←e]はPであり、これは、この場合 < x が P の中に出現しないという前提のおかげで適用可能である。 > すると、x が P の中に出現しないという前提のおかげで置換の合成の規則... > が適用可能となり、Q[x←e]はPと等しいことになる。 p.322 -3L < プログラムの確率(provability) > プログラムの証明可能性(provability) p.323 9.7.3章 +8L < 代入によって i=j かどうかの事後条件を保証できないため > 代入時に i=j かどうかによって事後条件を保証できるか否かが左右され p.325 +4L < c の not を行わなければならない。 > not c との "and" を行わなければならない。 p.325 [9.15] 式のうしろ4行目 < 隣のページ > 次のページ 多分原書では隣だったのでしょう。 p.325 [9.15] 式のうしろ5行目 < P と Q は事前条件と事後条件なので、２つの属性を > P と Q を [9.15] の事前条件と事後条件とすると、次の２つの属性を p.327 S4 < (m,n... > {m,n... p.330 9.7.7章 < 終了 どうして「停止性」という普通の用語を使わないのか。実のところ、 この 9.7.7 を point している、p.122 の脚注 *4 では「停止性」に している。 p.330 Figure9-5 L3 あたりから間違っている。CONS で事前条件をいじる場合、より強い条件に 置き換えねばならないのに、m,n>0 を落としてしまって、より弱くしている。 理由の表記もところどころ変。以下のような証明ではどうか。 INVMN := INV and m,n>0 とする。 ========================================================================== L1 {m,n>0} x :=m; y:=n; {x,y>0 and gcd(x,y)=gcd(m,n) and m,n>0} S5 そのもの L2 {m,n>0} x:=m; y:=n {INVMN} L1, INVMNの定義 L3 {INVMN and x≠y} CONDIT {INVMN} C7(326ページ);CONS L4 {INVMN} LOOP {INVMN and x=y} L3;ILOOP L5 {m,n>0} x:=m; y:=n; LOOP {INVMN and x=y} L2,L4;ICompound L6 x,y>0 and x=y implies gcd(x,y)=x EM L7a INVMN and x=y implies gcd(m,n)=x L6,EM L7b {x=gcd(m,n)} g:=x {g=gcd(m,n)} AAssignment L8 {INVMN and x=y} g:=x {g=gcd(m,n)} L7a,L7b;CONS L9 {m,n>0} EUCLID {g=gcd(m,n)} L5,L8;Icompound ========================================================================== p.331 定義 < 負でない限り V の値を少なくとも１減らす > 負にならない範囲で V の値を少なくとも１減らす p.337 黒丸のところ < 条件 c と Q を満たした状態で a が終了するための必要十分条件 < 条件 not c と Q を満たした状態で B が終了するための必要十分条件 「と」に関する曖昧さを排除してほしい。 > 条件 c かつ、Q を満たした状態で a が終了するための必要十分条件 > 条件 not c かつ、Q を満たした状態で B が終了するための必要十分条件 ただし、こう直す場合、直前の行の「次の組み合わせ」という表現も 調整が必要になる。 p.338 2番目の黒丸 < この繰り返しから 「この繰り返し」というのは明らかに直前の項目をいっているが、１回だけ なんだから『繰り返し』という表現はおかしい。表現だけの問題で、意味は 明らかで大丈夫とは思うが。 p.347 -3L < 引数のないルーチンの規則が得られる。 > 引数付きのルーチンに関する規則が得られる。 p.347 -2L < 下に示すように、いくつかの制限が適用される。 > ただし、後の節で示すような制限が存在している。 p.349 I1Routine 適用時の制約のリスト 実出力引数 o は P に現れてはならない(p.347 -17L 「o が P に出現しなけれ ば...」)が、これはどこに含まれているのか？この制約を含めておかないと、 assign(out:A, in:B) is do A := B end というルーチンがあった時に、 {A=0,Y=2} X := Y {A=0,X=2} AAssign {A=0,B=2} call assign(A,B) {A=0,A=2} I1Routine という証明が成り立ってしまってまずい。p.350 -3L には 制約の６は前向きの代入規則を適用するために必要である とあるので、著者の意図としては６番目に記述したいらしいが、 < result リストの要素は P の中に出現してはならない。 という表現には、このことは含まれていない。もしや、 > output リストの要素は P の中に出現してはならない。 の間違いとも思えるが、その場合逆に p.350 -4L で言っている、 変数リスト argument と result に適用され という部分が意味不明になる。 p.350 +11L < P[i <- argument] > P[argument <- i] p.350 +17L < (7.2節、特に、7.2.3 節を参照) 7.2 節はレコード拡張の節だった。ブロック構造の節の方がふさわしいはず。 > (7.6節、特に、7.6.3 節を参照) p.353 -14L < この規則の前提はF⊃Gという形式と、形式Hのその結論である > この規則は、F⊃Gという形式の前提から結論Hを導くという形をしている p.354 +1L < 始めて言及した文献 > 初めて... p.354 囲み記事 +6L < 始めて > 初めて p.354 -3L < 証明と導出は 派生という用語をつかわなくてよいのか？ p.357 Hanoi のコード 普通、公理的意味論の元でルーチンを考える時には、 Hanoi(n:Integer; xi,yi,zi:PEG; xo,yo,zo:PEG) のように入力引数と出力引数を分けるものだと思う。 現在のコードが正しく動くためには、move の２つの引数は両方とも入出力引数で なければならない。Hanoi についても、x,y,z の引数は入出力引数でなければ ならない。(あるいは、PEG がディスクへの「ポインタ」であって、move や Hanoi は副作用を持つような関数であると考えてもよいが。)ところが、入出力 引数がある場合には、I2Routine 規則はうまく働かないはず(注*)。入力引数と 出力引数は分離されているものという仮定で、ここまで定式化が進んできた のである。よって、このコードに関しての証明はうまくできないことになる。 実際、p.360 [9.43] の証明は間違っていると思う。 (*) I2Routine 規則を適用するには、実結果 o は事前条件に現れてはいけないので あった(p.347 -17L 「o が P に出現しなければ...」や、p.349 の第6条件)。 ところが、ルーチンの呼び出しで入出力実引数として W を使った場合、 その事前条件は W を(入力の引数として)使わずに表現することはできないだろう。 p.358 +2L < この例題では自明な再帰的でないルーチンは許されていない。 > この例題を再帰的でないルーチンで記述することは難しい。 p.360 [9.43] 証明全体がナンセンスなものになっている。まず、1行目に typo と思えるような 誤りがある。 < Q[s←s-i, t←t＋s^i] > Q[x←s-i, y←t＋s^i] ここが誤りであることを理解するには、3行目で主張している「適切な引数の 置換」というのを、p.320 の [9.10]と I2Routine に照らして厳格に試して みるとよい。 (Q[x <- x - n, y <- y + x^n])[n <- i, x <- s, y <- t, z <- u] は、(x,y,z が Q に出現しないという妥当な仮定の元で) Q[x <- s - i, y <- t + s^i] なのである。(それ以前に、「任意の Q」を持ち出してくるのもどうかと思う。 {|s|≧i and a=s, b=t} Hanoi(i,s,t,u) {s = a - i, t = b + a^i} を証明するので十分ではないか。) 実はこれは単なる typo ではなく、p.357 での Hanoi の定義までに遡る誤り のようだ。Hanoi を定義した時点では、move など(Hanoi 自身も)が副作用の ある手続きとして(あるいは、規則が想定していない入出力引数を使っている ものとして)認識されていた。PEG が、ディスクへのポインタであるつもり だったのだろう。ところが、これが汎用スタックに置き換えられた時点で 崩れてしまったのである。 Hanoi は、引数が単なる入力引数である仮定すれば、常に何もしない つまらないルーチンとなり、逆に入出力引数であれば、この章の定式化の 範囲外のルーチンということになる。もちろん、正しく動くと主張している [9.43] の証明は完全に間違っている。正しい証明は、まず Hanoi を Hanoi(in n:INTEGER;in xi,yi,zi:PEG;out xo,yo,zo:PEG) のように書き直し、(そして、任意の表明 Q などは持ち出してこずに） {|a| ≧ i} Hanoi(i,a,b,c,s,t,u) {s = a - i, t = b + a^i} を示す形になるはずである。 p.363 +5L < 始めから > 初めから p.363 3番目の黒丸の 3 行目 < 仮説的な証明への道を開くプログラム開発によって、 意味がわからない。 p.364 3番目の黒丸の 2 行目 < コンパイラが備えている > コンパイラに装備することができる p.364 -2L < 今述べた構文要素の外側の > 今述べた構文要素以外でも p.365 +5L < 今のところ論理式を使っている たぶん以下のような意味だろう。 > 今のところ命題論理の論理式に限っている p.368 1番めの黒丸 < I は始めから保証が簡単である(Result の false や i の 0) > I は初めから保証が簡単である(i = 0 の時に Result が faluse であること) p.370 9.11.4章の直前の行 < "For"ループはこの戦略を備えている > "For"ループにはこの戦略が適している。 p.371 +3L < 変更は |j-i| であるため、最初の行は将来のループ不変表明 I として使用する。 > |j-i| の部分を変更とし、... p.371 +4L < I の初期の妥当性を保証する方がずっと簡単である。 > 始まりの段階での I の妥当性を保証することがずっと簡単になった。 p.372 [9.50] の下 5 行めの式 < i>0 and then t[Result]=x > Result>0 and tnen t[Result]=x p.373 -12L < 空集合についての属性が∀なので > 空集合についての∀という属性をいっているので p.377 2番めの項目 < だからといってすぐ j に移行するわけではない。 > だからといって、j についても同じことがいえるわけではない。 < i i ループが多くとも |log2 n| + 1 回実行される p.379 +2L < |x| は x より大きくない最大の整数である。 そのような演算子としては、[x] という表記を用いたい気もする。 p.379 +3L < この場合、i < j (i と j は整数) である時は必ず、j - i は実際に少なくとも < ループの両方のケースで２で割られる。 この場合、では直前の文の話に思えてしまう。また、「実際に少なくとも」とは？ > 今の場合、i < j (i と j は整数) である限りにおいて、j - i を２で割った > ものが、ループの分岐の各々でどのように変化するのか(j-i ≦ old(j-i)/2 か > どうか)調べてみれば良い。 といった意味だろうか。 p.379 +6L < i - ((i + j) div 2) ≦ (j - i) div 2 > ((i + j) div 2) - i ≦ (j - i) div 2 p.379 < 建設的アプローチ > 構成的なアプローチ p.387 問題 9.19 < 静的意味制約としての規則 I1Routine (9.10.4節) について < ルーチンに対する制限を表せ。 > 規則 I1Routine (9.10.4節) を適用する際のルーチンに対する制限を > 静的意味制約として表せ。 p.394 10.2.3 +2L < P と Q の属性が表明である。 意味がわからない。「(P と Q の)表明に関する性質(属性)をあらわしている」 ということ？ < そして、この表明は 「この表明」とは文脈上 "P implies Q" のことに思える。しかし直前で 「P implies Q そのものは表明ではなく」とあるのと矛盾してしまう。 p.394 -6L < (これは同語反復である) > (こういった論理式は同語反復と呼ばれる) また、「同語反復」は tautology の訳語と思われるが、そうであれば この分野では「恒真論理式」「トートロジー」などの方が一般的だと思う。 p.398 -2L < MAssertion[pp.pre] > PAssertion[pp.pre] p.399 10.3.2章 -1L < λσ:State . σ∈dom transform and then σ(x) + σ(y) ≠ (σ(x))^2 > λσ:State . σ∈dom transform and then > given > σ' = transform(σ) > then > σ'(x) + σ'(y) ≠ (σ'(x))^2 > end p.400 +2L < それはつまり pre-post 式が何についての pre-post 式かということであり 何を言おうとしているのかわからない。 杉山氏によれば、 > pre-post 式は プログラム（或は その一部）が正しいかどうかについて > の式である。 とのことである。 p.400 +13L < 次の恒等関数による準狭義な "or" によって ⊃ を 8.7.9 節で説明した < 準狭義解釈の implies_if_defined として考えると、問題は解消する。 「次の恒等関数による」というのが意味不明。これがなければ意味がわかるが。 何の次？あるいは、どこの次なのか？また、ここでいっている恒等関数とは、 本当に恒等関数(Id)のこと？ 杉山氏によれば、 implies_if_defined のことです。 identity（＝implies_if_defined） を 恒等関数 と誤訳しているようです。 > 次の準狭義な "or" によって ⊃ を 8.7.9 節で説明した準狭義解釈の > implies_if_defined として考えると、問題は解消する。 とのことである。 p.403 像演算の補助定理 +2L < g は互いに素な定義域を持つ > f,g は... p.404 定理の下 4 行め < to_from は D のすべての要素が f を C のいくつかの要素に適用した < 結果である場合にだけ真を生成する。 「だけ」の位置が変ではないか。「だけ」は「C だけ」という意味であろう。 C 以外の要素に f を適用した場合のことが、現状の文でははっきりしない。 > to_from は D のどの要素も f を C の要素に適用した場合だけでしか > 得られない場合に真を生成する。 p.405 +2L < 396 ページの MWeakest の定義から > 397 ページの ... p.409 10.5.4 2番目の黒丸 < λσ:State . (σ ∪\ {}) 正確には、 > λσ:State . (σ ∪\ {}) 直後の証明では正確に記述しているので、省略か何かだろうか。 p.409 -3L < これはこの表明に関連付けられている論理式が状態σである時、すなわち、 < MExpression[Q.exp[x <- e]](σ) が真である時に真であることを意味する。 > これは、この表明に関連付けられている論理式が状態σの時に真であること、 > すなわち、MExpression[Q.exp[x <- e]](σ) が真であることを意味する。 p.410 -7L < この場合次の式が成立するので、 > 一方、次の式が成立するので、 p.411 +12L < 式の意味から(6.5節) > 式の意味から(6.4節) p.413 +9L < これは２つの個別の属性の証明から構成されている。 > この証明は、２つの個別の属性の証明から構成される。 p.413 -10L < (関数φの像によって、任意の集合は空の部分集合を与えられる。) 日本語が変。 任意の集合 (ここでは IS) に対する関数φの像は空集合であり、 一方空集合は任意の集合 (ここでは IS-cS) の部分集合である。 という意味なのか、 任意の集合に対する関数φの像は、State の空の部分集合である。 という意味なのか、どっちか不明。 杉山氏によれば、後者のように思われるとのことである。 p.416 -6L < lhs と rhs の両方の項はすでに等しいことが証明されており、和集合として < 表現できる。 lhs と rhs が続く次の行のように和集合で表現できるというのは正しいが、 両方の項が等しいことは、まだこれから証明しようとしていること。 p.416 -1L < t0 > T0 p.418 10.6章 +2L < (7.6 節と 9.10.3 節参照) 再帰を含めたルーチンの文法は 7.7 だし、再帰呼び出しの公理意味論は 9.10.6 だったと思う。それとも他の何か特別な部分を参照しているのか？ > (7.7 節と 9.10.6 節参照) p.418 -4L < (9.7.4 節) > (9.8.4 節)