11/03/13 23:15:04.74
興味はあるが……
3:デフォルトの名無しさん
11/03/13 23:48:36.06
Ｃｏｑ！Ｃｏｑ！Ｃｏｑ！Ｃｏｑぅぅうううわぁああああああああああああああああああああああん！！！
あぁああああ…ああ…あっあっー！あぁああああああ！！！ＣｏｑＣｏｑＣｏｑぅううぁわぁああああ！！！
あぁクンカクンカ！クンカクンカ！スーハースーハー！スーハースーハー！いい匂いだなぁ…くんくん
んはぁっ！ＰｒｏｏｆＧｅｎｅｒａｌたんの桃色ブロンドの髪をクンカクンカしたいお！クンカクンカ！あぁあ！！
間違えた！モフモフしたいお！モフモフ！モフモフ！髪髪モフモフ！カリカリモフモフ…きゅんきゅんきゅい！！
小説11巻のＣｏｑたんかわいかったよぅ！！あぁぁああ…あああ…あっあぁああああ！！ふぁぁあああんんっ！！
アニメ2期決まって良かったねＣｏｑたん！あぁあああああ！かわいい！Ｃｏｑたん！かわいい！あっああぁああ！
コミック2巻も発売されて嬉し…いやぁああああああ！！！にゃああああああああん！！ぎゃああああああああ！！
ぐあああああああああああ！！！コミックなんて現実じゃない！！！！あ…小説もアニメもよく考えたら…
Ｃ ｏ ｑ ち ゃ ん は 現実的 じ ゃ な い？にゃあああああああああああああん！！うぁああああああああああ！！
そんなぁああああああ！！いやぁぁぁあああああああああ！！はぁああああああん！！Ｒｏｃｑｕｅｎｃｏｕｒｔぅああああ！！
この！ちきしょー！やめてやる！！現実なんかやめ…て…え！？見…てる？ターミナルのＣｏｑちゃんが僕を見てる？
ターミナルのＣｏｑちゃんが僕を見てるぞ！Ｃｏｑちゃんが僕を見てるぞ！バッファのＣｏｑちゃんが僕を見てるぞ！！
アニメのＣｏｑちゃんが僕に話しかけてるぞ！！！よかった…世の中まだまだ捨てたモンじゃないんだねっ！
いやっほぉおおおおおおお！！！僕にはＣｏｑちゃんがいる！！やったよケティ！！ひとりでできるもん！！！
あ、コミックのＣｏｑちゃああああああああああああああん！！いやぁあああああああああああああああ！！！！
あっあんああっああんあアン様ぁあ！！セ、セイバー！！シャナぁああああああ！！！ヴィルヘルミナぁあああ！！
ううっうぅうう！！俺の想いよＣｏｑへ届け！！ＩＮＲＩＡのＣｏｑへ届け！
4:デフォルトの名無しさん
11/03/14 03:25:24.35
このスレッドは天才チンパンジー「アイちゃん」が
言語訓練のために立てたものです。
アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。
京都大学霊長類研究所
5:デフォルトの名無しさん
11/03/14 22:27:57.72
Gaaaaaaaaaaaaaze at my biiiiiiiiiiiig coooooooq!
6:デフォルトの名無しさん
11/03/16 01:00:21.48
これ日本にいるユーザ数ってどれくらいなの？
7:デフォルトの名無しさん
11/03/16 04:09:20.01
まともなレスがつかないから、だれか紹介サイトとかテンプレとか作ったらどう?
興味をそそるような紹介文とか書かないと、ほとんどの人は食いついてこないよ。
8:デフォルトの名無しさん
11/03/16 18:39:11.17
>>7
食いついたって仕方の無い言語
9:デフォルトの名無しさん
11/03/30 18:03:11.77
そうでもないよ
10:デフォルトの名無しさん
11/04/02 19:11:35.48
Coq は、INRIA にて開発されている対話的定理証明支援系です。 Calculus of Inductive Construction (CIC) を基礎とし、Tactics と呼ばれるコマンドを駆使することにより証明を行います。
URLﾘﾝｸ(www.eva-01.jp)
11:デフォルトの名無しさん
11/04/03 15:07:37.93
証明のゴルフ場があったぞ。ダレとくwww
URLﾘﾝｸ(d.hatena.ne.jp)
12:デフォルトの名無しさん
11/04/05 19:08:32.94
女子高生によるほんわかCoqチュートリアルキター！！！！
むねあつ！!!
URLﾘﾝｸ(www.iij-ii.co.jp)
13:デフォルトの名無しさん
11/04/05 20:17:12.22
＊ 「Coq！Coq！Coq！ どいつもこいつもCoq！
なぜだ！ なぜやつを認めて このおれを認めねえんだ！」
14:デフォルトの名無しさん
11/04/05 20:52:49.71
>>13
誰だお前？
15:デフォルトの名無しさん
11/04/05 21:23:47.27
>>13
Isabelle乙
16:デフォルトの名無しさん
11/04/11 13:03:53.15
>>15
実はAgdaじゃね？
こっちも依存型なのにCoqよりマイナーなのが悔しいとか。
17:デフォルトの名無しさん
11/04/11 21:38:42.94
>>16
Agdaの機能やシンタックスはかなりCoqにも影響を与えているよね。
id: forall {A: Type}, A -> A の{}とか。
国産の定理証明器だからぜひともがんばってほしいものだが。
18:デフォルトの名無しさん
11/04/12 00:50:38.97
>>17
確かに日本の人も貢献してるけど、北欧モノだよね？
19:デフォルトの名無しさん
11/04/19 00:36:34.38
Goal False <> True.
20:デフォルトの名無しさん
11/04/19 18:54:24.08
>>12
2章が公開されたね。
問5がわからない……
21:デフォルトの名無しさん
11/04/20 02:31:46.26
問5は apply (H (or P (~P))). がヒントかな
22:デフォルトの名無しさん
11/04/20 23:19:57.37
>>19
intro.
23:デフォルトの名無しさん
11/04/27 23:17:40.12
>>19
intro H.
symmetry in H.
induction H.
auto.
24:398
11/04/29 16:55:41.31
>>22
rewrite H.
25:デフォルトの名無しさん
11/05/11 19:39:05.96
>>12
読み始めたけど、素人っぽさはすごくあるな
初っぱなの"Definition"のDが大文字でなければならないことに注意が無かったり、
"Eval compute in"はプルダウンボックスから選ぶにもかかわらず、「左側のテキストボックスに……と打ち、」とか書いてあったり。
plus'やid'のアポストロフィが何の説明もなく出てきたり。
26:デフォルトの名無しさん
11/05/12 00:44:03.47
>>25
確かに説明はちょっと素人っぽいな。
しかし、少なくともCoqの知識はすごいな。高校生でCoqできるってなんか別の意味で人生楽しそうでいいな。
大人になったらなんの仕事をするんだろうか？
27:デフォルトの名無しさん
11/05/12 04:06:47.97
さては料理人だな
28:デフォルトの名無しさん
11/05/12 20:29:19.02
>>26
高校三年でCoqについて書けるのがすごいと思う。
フリーソフトの大部分は、高校レベルでは何するソフトかも想像できないのが普通だから。
将来は大学教授かテクニカルライターかな？
初学者の引っかかりやすい部分に注意を払えるようになって一人前なんだろうと思う。
大学で着実に勉強を重ねていって欲しいね。
29:デフォルトの名無しさん
11/05/12 20:58:15.53
俺も高校の時から英語の文献読んでたよ。
Coqは日本語の資料もあるし、それほど厳しくないと思われ
30:デフォルトの名無しさん
11/05/12 21:26:21.33
>>29
> Coqは日本語の資料もあるし、それほど厳しくないと思われ
どれのことですか？
教えてプリーズ。
自分は、高校数学の範囲は大人が思い出すよりかなり狭いと思うけどね。
述語論理、微分方程式の数値解法、品質管理に使う統計解析など、どれも高校数学には含まれない。
31:デフォルトの名無しさん
11/05/12 21:32:29.01
Coqで証明たてるのって、結構大変なんじゃないの？そこそこの経験者らしいよ。
相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。
32:デフォルトの名無しさん
11/05/12 21:57:28.35
英語よりも、数学の基礎知識が不足するんじゃないかと思うのだけど。
>>31
> 相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。
高校時代に偏微分方程式とか状態ベクトルとか推移行列とかヒルベルト空間とか？
内部進学者する人なら、高校時代に割と好きなこと勉強できるのかな？
33:デフォルトの名無しさん
11/05/12 23:55:42.39
与えられたものを必死で勉強する人間と、
自分で楽しい物を探して勉強する人間の違い。
優劣ではなく、ただの違い。
34:デフォルトの名無しさん
11/05/15 13:03:10.63
let と let recが違うのはカテゴリカルな意味が違うからだったはず。
CAMLってCategorical Abstract Machine Languageの略だし。
ソースは無い。
35:デフォルトの名無しさん
11/05/15 15:37:56.24
ML誤爆っすにゃ？
36:デフォルトの名無しさん
11/05/15 17:40:26.44
>>34
letrecの双対があるってこと？ほんまかいな。
37:デフォルトの名無しさん
11/05/16 20:28:28.05
双対？意味が違うから分けているんじゃないか、と言ってるだけだぞ。
スレチすまそ。
38:デフォルトの名無しさん
11/05/17 09:23:23.75
圏論でいう圏も哲学で使われる範疇も
どっちも英語としてはcategoryなんだよなややこしい
39:デフォルトの名無しさん
11/05/17 10:54:14.45
少なくともこのスレの文脈では全くややこしいことはなかった。
40:デフォルトの名無しさん
11/06/11 19:03:27.29
>>12
弱った。
チンプンカンプンだ。
説明が簡潔に過ぎる、ウルマンのMLの教科書などと比べて。
スタンフォード大学の偏差値の高い学生に教えるときですら、
ウルマンくらいの易しさが必要なのになあ。
41:デフォルトの名無しさん
11/06/11 21:24:53.86
自己紹介上手だね
42:40
11/06/11 21:58:40.74
山本和彦氏の指導の元で書かれたという前提で、さらに偏見を漏らしてみる。
山本和彦氏は自分がEngineerだと思っているようだ。
Educatorの発想が少し足りないのかもしれない。
Engineerは動くブラックボックスを作っていれば、
説明がテキトーでもバカにされることはない。
逆に、Educatorは理解できる説明をしなければならない。
ブラックボックスを作るとバカと呼ばれる。
43:デフォルトの名無しさん
11/06/11 23:22:40.14
アルバイトとかで、会社として管理職がいるだけじゃね？
本人は何やるかだけ承諾もらって、自由にやってるんだろう。
coqに興味あるなら、文章覚えるんじゃなくて、手を動かして覚えましょう。
44:デフォルトの名無しさん
11/06/11 23:33:59.32
教科書ほしいっていうのなら、
勉強会で使ってるのあるみたいだよ。
Certified Programming with Dependent Types
URLﾘﾝｸ(adam.chlipala.net)
URLﾘﾝｸ(adam.chlipala.net)
45:デフォルトの名無しさん
11/06/11 23:38:50.09
上階層貼ったほうがよかったね。ゴメン
URLﾘﾝｸ(adam.chlipala.net)
46:デフォルトの名無しさん
11/06/12 00:00:09.11
>>44-45
ありがとう
とても面白そうだね
MIT Pressから本としてももうすぐ出版されるみたいだね
最近、この手の分野の本の出版がほとんどなかったから楽しみ
ひところはGunterとかWinskelとかMitchellとかBruceとかどんどん出たのに
やっぱり本の形の方がディスプレイよりも目も疲れなくて読みやすいから
本が出たら買うことにしよう
47:デフォルトの名無しさん
11/06/12 00:01:46.38
>>44
英語は苦手ですが、ありがとうございます。
いろいろな試行をやってみるところまで、何とかたどり着きたいです。
48:デフォルトの名無しさん
11/06/12 23:46:24.58
こんなところでformal semanticsの専門家にでくわすとは
Gunterいいよね。
49:デフォルトの名無しさん
11/06/13 01:07:38.85
>>48
うん、Gunterのはとても良い本だよね
50:デフォルトの名無しさん
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の基礎を学んでいけるテキストが欲しい。
71:60
11/07/27 10:44:48.98
時間があったんで、
Software Foundations
URLﾘﾝｸ(www.cis.upenn.edu)
の「Basics」の章を全訳したんですけど、
公開するとまずいですよねぇ・・・・きっと。
巷にもう少し日本語の解説があれば普及も進むのでは
ないかと思うのですが。
72:デフォルトの名無しさん
11/07/27 12:14:00.96
Copyright書いてないね。
型理論の人たちは結構フリーで膨大なページ数のテキスト公開してるから聞いてみれば?
73:Matlab でもクラス記述できるでしょうか
11/07/27 12:49:09.99 BE:1370028454-2BP(0)
>> 公開するとまずいですよねぇ・・・・きっと。
原文のドキュメント作成者たちは無償で公開している。多くの方に読んでもらうためだ。
それを翻訳して公開するのに喜びこそすれ、嫌とは言わないだろう
もちろん、ドキュメント作成者の了解が前提になるが。
メールを出してみるべき。
74:60
11/07/27 13:46:38.43
ペンシルバニア大学の先生ですよね。ビビる・・・
CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
Software Foundationsのほうは、これをどうしたいのか、なんで
公開しているのか、どこにも書いてないんですよね。
メール出してもし許可がもらえたら、もう一度見直してボチボチ
公開したいところです。
まぁ、「４０代オッサンの夏休み」になりますが。
75:デフォルトの名無しさん
11/07/27 15:36:21.43
>>74
> CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
> Software Foundationsのほうは、これをどうしたいのか、なんで
> 公開しているのか、どこにも書いてないんですよね。
自分が担当している講義の為の資料を受講生以外の一般にも公開しているという事です。
このSoftware Foundationsに沿った形での講義をPierceさんらはやってますから。
（PierceさんのHPのTeachingの最初の科目、CIS500とかいう番号が付いてるやつです）
CPDTは明らかに本として出版するのを大前提として書かれてますし、本として読める単一ファイルの形でなっていますが、
こちらのSoftware Foundationsは少なくとも今の時点では紙に印刷される（か電子出版される）従来の書籍の形態にはなっていませんね。
マニュアルなどで良くあるWebページとリンクの集合体として現在は組織化されてますから、
当面は普通の書籍としては出版する予定はないように見えます。
もちろん、Pierceさんらが（少なからずが出版を最終目標とする）旧来型のPSやPDFの単一ファイルにしたものを
実は作っているが公開していないという可能性はゼロではありませんが、その可能性は少ないと思います。
76:60
11/07/27 16:23:12.05
>>75
よく見ると、前書きにその辺のことがチラッと書いてありましたね。跳ばして読んでました。
これによると、この文書を誰かが自分の講義に使うことは否定してませんね。
使う場合には連絡しろとも書いていない。
「ただ、そうするとどこかに直したいところや加筆したいところが出てくるだろうから、
そういうのがあったら連絡してね。subversionのレポジトリ教えてあげるから。」
てなことは書いてありますが。
この雰囲気だと、翻訳の公開を拒絶されそうな気配は無さそうですね、なんとなく。
77:デフォルトの名無しさん
11/07/27 22:47:28.23
あーそれだめだわ。
断られるわ。
78:デフォルトの名無しさん
11/07/27 23:09:04.95
>>75
coqdocだからPDFにはすぐ出来る。-pdf付けるだけ。
79:60
11/07/29 00:09:21.97
昨夜、Pierce先生にメールをしたところ、長文のお返事をいただき、
日本語版の公開を快諾していただきました。
ただ、公開間近の最新版がもうすぐ出来上がる予定で、今のとだいぶ変わって
いるので、それも考慮したほうがいいのではないのではとのことです。
ということなので、最新版とその差分が見られるよう、レポジトリの
アカウントを作っていただくことになりそうです。
とりあえず最新版を見せてもらって、あんまり変わってないようなら
今手元にあるのをさっさと公開しようと思っています。
80:デフォルトの名無しさん
11/07/29 00:37:49.56
やるじゃん
81:60
11/07/31 02:52:02.67
.vへのコピペに飽きてきたので暫定公開。
URLﾘﾝｸ(www.randmax.jp)
フォーマットがややオリジナルと異なりますが、二つ理由があります。
1. 僕がCSSを少しいじっているため。主に日本語対応。
2. sfのチームはcoqdocをカスタマイズして使っており、それを入手していないため。
単に「お前の翻訳はヘタ」というような批判は勘弁してください。「手伝ってください」としか言いようがありませんので。
具体的な「ここはたぶん誤解してる。正しくはこう」とか「この単語は普通こう訳す」というようなお話は歓迎します。
ここでやるのが不適切なようでしたら、どこかほかのところに場所を借りてもいいかと思っています。
「オレにもやらせろ」はもちろん「オレにやらせろ」も歓迎です。僕にとって翻訳は趣味でも仕事でもないので、日本語の文書が最初からあるなら（誰かが作ってくれるなら）、僕もそれに乗っかりたいぐらいです。
Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・
82:デフォルトの名無しさん
11/07/31 03:28:17.28
>>81
翻訳Webページに、参加方法やリポジトリ閲覧方法や訳文投稿窓口を含めておくと、敷居が低くなるかもしれない。
たとえばwikiのようなものとか。
83:デフォルトの名無しさん
11/07/31 07:59:42.65
>>81
> Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・
最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。
84:デフォルトの名無しさん
11/07/31 12:04:46.18
>>82の案を推す
俺もこのページは読んだことあるから多少は助力できるかも
85:デフォルトの名無しさん
11/07/31 15:20:26.31
>>81
誤字をなおしたりとかならお手伝いできるから、>>82みたいにしてくれるとうれしい
86:60
11/07/31 22:15:43.81
みなさんいろいろありがとうございます。
Wikiについては、だいぶ更新がとまっているCoqWikiがなるものがあるので間借りすることも考えたのですが、
たいしたコストがかかるわけでもなさそうなので、どこか別に借りてみようかと思います。
準備ができたらそちらも追って公開します。
とりあえず明日には、Basicsの全体を暫定公開できると思います。
そうこうしているうちにSVNレポジトリのアカウントが届くのではないかと。
なんだか長い旅になりそうですが、ひとつ気長にお付き合いください。m(_ _)m
>>83
>最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。
僕もそう思うんですけど、本当言うと学生さんに頑張ってほしいんですよね。
こういう日本で開拓の進んでない分野に切り込んで貢献する体験を若い人に沢山積んで欲しいと思うのです。
僕など成長したところで先が知れてますんで。
だからといって若い人に「お前がやれ」というのもかっこ悪い大人だと思うので、自分でやってしまったのですが。
どこかで誰かが「しまった！僕が先にやっておけばよかった！」と後悔してくれていればいいなと。
87:60
11/08/01 23:22:27.01
とりあえずWikiを借りてみました。
URLﾘﾝｸ(www16.atwiki.jp)
特に制限などつけていませんが、できればWikiに参加してログインを行って書き込んでいただけると安心できます。
僕の身分は自己紹介のとこからリンクをたどっていくとわかるようになっています。
大した者ではありませんが、怪しい者でもありません。
皆様のご参加をお待ちしております。
88:デフォルトの名無しさん
11/08/02 21:26:40.40
>>87
『ソフィーの世界』、関係ねぇwww
これも何かの縁だと思って、正義論とか心の哲学とかも読もうぜ
89:60
11/08/02 22:59:31.02
今日いろいろ調べ物をしていて仰天しました。
僕が先月下旬ごろノートに一生懸命翻訳を書いている間に、
「プログラミング言語の基礎概念」という本が、サイエンス社から出版されていたのですね！
しかも著者は、ラクダ（OCaml）本の五十嵐淳先生。ペンシルバニア大でPierce先生と机を並べていたこともあるという。
一瞬、「Software Foundations」の翻訳が出たのかと思ったのですが、会社の帰りに日本橋丸善に寄って探すと、別の本でした。
とはいえ、内容的にはチョコチョコ重なっているところもあり（OCamlですが）、日本語で書き下されているものなので非常に読みやすいし、わかりやすいです。
これはお勧め。1850円というのもびっくりリーゾナブルです。
ここ見ているような人は内容的に目新しくないのかもしれませんが・・・
90:デフォルトの名無しさん
11/08/03 09:00:22.23
とりあえずwikiの下の方の広告をクリックしまくっておいた。
91:デフォルトの名無しさん
11/08/03 13:36:59.98
なんだそのブログみたいな文体は
92:60
11/08/04 00:34:58.51
>>90
お気遣い、とてもありがたいのですが、
Wikiの広告をクリックしていただいても僕には１円も入りません・・・・単にWikiサーバの運営費と運営会社の利益になるだけでだと思います。
もちろんクリックしても何の問題もないとは思いますが。
93:デフォルトの名無しさん
11/08/04 23:04:14.47
>>92
早とちりで失礼しました。
94:60
11/08/15 22:52:35.14
本日、日本語版を一応リリースいたしました。Pierce先生にもその旨連絡しました。
Basicsまでは、そこそこの完成度の翻訳になっているつもりですが、何かお気づきの点がありましたらWikiにお願いします。
僕自身もこれを翻訳した後、自分の日本語を読みながら一通り課題をやりましたが、
難易度が上がっていくペースがなかなかいい教材なのではないかと思います。
未来嬢の「プログラミングCoq」と併せてとりくんでもらえるといいかなと。
95:デフォルトの名無しさん
11/09/05 17:35:48.93
型定義、関数シグニチャを提供して、
ユーザーに関数の中身を定義してもらう枠組みを考えてるんだけど、
ある種の制約を守れば正しく動作する関数が定義できますよ、としたいんだけど、
そのときの制約として、
・関数シグニチャに沿っていること
・こちらで定義した補助関数のうち、絶対に使っちゃいけないものがある
・関数の中はCoqに通り、上2つの制約に矛盾しなければ何でもOK
というようにするには、どうしたらいいんでしょうか。
最初のは多分Classとして与え、
ユーザーにInstance化してもらえばいいんだけど、
2個目の条件が満されていることはどうやって確認したらいいんですかね?
96:デフォルトの名無しさん
11/09/07 17:55:08.74
確かextraction機構はプラグインみたいな形でコア部分と別だったから
Extractionする段階で、定義済みの関数の式木を舐めて特定の名前の関数を使用しているかいないかで判定とかは可能だと思う
97:デフォルトの名無しさん
11/10/03 09:45:16.35
RT @mzp #sfja URLﾘﾝｸ(proofcafe.org) SoftwareFoundation和訳(4章まで)
98:デフォルトの名無しさん
11/10/03 10:00:02.78
もしし
99:デフォルトの名無しさん
11/10/14 22:55:59.64
>> 60さん
あれ、Software Foundationsの場所変わったの？
作業場所もwikiからGithubに変わったみたいだけど、運営者かわったの？
100:デフォルトの名無しさん
11/10/14 23:09:28.89
wikiに説明が書いてあると思うが
101:デフォルトの名無しさん
11/10/14 23:09:59.10
>>githubの方は60さんに刺激を受けたfm forumの人がやってるやつで完全に二つは独立してるよ
102:デフォルトの名無しさん
11/10/15 22:24:07.91
>>101
なるほど。ありがとうございます。見た感じ今はgithubの方が勢いがあるのかな？
103:デフォルトの名無しさん
11/10/16 10:55:36.52
>>101
実際は、60が10月から忙しくなったのでProofSummit で協力をよびかけて、賛同者の作業がやりやすいようGithubに移行したということです。60もGithubに参加しています。
104:デフォルトの名無しさん
11/10/16 10:58:10.00
それは知らなかった説明ありがとう
105:デフォルトの名無しさん
11/10/16 12:24:15.43
>>103
うん？どういうこと？
二つは独立しているのではなく、作業場所が変更したってこと？
最新の作業情報はgithubのプロジェクトをみればよい？
106:60
11/10/16 12:36:30.91
>>105
そういうことです。
Github のほうが真(新)です。
Wiki のほうは、その事がちゃんと分かるように直しておきます。
107:デフォルトの名無しさん
11/10/16 22:06:31.22
>>106 わかりました。ありがとうございます。
108:デフォルトの名無しさん
11/10/17 09:21:46.34
@n_k28 魔理沙気持ち悪かったです。もう二度とやらないで下さい＾＾
109:デフォルトの名無しさん
11/10/27 22:46:35.48
(P -> Q) -> (~P \/ Q)
これの証明ができん。
110:デフォルトの名無しさん
11/10/27 22:54:20.25
ああ
~~((P -> Q) -> (~P \/ Q))
なら証明できるのか。
直観主義論理がどうとか俺にはちんぷんかんぷんだ…。
111:デフォルトの名無しさん
11/10/30 10:33:11.77
tauto.でおｋ
112:デフォルトの名無しさん
11/11/11 16:16:46.14
Inductiveな型TからT_rectが生成される原理がどうしてもわからないなあ。
誰か教えてちょーだいな。
113:デフォルトの名無しさん
11/11/12 05:51:58.15
#coq #inductive
>>112 例えば nat_rectならFixpointでも定義できるよ。
Variable P : nat -> Type.
Axiom fO : P O.
Axiom fS : forall n, P n -> P (S n).
Fixpoint nat_rect' n : P n :=
match n with
| O => fO
| S m => fS m (nat_rect' m)
end.
114:112
11/11/12 12:04:00.72
nat_rectぐらいなら、数学的帰納法なんてなじみがあるからなんとなくわかるけど、
例えば
Inductive sand (A B : Set) : Set :=
sconj : A -> B -> sand A B.
から作られるsand_rectなんかは、
sand_rect =
fun (A B : Set) (P : sand A B -> Type)
(f : forall (a : A) (b : B), P (sconj A B a b)) (s : sand A B) =>
match s as s0 return (P s0) with
| sconj x x0 => f x x0
end
: forall (A B : Set) (P : sand A B -> Type),
(forall (a : A) (b : B), P (sconj A B a b)) ->
forall s : sand A B, P s
となって、わかりそうなわからなそうな。上記のSetをPropにかえるともうお手上げ。
いったい何を理解すればいいのやら。どうか神様教えて。
115:デフォルトの名無しさん
11/11/12 12:39:28.72
>>114 nat以外のものも構造的帰納法を表しているだけ。
X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても
型だけわかれば、使えるからそれで いいと思う。
このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが
知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。
116:112
11/11/12 16:10:50.99
>>115
ということは、構造的帰納法について、私が理解している以上に何か深いこと、
あるいは、もっと詳しいことがあるということでしょうか。論理式の定義に従って
帰納的に何かを証明するとか、そんなことは何の苦もなく理解してきましたけど、
上記>>114のsand_rectなんぞは、なぜそうなるのかいまひとつわからないのです。
また、sandの定義中のSetをPropにかえたものをpandとすると、pand_rectは
sand_rectのSetをPropにかえただけのものとは異なります。ますますわかりません。
もし構造的帰納法について詳しく書かれた文献等あったらご紹介いただけないで
しょうか。
117:112
11/11/12 20:54:41.74
少しだけわかってきました。sand_rectの型の部分がそうなりそうな気もしてきました。
すると、本体（t:Tにおけるtのこと）がなぜそのように構成されるのか、という疑問に
なりますが、それは半分は発見的経験的に考えないといけないのでしょうか。
また、pand_rectに関しては、sand_rectの(P : sand A B -> Type)の部分が
なぜか(P : Type)になっている。つまりsand_rectにあるPはsand A Bを引数にとってたのに、
pand_rectにあるPはpand A Bを引数にとらなくなっている。
これさえ認めればsand_rectとpand_rectの違いは説明できます。これはなぜなんでしょう？
118:112
11/11/13 09:55:45.41
少しずつわかってくるにつれて、Coqとは直接関係ない気もしてきたのですが、
どなたか教えてくださるか、もしくは良い文献の紹介等していただけないで
しょうか。
自然数の定義を例に話します。
（１）Oを自然数とする。
（２）nを自然数とするとき、S nも自然数とする。
（３）上記（１）（２）によって定められるもののみを自然数とする。
といった具合に自然数を定義することができますが、この（３）をどのように
形式的に表すかをもっと詳しく理解すれば、私の疑問が解けるような気がしてき
ました。
どうか偉い方々、よろしくお願いいたします。
119:デフォルトの名無しさん
11/11/13 15:44:37.16
Coq'Artの14章あたりにもある程度載ってるんだけども形式的な説明というわけでは無いね
論理や集合論の命題と型付きラムダ計算の式が1対1対応するっていう性質を使ってるってことは聞くけど
再帰型の定義が計算体系に及ぼす影響が対応する論理体系にどういう影響与えるかとか
そういうのはよくわからない・・・
せいぜい構築子の無い型の値を仮定するのとFalseぶち込むのが対応してどちらも滅茶苦茶になるとか、そういうのぐらい
::=はiffに対応するとか|は排他論理和に対応するんだなぁというのは経験則でみえてくるけども
120:デフォルトの名無しさん
11/11/13 19:01:45.89
×型付きﾗﾑﾀﾞ計算の式
○型付きﾗﾑﾀﾞ計算の型
121:デフォルトの名無しさん
11/11/19 09:32:29.84
>>118 構造的帰納法に関しては俺はTAPLで勉強したな。あの本は丁寧で
わかりやすい。
122:112
11/11/21 12:32:03.21
>>119-121
いろいろと情報提供ありがとうございます。いまはCoq'Artの14章で奮闘中です。もともと英語が苦手
なのですが、贅沢は言ってられません。TAPLって、Benjamin C. Pierceの「Types and Programming
Languages」のことですよね。あたってみます。（砕けたりして。トホホ）
123:デフォルトの名無しさん
12/02/10 07:07:56.25
URLﾘﾝｸ(proofcafe.org) に日本語訳を上げて下さっている方の書き込みがあったので、ここに書いておきます。
一部訳に打ち間違いがあります。どこに言ったら良いのかわからないので、ここに書いておきます。
URLﾘﾝｸ(proofcafe.org)
の[マップ（Map）関数]のちょっと上に「理宇土」とあります多分「リスト」の誤変換だと思います。
この訳のお陰で大変楽して勉強できてます。ありがとうございます。
124:デフォルトの名無しさん
12/02/10 09:10:05.55
URLﾘﾝｸ(proofcafe.org)
の
rememberタクティック
のちょっと前に「なるべくintrosを使うタイミングを送らせ」の「送らせ」は「遅らせ」だと思います。
よろしくお願い致します。
訳ありがとうございます。
125:デフォルトの名無しさん
12/02/10 09:35:05.24
報告するならgithubのissue tracker
URLﾘﾝｸ(github.com)
か
wikiの専用ページ
URLﾘﾝｸ(www16.atwiki.jp)
でやるほうがいいと思うよ
126:デフォルトの名無しさん
12/02/10 17:57:06.05
>125
ありがとうございます。そっちに書いときます。
127:デフォルトの名無しさん
12/02/11 16:49:49.67
うわーはずかしいtypo。直しておきます。レポート感謝。
128:デフォルトの名無しさん
12/02/16 10:19:23.91
0 と 1 だけのタイプを作りたいと思い
Inductive my : Type := O : my .
my is defined
my_rect is defined
my_ind is defined
my_rec is defined
は上手く動作するのですが
Coq < Reset my.
Coq < Inductive my : Type := O : my | 1 : my .
Toplevel input, characters 32-33:
> Inductive my : Type := O : my | 1 : my .
> ^
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
Coq < Inductive my : Type := O : my | (S O) : my .
Toplevel input, characters 32-33:
> Inductive my : Type := O : my | (S O) : my .
> ^
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
となって上手く定義できません。どうやれば 0 と 1 だけのタイプを定義できるんでしょうか。
129:デフォルトの名無しさん
12/02/16 13:24:10.57
Inductiveで列挙するのはコンストラクタの名前とその型。
値を並べられるわけではない。
130:デフォルトの名無しさん
12/02/16 22:24:41.28
1を名前に使えない
Inductive my : Type := O : my | one : my .
ならいい
131:デフォルトの名無しさん
12/02/18 11:13:09.87
O(:nat)もコンストラクターなんじゃない？
132:デフォルトの名無しさん
12/02/26 23:56:37.37
なんか >>60 が変な扉を開いてしまったかもしれない。
「関数型ガール」
URLﾘﾝｸ(www16.atwiki.jp)
133:デフォルトの名無しさん
12/03/09 10:10:41.05
>129
>130
>131
>132
回答ありがとうございます。
134:デフォルトの名無しさん
12/03/09 10:17:33.18
O を起点として
O と (S O) だけの Typeとか
O と (S O) と (S (S O)) だけの Type とか
O と (S O) と (S (S O)) と (S (S (S O))) だけのTypeとか
...
を作りたかったのですが、そうするにはどういうコマンド入れたら良いのでしょうか>
レベル低い質問ですみません。
Inductive my : Type := O : my | S : my -> my.
こうしちゃうと O と (S O)だけじゃなく (S (S O))も myタイプになってしまうのでどうしたらよいのかわかりません。
135:デフォルトの名無しさん
12/03/09 10:57:54.37
>>134
証明を引数として取るコンストラクタを使うとか
Require Import Arith.
Inductive my (n:nat) : Set :=
| myO : my n
| myS a : a <= n -> my n.
Section my1.
Let my1 := my 1.
Definition my1_0 : my1 := myO 1.
Program Definition my1_1 : my1 := myS _ 1 _.
End my1.
136:デフォルトの名無しさん
12/03/09 23:40:56.06
Inductive Fin : nat -> Type :=
| FinO n : Fin (S n)
| FinS n : Fin n -> Fin (S n).
というのをcoq-clubで見た。
137:名無しさん
12/03/15 01:21:22.24
ネット務
138:デフォルトの名無しさん
12/03/20 10:49:54.36
>>135
>>136
ありがとうございました。
またやってみます。
139:デフォルトの名無しさん
12/04/19 09:20:01.83
Software Foumdationsの翻訳がとりあえず最後まで終わりました！
というわけでお願いなのですが、読んでください。
で、誤字脱字誤訳など指摘頂けると助かります。