ゴール関係
implementation文書4章、ここに色々書いてあった。だけど、けっこう無茶苦茶。
- initial claim ＝ final goal だぁーー。backward reasoningだから。
- {final,main,primary,initial}{goal,claim,statement,thesis,proposition}はどう組み合わせても、ほぼ同義
- 証明状態の終状態はsolved formと呼ぶ。
- tactic は refinement operation だ。ということは、refinmentという行為で証明（つうかリーズニング）を行う。
- refineに似た言葉で、derive, solve, resolve, duduce, reduct, normalize, rewrite, simplify
- tacticalはmethod combinator
- methodの意味はまだハッキリしない。
- goalはmain goalとsubgoalsからなる、と、まーた、再帰的つうか帰納的つうかワケワカなこと言っている。伝統か。
- goalのconclusionはいいが、goalのgoalはワケワカだ、いくらなんでも酷い。
- goalのgoalをmain goalとかmain conclusionとか言っている。
- subgoalsの全体をgoalのcontextとも言う。
- main goalの意味がやっぱり曖昧。
- 提示された定理（の命題）に対してリーズニング（証明行為）の初期状態のゴール
- ゴールの結論（conclusion）
- ある証明状態におけるoutermostなPureの含意式
- goalはtheoremだ、とか言っている。そう言われても、今度はtheoremの意味がワカラン。
- goalのconclusionはpropositionだ、と言っている。んで、propositionてナンだよ？
- protected propositionて全然聞いたこともない言葉が、、、
- structured claim ？？
- Pure ruleとは、Mの実装であるPureが備える推論規則で、MLで書かれたもののこと、だと思う。
- あんれーーー？ 定理って、MLのデータ構造であるthmのこと。だとしたら、実装ベッタリの用語法やん、どこが宣言的で文書指向なんだよ!?
- 「goal stateはtheoremで表される」。goal steteってまた新語。たぶん、proof steteと同義で、stateがgoalだ、と言いたいのだろう。それがtheoremだってのは、データ構造がMLのthmだということだろう。
- successor state このsteteは証明状態＝ゴールのことか？ successorとは言ってもbackwardだから、後続じゃなくて事前の状態かもしれない。リーズニングの時間的進行方向と、証明図の空間的流れ方向が逆だから混乱する。どっちの事かも判断できない。
- implyとentailとdeduceとconcludeをどう使い分ける？たぶん、使い分けてない。
- resultまたはresult sequenceとは、tactic（の実装関数）の戻り値のこと。
- refine a subgoalとsolve a subgoalは違う？
- goalはツリー構造だと思えばいいか。
- outermostなgoalと、subgoalとしてのgoalは構造が違うらしい。知らなかったよ。
- outermostなgoalはホーン節、内側のゴールはHereditary Harrop Formulaだと。ほんと知らねーよ。
- goalの場合は、context=subgoalsの要素＝subgoalだけど、これをgoal hypothesisと呼ぶ。なんでだよー、なんでまた用語を増やすんだよ。
- それでさらに、context=goal hypotheses（複数形）をfactsと言う。factsって、やっぱりcontextだったのか。
- goalはツリー構造、つまり入れ子なのでブロック構造だと思って、内側のほうのgoalのcontext=factsの要素であるproposition（=formula=termだと思う）を、localなassumptionとも言う。そろそろ呆れてきた。
- なんでこんなにも同義語、類義語が多いのか、、、、
分かってきたのは、ウェンツェルは、定理＝thm、コンテキスト＝Proof.context というイメージで話していること。だから、「ゴールとは定理である」とか言えるわけだ。「定理」という名のデータ構造だから。「ルールも定理」とか「定理もルール」とかも、同じデータ構造thmを使って表現しているから言っているのね。
酷い話だ。説明する側が実装に基づいて話していて、聞いている側は実装について知らない。しかも、実装は知らなくていい、むしろ積極的に知らせない方針なのに。
