Coqスレ

1 名前：デフォルトの名無しさん mailto:sage [2011/03/13(日) 21:05:23.37 ] こけこっこー coq.inria.fr/ 75 名前：デフォルトの名無しさん mailto:sage [2011/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 [2011/07/27(水) 16:23:12.05 ] >>75 よく見ると、前書きにその辺のことがチラッと書いてありましたね。跳ばして読んでました。 これによると、この文書を誰かが自分の講義に使うことは否定してませんね。 使う場合には連絡しろとも書いていない。 「ただ、そうするとどこかに直したいところや加筆したいところが出てくるだろうから、 そういうのがあったら連絡してね。subversionのレポジトリ教えてあげるから。」 てなことは書いてありますが。 この雰囲気だと、翻訳の公開を拒絶されそうな気配は無さそうですね、なんとなく。 77 名前：デフォルトの名無しさん mailto:sage [2011/07/27(水) 22:47:28.23 ] あーそれだめだわ。 断られるわ。 78 名前：デフォルトの名無しさん mailto:sage [2011/07/27(水) 23:09:04.95 ] >>75 coqdocだからPDFにはすぐ出来る。-pdf付けるだけ。 79 名前：60 [2011/07/29(金) 00:09:21.97 ] 昨夜、Pierce先生にメールをしたところ、長文のお返事をいただき、 日本語版の公開を快諾していただきました。 ただ、公開間近の最新版がもうすぐ出来上がる予定で、今のとだいぶ変わって いるので、それも考慮したほうがいいのではないのではとのことです。 ということなので、最新版とその差分が見られるよう、レポジトリの アカウントを作っていただくことになりそうです。 とりあえず最新版を見せてもらって、あんまり変わってないようなら 今手元にあるのをさっさと公開しようと思っています。 80 名前：デフォルトの名無しさん mailto:sage [2011/07/29(金) 00:37:49.56 ] やるじゃん 81 名前：60 [2011/07/31(日) 02:52:02.67 ] .vへのコピペに飽きてきたので暫定公開。 www.randmax.jp/sf/Basics_J.html フォーマットがややオリジナルと異なりますが、二つ理由があります。 　1. 僕がCSSを少しいじっているため。主に日本語対応。 　2. sfのチームはcoqdocをカスタマイズして使っており、それを入手していないため。 単に「お前の翻訳はヘタ」というような批判は勘弁してください。「手伝ってください」としか言いようがありませんので。 具体的な「ここはたぶん誤解してる。正しくはこう」とか「この単語は普通こう訳す」というようなお話は歓迎します。 ここでやるのが不適切なようでしたら、どこかほかのところに場所を借りてもいいかと思っています。 「オレにもやらせろ」はもちろん「オレにやらせろ」も歓迎です。僕にとって翻訳は趣味でも仕事でもないので、日本語の文書が最初からあるなら（誰かが作ってくれるなら）、僕もそれに乗っかりたいぐらいです。 Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・ 82 名前：デフォルトの名無しさん mailto:sage [2011/07/31(日) 03:28:17.28 ] >>81 翻訳Webページに、参加方法やリポジトリ閲覧方法や訳文投稿窓口を含めておくと、敷居が低くなるかもしれない。 たとえばwikiのようなものとか。 83 名前：デフォルトの名無しさん mailto:sage [2011/07/31(日) 07:59:42.65 ] >>81 > Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・ 最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。 84 名前：デフォルトの名無しさん mailto:sage [2011/07/31(日) 12:04:46.18 ] >>82の案を推す 俺もこのページは読んだことあるから多少は助力できるかも 85 名前：デフォルトの名無しさん mailto:sage [2011/07/31(日) 15:20:26.31 ] >>81 誤字をなおしたりとかならお手伝いできるから、>>82みたいにしてくれるとうれしい 86 名前：60 [2011/07/31(日) 22:15:43.81 ] みなさんいろいろありがとうございます。 Wikiについては、だいぶ更新がとまっているCoqWikiがなるものがあるので間借りすることも考えたのですが、 たいしたコストがかかるわけでもなさそうなので、どこか別に借りてみようかと思います。 準備ができたらそちらも追って公開します。 とりあえず明日には、Basicsの全体を暫定公開できると思います。 そうこうしているうちにSVNレポジトリのアカウントが届くのではないかと。 なんだか長い旅になりそうですが、ひとつ気長にお付き合いください。m(_ _)m >>83 >最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。 僕もそう思うんですけど、本当言うと学生さんに頑張ってほしいんですよね。 こういう日本で開拓の進んでない分野に切り込んで貢献する体験を若い人に沢山積んで欲しいと思うのです。 僕など成長したところで先が知れてますんで。 だからといって若い人に「お前がやれ」というのもかっこ悪い大人だと思うので、自分でやってしまったのですが。 どこかで誰かが「しまった！僕が先にやっておけばよかった！」と後悔してくれていればいいなと。 87 名前：60 [2011/08/01(月) 23:22:27.01 ] とりあえずWikiを借りてみました。 www16.atwiki.jp/sf_j/ 特に制限などつけていませんが、できればWikiに参加してログインを行って書き込んでいただけると安心できます。 僕の身分は自己紹介のとこからリンクをたどっていくとわかるようになっています。 大した者ではありませんが、怪しい者でもありません。 皆様のご参加をお待ちしております。 88 名前：デフォルトの名無しさん mailto:sage [2011/08/02(火) 21:26:40.40 ] >>87 『ソフィーの世界』、関係ねぇwww これも何かの縁だと思って、正義論とか心の哲学とかも読もうぜ 89 名前：60 [2011/08/02(火) 22:59:31.02 ] 今日いろいろ調べ物をしていて仰天しました。 僕が先月下旬ごろノートに一生懸命翻訳を書いている間に、 「プログラミング言語の基礎概念」という本が、サイエンス社から出版されていたのですね！ しかも著者は、ラクダ（OCaml）本の五十嵐淳先生。ペンシルバニア大でPierce先生と机を並べていたこともあるという。 一瞬、「Software Foundations」の翻訳が出たのかと思ったのですが、会社の帰りに日本橋丸善に寄って探すと、別の本でした。 とはいえ、内容的にはチョコチョコ重なっているところもあり（OCamlですが）、日本語で書き下されているものなので非常に読みやすいし、わかりやすいです。 これはお勧め。1850円というのもびっくりリーゾナブルです。 ここ見ているような人は内容的に目新しくないのかもしれませんが・・・ 90 名前：デフォルトの名無しさん mailto:sage [2011/08/03(水) 09:00:22.23 ] とりあえずwikiの下の方の広告をクリックしまくっておいた。 91 名前：デフォルトの名無しさん mailto:sage [2011/08/03(水) 13:36:59.98 ] なんだそのブログみたいな文体は 92 名前：60 [2011/08/04(木) 00:34:58.51 ] >>90 お気遣い、とてもありがたいのですが、 Wikiの広告をクリックしていただいても僕には１円も入りません・・・・単にWikiサーバの運営費と運営会社の利益になるだけでだと思います。 もちろんクリックしても何の問題もないとは思いますが。 93 名前：デフォルトの名無しさん mailto:sage [2011/08/04(木) 23:04:14.47 ] >>92 早とちりで失礼しました。 94 名前：60 [2011/08/15(月) 22:52:35.14 ] 本日、日本語版を一応リリースいたしました。Pierce先生にもその旨連絡しました。 Basicsまでは、そこそこの完成度の翻訳になっているつもりですが、何かお気づきの点がありましたらWikiにお願いします。 僕自身もこれを翻訳した後、自分の日本語を読みながら一通り課題をやりましたが、 難易度が上がっていくペースがなかなかいい教材なのではないかと思います。 未来嬢の「プログラミングCoq」と併せてとりくんでもらえるといいかなと。 95 名前：デフォルトの名無しさん mailto:sage [2011/09/05(月) 17:35:48.93 ] 型定義、関数シグニチャを提供して、 ユーザーに関数の中身を定義してもらう枠組みを考えてるんだけど、 ある種の制約を守れば正しく動作する関数が定義できますよ、としたいんだけど、 そのときの制約として、 ・関数シグニチャに沿っていること ・こちらで定義した補助関数のうち、絶対に使っちゃいけないものがある ・関数の中はCoqに通り、上2つの制約に矛盾しなければ何でもOK というようにするには、どうしたらいいんでしょうか。 最初のは多分Classとして与え、 ユーザーにInstance化してもらえばいいんだけど、 2個目の条件が満されていることはどうやって確認したらいいんですかね? 96 名前：デフォルトの名無しさん mailto:sage [2011/09/07(水) 17:55:08.74 ] 確かextraction機構はプラグインみたいな形でコア部分と別だったから Extractionする段階で、定義済みの関数の式木を舐めて特定の名前の関数を使用しているかいないかで判定とかは可能だと思う 97 名前：デフォルトの名無しさん [2011/10/03(月) 09:45:16.35 ] RT @mzp #sfja proofcafe.org/sf/ SoftwareFoundation和訳(4章まで) 98 名前：デフォルトの名無しさん mailto:sage [2011/10/03(月) 10:00:02.78 ] もしし 99 名前：デフォルトの名無しさん mailto:さげ [2011/10/14(金) 22:55:59.64 ] >> 60さん あれ、Software Foundationsの場所変わったの？ 作業場所もwikiからGithubに変わったみたいだけど、運営者かわったの？ 100 名前：デフォルトの名無しさん mailto:sage [2011/10/14(金) 23:09:28.89 ] wikiに説明が書いてあると思うが 101 名前：デフォルトの名無しさん mailto:sage [2011/10/14(金) 23:09:59.10 ] >>githubの方は60さんに刺激を受けたfm forumの人がやってるやつで完全に二つは独立してるよ 102 名前：デフォルトの名無しさん [2011/10/15(土) 22:24:07.91 ] >>101 なるほど。ありがとうございます。見た感じ今はgithubの方が勢いがあるのかな？ 103 名前：デフォルトの名無しさん mailto:sage [2011/10/16(日) 10:55:36.52 ] >>101 実際は、60が10月から忙しくなったのでProofSummit で協力をよびかけて、賛同者の作業がやりやすいようGithubに移行したということです。60もGithubに参加しています。 104 名前：デフォルトの名無しさん mailto:sage [2011/10/16(日) 10:58:10.00 ] それは知らなかった説明ありがとう 105 名前：デフォルトの名無しさん mailto:さげ [2011/10/16(日) 12:24:15.43 ] >>103 うん？どういうこと？ 二つは独立しているのではなく、作業場所が変更したってこと？ 最新の作業情報はgithubのプロジェクトをみればよい？ 106 名前：60 mailto:sage [2011/10/16(日) 12:36:30.91 ] >>105 そういうことです。 Github のほうが真(新)です。 Wiki のほうは、その事がちゃんと分かるように直しておきます。 107 名前：デフォルトの名無しさん [2011/10/16(日) 22:06:31.22 ] >>106 わかりました。ありがとうございます。 108 名前：デフォルトの名無しさん mailto:sage [2011/10/17(月) 09:21:46.34 ] @n_k28 魔理沙気持ち悪かったです。もう二度とやらないで下さい＾＾ 109 名前：デフォルトの名無しさん mailto:sage [2011/10/27(木) 22:46:35.48 ] (P -> Q) -> (~P \/ Q) これの証明ができん。 110 名前：デフォルトの名無しさん mailto:sage [2011/10/27(木) 22:54:20.25 ] ああ ~~((P -> Q) -> (~P \/ Q)) なら証明できるのか。 直観主義論理がどうとか俺にはちんぷんかんぷんだ…。 111 名前：デフォルトの名無しさん mailto:sage [2011/10/30(日) 10:33:11.77 ] tauto.でおｋ 112 名前：デフォルトの名無しさん mailto:sage [2011/11/11(金) 16:16:46.14 ] Inductiveな型TからT_rectが生成される原理がどうしてもわからないなあ。 誰か教えてちょーだいな。 113 名前：デフォルトの名無しさん mailto:sage [2011/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 mailto:sage [2011/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 名前：デフォルトの名無しさん mailto:sage [2011/11/12(土) 12:39:28.72 ] >>114 nat以外のものも構造的帰納法を表しているだけ。 X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても 型だけわかれば、使えるからそれで いいと思う。 このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが 知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。 116 名前：112 mailto:sage [2011/11/12(土) 16:10:50.99 ] >>115 ということは、構造的帰納法について、私が理解している以上に何か深いこと、 あるいは、もっと詳しいことがあるということでしょうか。論理式の定義に従って 帰納的に何かを証明するとか、そんなことは何の苦もなく理解してきましたけど、 上記>>114のsand_rectなんぞは、なぜそうなるのかいまひとつわからないのです。 また、sandの定義中のSetをPropにかえたものをpandとすると、pand_rectは sand_rectのSetをPropにかえただけのものとは異なります。ますますわかりません。 もし構造的帰納法について詳しく書かれた文献等あったらご紹介いただけないで しょうか。 117 名前：112 mailto:sage [2011/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 mailto:sage [2011/11/13(日) 09:55:45.41 ] 少しずつわかってくるにつれて、Coqとは直接関係ない気もしてきたのですが、 どなたか教えてくださるか、もしくは良い文献の紹介等していただけないで しょうか。 自然数の定義を例に話します。 （１）Oを自然数とする。 （２）nを自然数とするとき、S nも自然数とする。 （３）上記（１）（２）によって定められるもののみを自然数とする。 といった具合に自然数を定義することができますが、この（３）をどのように 形式的に表すかをもっと詳しく理解すれば、私の疑問が解けるような気がしてき ました。 どうか偉い方々、よろしくお願いいたします。 119 名前：デフォルトの名無しさん mailto:sage [2011/11/13(日) 15:44:37.16 ] Coq'Artの14章あたりにもある程度載ってるんだけども形式的な説明というわけでは無いね 論理や集合論の命題と型付きラムダ計算の式が1対1対応するっていう性質を使ってるってことは聞くけど 再帰型の定義が計算体系に及ぼす影響が対応する論理体系にどういう影響与えるかとか そういうのはよくわからない・・・ せいぜい構築子の無い型の値を仮定するのとFalseぶち込むのが対応してどちらも滅茶苦茶になるとか、そういうのぐらい ::=はiffに対応するとか|は排他論理和に対応するんだなぁというのは経験則でみえてくるけども 120 名前：デフォルトの名無しさん mailto:sage [2011/11/13(日) 19:01:45.89 ] ×型付きﾗﾑﾀﾞ計算の式 ○型付きﾗﾑﾀﾞ計算の型 121 名前：デフォルトの名無しさん mailto:sage [2011/11/19(土) 09:32:29.84 ] >>118 構造的帰納法に関しては俺はTAPLで勉強したな。あの本は丁寧で わかりやすい。 122 名前：112 mailto:sage [2011/11/21(月) 12:32:03.21 ] >>119-121 いろいろと情報提供ありがとうございます。いまはCoq'Artの14章で奮闘中です。もともと英語が苦手 なのですが、贅沢は言ってられません。TAPLって、Benjamin C. Pierceの「Types and Programming Languages」のことですよね。あたってみます。（砕けたりして。トホホ） 123 名前：デフォルトの名無しさん [2012/02/10(金) 07:07:56.25 ] proofcafe.org/sf/ に日本語訳を上げて下さっている方の書き込みがあったので、ここに書いておきます。 一部訳に打ち間違いがあります。どこに言ったら良いのかわからないので、ここに書いておきます。 proofcafe.org/sf/Poly_J.html の[マップ（Map）関数]のちょっと上に「理宇土」とあります多分「リスト」の誤変換だと思います。 この訳のお陰で大変楽して勉強できてます。ありがとうございます。 124 名前：デフォルトの名無しさん [2012/02/10(金) 09:10:05.55 ] proofcafe.org/sf/Poly_J.html の rememberタクティック のちょっと前に「なるべくintrosを使うタイミングを送らせ」の「送らせ」は「遅らせ」だと思います。 よろしくお願い致します。 訳ありがとうございます。 125 名前：デフォルトの名無しさん mailto:sage [2012/02/10(金) 09:35:05.24 ] 報告するならgithubのissue tracker https://github.com/sfja/sfja/issues か wikiの専用ページ www16.atwiki.jp/sf_j/pages/49.html でやるほうがいいと思うよ 126 名前：デフォルトの名無しさん [2012/02/10(金) 17:57:06.05 ] >125 ありがとうございます。そっちに書いときます。 127 名前：デフォルトの名無しさん mailto:sage [2012/02/11(土) 16:49:49.67 ] うわーはずかしいtypo。直しておきます。レポート感謝。 128 名前：デフォルトの名無しさん [2012/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 名前：デフォルトの名無しさん mailto:sage [2012/02/16(木) 13:24:10.57 ] Inductiveで列挙するのはコンストラクタの名前とその型。 値を並べられるわけではない。 130 名前：デフォルトの名無しさん mailto:sage [2012/02/16(木) 22:24:41.28 ] 1を名前に使えない Inductive my : Type := O : my | one : my . ならいい 131 名前：デフォルトの名無しさん mailto:sage [2012/02/18(土) 11:13:09.87 ] O(:nat)もコンストラクターなんじゃない？ 132 名前：デフォルトの名無しさん [2012/02/26(日) 23:56:37.37 ] なんか >>60 が変な扉を開いてしまったかもしれない。 「関数型ガール」 www16.atwiki.jp/sf_j/pages/56.html 133 名前：デフォルトの名無しさん [2012/03/09(金) 10:10:41.05 ] >129 >130 >131 >132 回答ありがとうございます。 134 名前：デフォルトの名無しさん [2012/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 名前：デフォルトの名無しさん mailto:sage [2012/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 名前：デフォルトの名無しさん mailto:sage [2012/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 名前：名無しさん [2012/03/15(木) 01:21:22.24 ] ネット務 138 名前：デフォルトの名無しさん [2012/03/20(火) 10:49:54.36 ] >>135 >>136 ありがとうございました。 またやってみます。 139 名前：デフォルトの名無しさん [2012/04/19(木) 09:20:01.83 ] Software Foumdationsの翻訳がとりあえず最後まで終わりました！ というわけでお願いなのですが、読んでください。 で、誤字脱字誤訳など指摘頂けると助かります。

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef