11/06/13 13:47:54.24
Gunterってなんぞ？CPDTと関係あるのか？
51:デフォルトの名無しさん
11/06/13 21:42:28.31
Winskel の方が整理されてて良い、という人も多いが、
あれの良さがわからん。英語も変だし。
52:デフォルトの名無しさん
11/06/14 07:33:14.29
にわかだからYvesPierr、mathewぐらいしかわからん
53:デフォルトの名無しさん
11/06/15 09:33:20.44
>>52
> にわかだからYvesPierr、mathewぐらいしかわからん
さらにニワカなんで質問するんだけど、この２人ってどんな仕事してる人？
ググったけどわからない。
54:デフォルトの名無しさん
11/06/15 12:50:54.72
yvesはCoq'Artの著者の一人
matthieuは最近Coqに追加された機能Type Class, User defined equialities and relations, Program等の中心開発者
55:デフォルトの名無しさん
11/06/16 00:20:55.88
>>54
ありがとうございました。
52に"YvesPierr、mathew"って書いてるから "Yves Pierre"が一人の名前だと思ってググったんだけど
でもYvesとPierreは別々の２人それぞれのファーストネームということなんですね。
それじゃググってもわからなくて当たり前でした。
56:デフォルトの名無しさん
11/06/24 00:33:10.88
正直、この歳になって女子大生の夏休みを心待ちにすることになるとは思わんかった
57:46,49
11/06/24 01:41:20.53
>>50
> Gunterってなんぞ？CPDTと関係あるのか？
49を書いて久しく見てなかったんですまない、質問が出てたんだね
Gunterというのは次の本のことです
Carl A. Gunter "Semantics of Programming Languages" (MIT Press, 1992)
この本はプログラミング言語に対する表示的意味論の本なんだが
それに必要な領域理論（domain theory: cpoとかの構成法やその圏論的な定式化とか）を市販の教科書の中では一番詳しく書いてある
（その方面専門の数学の専門書ならもっと詳しいのはいくらでもあるが計算機屋向けだとこれが一番詳しい）
共立の朱色のシリーズから出ていた横内さんの『プログラム意味論』（もう品切れ放置プレーされてるのかな、それともまだ出てるか？）は
ある意味ではGunter本の基本部分を纏めたようなもの
横内さんの本が好きな人ならばGunter本も読んでとても楽しめると思う
ちなみにCPDTとは直接には無関係
90年代前半は社会全体もバブルの時代だったがフォーマルセマンティックスの分野も次々に良い本が出版されて一種のバブルみたいだったなあ
最近、そういう本の出版が少なくなって（フォーマルセマンティックスの出版バブルの後、型理論関係の本の出版が少し多かった時期はあるが）寂しかったので
CPDTが出るのは本当に楽しみ
58:デフォルトの名無しさん
11/06/24 08:29:55.36
>>57 トンクス
>>56 女子大生の夏休みワロタwww でも俺も楽しみwww
59:デフォルトの名無しさん
11/07/11 23:16:21.71
おねえさんの説明でさっぱりわからなかった俺用メモ
URLﾘﾝｸ(sunak2.cs.shinshu-u.ac.jp)
60:デフォルトの名無しさん
11/07/13 17:25:41.25
とてつもなく基本的な質問ではないかと思うのですが、
Definition prop1 : forall (A : Prop), A \/ ~A.
のような、仮定のない証明はどのようにすればいいのでしょうか？
プログラミングCoqの練習問題には
問3. forall (P : Prop), ~(P /\ ~P)
という、→のない証明の回答例がありますが、これは
一番外のnotを展開することで→Falseが発生しているのでそれを
使っているようです。
なにぶんCoqどころか論理学自体初心者なものですみません。
61:デフォルトの名無しさん
11/07/13 22:05:51.26
Require Import Classical.
Definition prop1 : forall (A : Prop), A \/ ~A.
apply classic.
Defined.
62:デフォルトの名無しさん
11/07/13 23:01:31.14
こらｗ
63:デフォルトの名無しさん
11/07/13 23:22:33.05
Require Import Classical.
Theorem eom : forall P:Prop, P \/ ~P.
intro P.
apply NNPP.
intro H.
elim H.
right.
intro p.
elim H.
left.
assumption.
Qed.
こんな知ってるか知らないかだし
CoqIDEなるProofGEneralなり使って一行ずつ動かしながらどうGoalが変化するか観察するのがいいよ
俺はそうやって覚えた
64:デフォルトの名無しさん
11/07/14 00:50:49.86
>>63
回答ありがとうございます。
「Proof-editing mode であそぼう」レベルの今の自分にはとても立ち向かえない
課題だったということがわかりました．．．
しかし、~(P /\ ~P) は割とあっさりできるのに、A \/ ~Aはいろいろ大変なあたり、
独学で自分で課題を決めて取り組む、というのがやりにくいですね。どの程度大変な
ものに向き合ってるのか、まだ読めないです。
学校で勉強したい・・・
65:デフォルトの名無しさん
11/07/14 01:14:11.89
流石に直感主義論理とNDの初歩ぐらい知っておかないとこの問題を自力で解くのは難しいかもしれない
とはいうものの簡単な数理論理学の教科書一冊読めばそれぐらいの力付くと思うけどね
独学なら
Coq'Art
URLﾘﾝｸ(www.labri.fr)
Software Foundations
URLﾘﾝｸ(www.cis.upenn.edu)
cpdt
URLﾘﾝｸ(adam.chlipala.net)
あたりがおすすめ
Coq'Art買えないというならSoftware Foundationsからかな
coq'artも課題の答えが著者のサイトで見れるから独学には向いてると思う
66:デフォルトの名無しさん
11/07/14 04:11:38.80
Coq'Art 中国語版あんのかよ。
専門書もサイトもソフトも、日本語訳って以前より減ってない?
67:60
11/07/15 00:34:49.12
>>65
ありがとうございます。とりあえずSoftware Foundationsから読み始めてみます。
Coq'Artが届いたらそちらにシフトしてみます。
もしよろしかったら、直感主義論理とかNDにたどり着けるような日本語の本も
ご教授いただけますか？
ちなみに今読んでいるのは、野崎先生の「不完全性定理（ちくま学芸文庫）」です。
とまぁ、こんなレベルなのですが・・・
持ってるだけですが、「論理と計算のしくみ」とか「圏論による論理学」とか
「計算可能性とラムダ計算」は手元にあります。
が、「この辺の本を読む前に読んでおくべき本があるはずだぁ」というのが素直な
感想です．．．
>>66
悲しいですがこれが現実なんですかね・・・
これ以上差をつめられないように（開かないように？）、がんばらないと。
68:デフォルトの名無しさん
11/07/15 00:43:58.72
>>67
その三冊なら論理と計算のしくみを読むのがいいかな
というかその本の演習問題に全く同じような証明問題があるから
69:60
11/07/15 01:02:59.55
>>68
今見直してみると、「論理と計算のしくみ」っていい本ですねこれ。
買ったときはラムダ計算のところが読みたかったので後半しか見てなかったのですが、
前半に論理学の基礎がてんこ盛りに整理されてますね。
一緒に取り組んでみます。ありがとうございます。
70:デフォルトの名無しさん
11/07/15 19:21:43.77
サイモン博士とニューウェル博士が最初の定理証明システムを手がけたときのことを想像してみる。
論文を読んだ人はプリンシピア・マセマティカを横に並べて読み進んだんじゃないだろうか？
小学校レベルでも高校レベルでもかまわないから、
数学の教科書と並行してCoqの基礎を学んでいけるテキストが欲しい。