http://coq.inria.fr/
あぁああああ…ああ…あっあっー！あぁああああああ！！！ＣｏｑＣｏｑＣｏｑぅううぁわぁああああ！！！
あぁクンカクンカ！クンカクンカ！スーハースーハー！スーハースーハー！いい匂いだなぁ…くんくん
んはぁっ！ＰｒｏｏｆＧｅｎｅｒａｌたんの桃色ブロンドの髪をクンカクンカしたいお！クンカクンカ！あぁあ！！
間違えた！モフモフしたいお！モフモフ！モフモフ！髪髪モフモフ！カリカリモフモフ…きゅんきゅんきゅい！！
小説11巻のＣｏｑたんかわいかったよぅ！！あぁぁああ…あああ…あっあぁああああ！！ふぁぁあああんんっ！！
アニメ2期決まって良かったねＣｏｑたん！あぁあああああ！かわいい！Ｃｏｑたん！かわいい！あっああぁああ！
コミック2巻も発売されて嬉し…いやぁああああああ！！！にゃああああああああん！！ぎゃああああああああ！！
ぐあああああああああああ！！！コミックなんて現実じゃない！！！！あ…小説もアニメもよく考えたら…
Ｃ ｏ ｑ ち ゃ ん は 現実的 じ ゃ な い？にゃあああああああああああああん！！うぁああああああああああ！！
そんなぁああああああ！！いやぁぁぁあああああああああ！！はぁああああああん！！Ｒｏｃｑｕｅｎｃｏｕｒｔぅああああ！！
この！ちきしょー！やめてやる！！現実なんかやめ…て…え！？見…てる？ターミナルのＣｏｑちゃんが僕を見てる？
ターミナルのＣｏｑちゃんが僕を見てるぞ！Ｃｏｑちゃんが僕を見てるぞ！バッファのＣｏｑちゃんが僕を見てるぞ！！
アニメのＣｏｑちゃんが僕に話しかけてるぞ！！！よかった…世の中まだまだ捨てたモンじゃないんだねっ！
いやっほぉおおおおおおお！！！僕にはＣｏｑちゃんがいる！！やったよケティ！！ひとりでできるもん！！！
あ、コミックのＣｏｑちゃああああああああああああああん！！いやぁあああああああああああああああ！！！！
あっあんああっああんあアン様ぁあ！！セ、セイバー！！シャナぁああああああ！！！ヴィルヘルミナぁあああ！！
ううっうぅうう！！俺の想いよＣｏｑへ届け！！ＩＮＲＩＡのＣｏｑへ届け！
言語訓練のために立てたものです。
アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。
京都大学霊長類研究所
興味をそそるような紹介文とか書かないと、ほとんどの人は食いついてこないよ。
食いついたって仕方の無い言語
http://www.eva-01.jp/wiki/pukiwiki.php?Coq
http://d.hatena.ne.jp/kikx/20100807
むねあつ！!!
http://www.iij-ii.co.jp/lab/techdoc/coqt/
なぜだ！ なぜやつを認めて このおれを認めねえんだ！」
誰だお前？
Isabelle乙
実はAgdaじゃね？
こっちも依存型なのにCoqよりマイナーなのが悔しいとか。
Agdaの機能やシンタックスはかなりCoqにも影響を与えているよね。
id: forall {A: Type}, A -> A の{}とか。
国産の定理証明器だからぜひともがんばってほしいものだが。
確かに日本の人も貢献してるけど、北欧モノだよね？
2章が公開されたね。
問5がわからない……
intro.
intro H.
symmetry in H.
induction H.
auto.
rewrite H.
読み始めたけど、素人っぽさはすごくあるな
初っぱなの"Definition"のDが大文字でなければならないことに注意が無かったり、
"Eval compute in"はプルダウンボックスから選ぶにもかかわらず、「左側のテキストボックスに……と打ち、」とか書いてあったり。
plus'やid'のアポストロフィが何の説明もなく出てきたり。
確かに説明はちょっと素人っぽいな。
しかし、少なくともCoqの知識はすごいな。高校生でCoqできるってなんか別の意味で人生楽しそうでいいな。
大人になったらなんの仕事をするんだろうか？
高校三年でCoqについて書けるのがすごいと思う。
フリーソフトの大部分は、高校レベルでは何するソフトかも想像できないのが普通だから。
将来は大学教授かテクニカルライターかな？
初学者の引っかかりやすい部分に注意を払えるようになって一人前なんだろうと思う。
大学で着実に勉強を重ねていって欲しいね。
Coqは日本語の資料もあるし、それほど厳しくないと思われ
> Coqは日本語の資料もあるし、それほど厳しくないと思われ
どれのことですか？
教えてプリーズ。
自分は、高校数学の範囲は大人が思い出すよりかなり狭いと思うけどね。
述語論理、微分方程式の数値解法、品質管理に使う統計解析など、どれも高校数学には含まれない。
相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。
>>31
> 相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。
高校時代に偏微分方程式とか状態ベクトルとか推移行列とかヒルベルト空間とか？
内部進学者する人なら、高校時代に割と好きなこと勉強できるのかな？
自分で楽しい物を探して勉強する人間の違い。
優劣ではなく、ただの違い。
CAMLってCategorical Abstract Machine Languageの略だし。
ソースは無い。
letrecの双対があるってこと？ほんまかいな。
スレチすまそ。
どっちも英語としてはcategoryなんだよなややこしい
弱った。
vンカンプンだ。
説明が簡潔に過ぎる、ウルマンのMLの教科書などと比べて。
スタンフォード大学の偏差値の高い学生に教えるときですら、
ウルマンくらいの易しさが必要なのになあ。
山本和彦氏は自分がEngineerだと思っているようだ。
Educatorの発想が少し足りないのかもしれない。
Engineerは動くブラックボックスを作っていれば、
説明がテキトーでもバカにされることはない。
逆に、Educatorは理解できる説明をしなければならない。
ブラックボックスを作るとバカと呼ばれる。
本人は何やるかだけ承諾もらって、自由にやってるんだろう。
coqに興味あるなら、文章覚えるんじゃなくて、手を動かして覚えましょう。
勉強会で使ってるのあるみたいだよ。
Certified Programming with Dependent Types
http://adam.chlipala.net/cpdt/html/toc.html
http://adam.chlipala.net/cpdt/cpdt.pdf
http://adam.chlipala.net/cpdt/
ありがとう
とても面白そうだね
MIT Pressから本としてももうすぐ出版されるみたいだね
最近、この手の分野の本の出版がほとんどなかったから楽しみ
ひところはGunterとかWinskelとかMitchellとかBruceとかどんどん出たのに
やっぱり本の形の方がディスプレイよりも目も疲れなくて読みやすいから
本が出たら買うことにしよう
英語は苦手ですが、ありがとうございます。
いろいろな試行をやってみるところまで、何とかたどり着きたいです。
Gunterいいよね。
うん、Gunterのはとても良い本だよね
あれの良さがわからん。英語も変だし。
> にわかだからYvesPierr、mathewぐらいしかわからん
さらにニワカなんで質問するんだけど、この２人ってどんな仕事してる人？
ググったけどわからない。
matthieuは最近Coqに追加された機能Type Class, User defined equialities and relations, Program等の中心開発者
ありがとうございました。
52に"YvesPierr、mathew"って書いてるから "Yves Pierre"が一人の名前だと思ってググったんだけど
でもYvesとPierreは別々の２人それぞれのファーストネームということなんですね。
それじゃググってもわからなくて当たり前でした。
> Gunterってなんぞ？CPDTと関係あるのか？
49を書いて久しく見てなかったんですまない、質問が出てたんだね
Gunterというのは次の本のことです
Carl A. Gunter "Semantics of Programming Languages" (MIT Press, 1992)
この本はプログラミング言語に対する表示的意味論の本なんだが
それに必要な領域理論（domain theory: cpoとかの構成法やその圏論的な定式化とか）を市販の教科書の中では一番詳しく書いてある
（その方面専門の数学の専門書ならもっと詳しいのはいくらでもあるが計算機屋向けだとこれが一番詳しい）
共立の朱色のシリーズから出ていた横内さんの『プログラム意味論』（もう品切れ放置プレーされてるのかな、それともまだ出てるか？）は
ある意味ではGunter本の基本部分を纏めたようなもの
横内さんの本が好きな人ならばGunter本も読んでとても楽しめると思う
ちなみにCPDTとは直接には無関係
90年代前半は社会全体もバブルの時代だったがフォーマルセマンティックスの分野も次々に良い本が出版されて一種のバブルみたいだったなあ
最近、そういう本の出版が少なくなって（フォーマルセマンティックスの出版バブルの後、型理論関係の本の出版が少し多かった時期はあるが）寂しかったので
CPDTが出るのは本当に楽しみ
>>56 女子大生の夏休みワロタwww でも俺も楽しみwww
ttp://sunak2.cs.shinshu-u.ac.jp/~miyao/UD/Subjects/Kouri/logic.htm
Definition prop1 : forall (A : Prop), A \/ ~A.
のような、仮定のない証明はどのようにすればいいのでしょうか？
プログラミングCoqの練習問題には
問3. forall (P : Prop), ~(P /\ ~P)
という、→のない証明の回答例がありますが、これは
一番外のnotを展開することで→Falseが発生しているのでそれを
使っているようです。
なにぶんCoqどころか論理学自体初心者なものですみません。
Definition prop1 : forall (A : Prop), A \/ ~A.
apply classic.
Defined.
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が変化するか観察するのがいいよ
俺はそうやって覚えた
回答ありがとうございます。
「Proof-editing mode であそぼう」レベルの今の自分にはとても立ち向かえない
課題だったということがわかりました．．．
しかし、~(P /\ ~P) は割とあっさりできるのに、A \/ ~Aはいろいろ大変なあたり、
独学で自分で課題を決めて取り組む、というのがやりにくいですね。どの程度大変な
ものに向き合ってるのか、まだ読めないです。
学校で勉強したい・・・
とはいうものの簡単な数理論理学の教科書一冊読めばそれぐらいの力付くと思うけどね
独学なら
Coq'Art
http://www.labri.fr/perso/casteran/CoqArt/index.html
Software Foundations
http://www.cis.upenn.edu/~bcpierce/sf/toc.html
cpdt
http://adam.chlipala.net/cpdt/
あたりがおすすめ
Coq'Art買えないというならSoftware Foundationsからかな
coq'artも課題の答えが著者のサイトで見れるから独学には向いてると思う
専門書もサイトもソフトも、日本語訳って以前より減ってない?
ありがとうございます。とりあえずSoftware Foundationsから読み始めてみます。
Coq'Artが届いたらそちらにシフトしてみます。
もしよろしかったら、直感主義論理とかNDにたどり着けるような日本語の本も
ご教授いただけますか？
ちなみに今読んでいるのは、野崎先生の「不完全性定理（ちくま学芸文庫）」です。
とまぁ、こんなレベルなのですが・・・
持ってるだけですが、「論理と計算のしくみ」とか「圏論による論理学」とか
「計算可能性とラムダ計算」は手元にあります。
が、「この辺の本を読む前に読んでおくべき本があるはずだぁ」というのが素直な
感想です．．．
>>66
悲しいですがこれが現実なんですかね・・・
これ以上差をつめられないように（開かないように？）、がんばらないと。
その三冊なら論理と計算のしくみを読むのがいいかな
というかその本の演習問題に全く同じような証明問題があるから
今見直してみると、「論理と計算のしくみ」っていい本ですねこれ。
買ったときはラムダ計算のところが読みたかったので後半しか見てなかったのですが、
前半に論理学の基礎がてんこ盛りに整理されてますね。
一緒に取り組んでみます。ありがとうございます。
論文を読んだ人はプリンシピア・マセマティカを横に並べて読み進んだんじゃないだろうか？
小学校レベルでも高校レベルでもかまわないから、
数学の教科書と並行してCoqの基礎を学んでいけるテキストが欲しい。
Software Foundations
http://www.cis.upenn.edu/~bcpierce/sf/toc.html
の「Basics」の章を全訳したんですけど、
公開するとまずいですよねぇ・・・・きっと。
巷にもう少し日本語の解説があれば普及も進むのでは
ないかと思うのですが。
型理論の人たちは結構フリーで膨大なページ数のテキスト公開してるから聞いてみれば?
原文のドキュメント作成者たちは無償で公開している。多くの方に読んでもらうためだ。
それを翻訳して公開するのに喜びこそすれ、嫌とは言わないだろう
もちろん、ドキュメント作成者の了解が前提になるが。
メールを出してみるべき。
CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
Software Foundationsのほうは、これをどうしたいのか、なんで
公開しているのか、どこにも書いてないんですよね。
メール出してもし許可がもらえたら、もう一度見直してボチボチ
公開したいところです。
まぁ、「４０代オッサンの夏休み」になりますが。
> CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
> Software Foundationsのほうは、これをどうしたいのか、なんで
> 公開しているのか、どこにも書いてないんですよね。
自分が担当している講義の為の資料を受講生以外の一般にも公開しているという事です。
このSoftware Foundationsに沿った形での講義をPierceさんらはやってますから。
（PierceさんのHPのTeachingの最初の科目、CIS500とかいう番号が付いてるやつです）
CPDTは明らかに本として出版するのを大前提として書かれてますし、本として読める単一ファイルの形でなっていますが、
こちらのSoftware Foundationsは少なくとも今の時点では紙に印刷される（か電子出版される）従来の書籍の形態にはなっていませんね。
マニュアルなどで良くあるWebページとリンクの集合体として現在は組織化されてますから、
当面は普通の書籍としては出版する予定はないように見えます。
もちろん、Pierceさんらが（少なからずが出版を最終目標とする）旧来型のPSやPDFの単一ファイルにしたものを
実は作っているが公開していないという可能性はゼロではありませんが、その可能性は少ないと思います。
よく見ると、前書きにその辺のことがチラッと書いてありましたね。跳ばして読んでました。
これによると、この文書を誰かが自分の講義に使うことは否定してませんね。
使う場合には連絡しろとも書いていない。
「ただ、そうするとどこかに直したいところや加筆したいところが出てくるだろうから、
そういうのがあったら連絡してね。subversionのレポジトリ教えてあげるから。」
てなことは書いてありますが。
この雰囲気だと、翻訳の公開を拒絶されそうな気配は無さそうですね、なんとなく。
断られるわ。
coqdocだからPDFにはすぐ出来る。-pdf付けるだけ。
日本語版の公開を快諾していただきました。
ただ、公開間近の最新版がもうすぐ出来上がる予定で、今のとだいぶ変わって
いるので、それも考慮したほうがいいのではないのではとのことです。
ということなので、最新版とその差分が見られるよう、レポジトリの
アカウントを作っていただくことになりそうです。
とりあえず最新版を見せてもらって、あんまり変わってないようなら
今手元にあるのをさっさと公開しようと思っています。
http://www.randmax.jp/sf/Basics_J.html
フォーマットがややオリジナルと異なりますが、二つ理由があります。
1. 僕がCSSを少しいじっているため。主に日本語対応。
2. sfのチームはcoqdocをカスタマイズして使っており、それを入手していないため。
単に「お前の翻訳はヘタ」というような批判は勘弁してください。「手伝ってください」としか言いようがありませんので。
具体的な「ここはたぶん誤解してる。正しくはこう」とか「この単語は普通こう訳す」というようなお話は歓迎します。
ここでやるのが不適切なようでしたら、どこかほかのところに場所を借りてもいいかと思っています。
「オレにもやらせろ」はもちろん「オレにやらせろ」も歓迎です。僕にとって翻訳は趣味でも仕事でもないので、日本語の文書が最初からあるなら（誰かが作ってくれるなら）、僕もそれに乗っかりたいぐらいです。
Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・
翻訳Webページに、参加方法やリポジトリ閲覧方法や訳文投稿窓口を含めておくと、敷居が低くなるかもしれない。
たとえばwikiのようなものとか。
> Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・
最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。
俺もこのページは読んだことあるから多少は助力できるかも
誤字をなおしたりとかならお手伝いできるから、>>82みたいにしてくれるとうれしい
Wikiについては、だいぶ更新がとまっているCoqWikiがなるものがあるので間借りすることも考えたのですが、
たいしたコストがかかるわけでもなさそうなので、どこか別に借りてみようかと思います。
準備ができたらそちらも追って公開します。
とりあえず明日には、Basicsの全体を暫定公開できると思います。
そうこうしているうちにSVNレポジトリのアカウントが届くのではないかと。
なんだか長い旅になりそうですが、ひとつ気長にお付き合いください。m(_ _)m
>>83
>最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。
僕もそう思うんですけど、本当言うと学生さんに頑張ってほしいんですよね。
こういう日本で開拓の進んでない分野に切り込んで貢献する体験を若い人に沢山積んで欲しいと思うのです。
僕など成長したところで先が知れてますんで。
だからといって若い人に「お前がやれ」というのもかっこ悪い大人だと思うので、自分でやってしまったのですが。
どこかで誰かが「しまった！僕が先にやっておけばよかった！」と後悔してくれていればいいなと。
http://www16.atwiki.jp/sf_j/
特に制限などつけていませんが、できればWikiに参加してログインを行って書き込んでいただけると安心できます。
僕の身分は自己紹介のとこからリンクをたどっていくとわかるようになっています。
大した者ではありませんが、怪しい者でもありません。
皆様のご参加をお待ちしております。
『ソフィーの世界』、関係ねぇwww
これも何かの縁だと思って、正義論とか心の哲学とかも読もうぜ
僕が先月下旬ごろノートに一生懸命翻訳を書いている間に、
「プログラミング言語の基礎概念」という本が、サイエンス社から出版されていたのですね！
しかも著者は、ラクダ（OCaml）本の五十嵐淳先生。ペンシルバニア大でPierce先生と机を並べていたこともあるという。
一瞬、「Software Foundations」の翻訳が出たのかと思ったのですが、会社の帰りに日本橋丸善に寄って探すと、別の本でした。
とはいえ、内容的にはチョコチョコ重なっているところもあり（OCamlですが）、日本語で書き下されているものなので非常に読みやすいし、わかりやすいです。
これはお勧め。1850円というのもびっくりリーゾナブルです。
ここ見ているような人は内容的に目新しくないのかもしれませんが・・・
お気遣い、とてもありがたいのですが、
Wikiの広告をクリックしていただいても僕には１円も入りません・・・・単にWikiサーバの運営費と運営会社の利益になるだけでだと思います。
もちろんクリックしても何の問題もないとは思いますが。
早とちりで失礼しました。
Basicsまでは、そこそこの完成度の翻訳になっているつもりですが、何かお気づきの点がありましたらWikiにお願いします。
僕自身もこれを翻訳した後、自分の日本語を読みながら一通り課題をやりましたが、
難易度が上がっていくペースがなかなかいい教材なのではないかと思います。
未来嬢の「プログラミングCoq」と併せてとりくんでもらえるといいかなと。
ユーザーに関数の中身を定義してもらう枠組みを考えてるんだけど、
ある種の制約を守れば正しく動作する関数が定義できますよ、としたいんだけど、
そのときの制約として、
・関数シグニチャに沿っていること
・こちらで定義した補助関数のうち、絶対に使っちゃいけないものがある
・関数の中はCoqに通り、上2つの制約に矛盾しなければ何でもOK
というようにするには、どうしたらいいんでしょうか。
最初のは多分Classとして与え、
ユーザーにInstance化してもらえばいいんだけど、
2個目の条件が満されていることはどうやって確認したらいいんですかね?
Extractionする段階で、定義済みの関数の式木を舐めて特定の名前の関数を使用しているかいないかで判定とかは可能だと思う
あれ、Software Foundationsの場所変わったの？
作業場所もwikiからGithubに変わったみたいだけど、運営者かわったの？
TOP カテ一覧 スレ一覧 2ch元 削除依頼 ▲
オブジェクト指向は本当に正しいのか？ (234)
◆◇◆dbMAGICってどうよ？◆◇◆ (793)
くだすれPython(超初心者用) その13 (126)
CVS導入スレ〜 Rev.3 (835)
【アンチ】関数型言語は使えない【玩具】 ２ (226)
おまいら最強のシストレFXプログラムをしてみろよ (391)
--log9.info------------------
ホログラム光ディスク「HVD」容量200GBで製品化 (226)
DVD、Blu-rayのリッピング違法化へ2 (241)
TDK製品は絶対に買うな！ (176)
ケンウッドドライブを使い込む (707)
パイオニア2層DVD-Rにこっそり期待するスレ (430)
CD-Rがコンポとかカーステで聞けないのは、なぜ？ (336)
B's Recorder 総合スレ Part.10 (288)
ビデオCDの作り方教えれ (336)
パナソニック四国エレクトロニクス総合スレ1 (816)
☆★☆フリーのライティングソフト Part4☆★☆ (864)
ライティングソフト不要☆WindowsXP (190)
やっぱ三洋電機のドライブだな (669)
プレク2410について語るスレ (393)
Cinavia報告スレ (234)
ナビゲーションのバックアップに関するスレ (916)
cprmgetkey対応ドライブ (552)
--log55.com------------------
【新潟/親子遭難】捜索開始から10日 依然行方わからず 五頭連峰★10
【宮城】国連事務総長特別代表が、津波被害の大川小を視察 石巻市
【余命vs弁護士】佐々木弁護士「懲戒請求してきた人の年齢、一番若くて43歳。40後半〜50代が厚く、60代、70代もおられる」★26
【はしか速報】感染経路が不明…愛知で24人目のはしか感染者 瀬戸市の会社員で発症後に豊田市の病院受診
【ムサコ】武蔵小杉駅の混雑、ＪＲに対策求め署名運動スタート 改札、ホーム、車内すし詰め「あばら折れちゃう！」神奈川県川崎市★３
【働き方改革】自民幹部、「高プロ」修正に言及 申請後元に戻れる仕組み
【話題】子供相手に激怒男が怒鳴る動画 札幌ドームで撮影しTwitterで拡散炎上★8
【自動車】「車体課税の軽減を」 業界団体の豊田会長が訴え 若者の車離れなど市場縮小に歯止め ★６
