Coqスレ

1 ：11/03/13 〜 最終レス ：12/05/01

こけこっこー
http://coq.inria.fr/

2 ：

興味はあるが……

3 ：

Ｃｏｑ！Ｃｏｑ！Ｃｏｑ！Ｃｏｑぅぅうううわぁああああああああああああああああああああああん！！！
あぁああああ…ああ…あっあっー！あぁああああああ！！！ＣｏｑＣｏｑＣｏｑぅううぁわぁああああ！！！
あぁクンカクンカ！クンカクンカ！スーハースーハー！スーハースーハー！いい匂いだなぁ…くんくん
んはぁっ！ＰｒｏｏｆＧｅｎｅｒａｌたんの桃色ブロンドの髪をクンカクンカしたいお！クンカクンカ！あぁあ！！
間違えた！モフモフしたいお！モフモフ！モフモフ！髪髪モフモフ！カリカリモフモフ…きゅんきゅんきゅい！！
小説11巻のＣｏｑたんかわいかったよぅ！！あぁぁああ…あああ…あっあぁああああ！！ふぁぁあああんんっ！！
アニメ2期決まって良かったねＣｏｑたん！あぁあああああ！かわいい！Ｃｏｑたん！かわいい！あっああぁああ！
コミック2巻も発売されて嬉し…いやぁああああああ！！！にゃああああああああん！！ぎゃああああああああ！！
ぐあああああああああああ！！！コミックなんて現実じゃない！！！！あ…小説もアニメもよく考えたら…
Ｃ ｏ ｑ ち ゃ ん は 現実的 じ ゃ な い？にゃあああああああああああああん！！うぁああああああああああ！！
そんなぁああああああ！！いやぁぁぁあああああああああ！！はぁああああああん！！Ｒｏｃｑｕｅｎｃｏｕｒｔぅああああ！！
この！ちきしょー！やめてやる！！現実なんかやめ…て…え！？見…てる？ターミナルのＣｏｑちゃんが僕を見てる？
ターミナルのＣｏｑちゃんが僕を見てるぞ！Ｃｏｑちゃんが僕を見てるぞ！バッファのＣｏｑちゃんが僕を見てるぞ！！
アニメのＣｏｑちゃんが僕に話しかけてるぞ！！！よかった…世の中まだまだ捨てたモンじゃないんだねっ！
いやっほぉおおおおおおお！！！僕にはＣｏｑちゃんがいる！！やったよケティ！！ひとりでできるもん！！！
あ、コミックのＣｏｑちゃああああああああああああああん！！いやぁあああああああああああああああ！！！！
あっあんああっああんあアン様ぁあ！！セ、セイバー！！シャナぁああああああ！！！ヴィルヘルミナぁあああ！！
ううっうぅうう！！俺の想いよＣｏｑへ届け！！ＩＮＲＩＡのＣｏｑへ届け！

4 ：

このスレッドは天才pンジー「アイちゃん」が
言語訓練のために立てたものです。
アイと研究員とのやり取りに利用するスレッドなので、
関係者以外は書きこまないで下さい。
　　　　　　　　　　　　　　　　　　京都大学霊長類研究所

5 ：

Gaaaaaaaaaaaaaze at my biiiiiiiiiiiig coooooooq!

6 ：

これ日本にいるユーザ数ってどれくらいなの？

7 ：

まともなレスがつかないから、だれか紹介サイトとかテンプレとか作ったらどう?
興味をそそるような紹介文とか書かないと、ほとんどの人は食いついてこないよ。

8 ：

>>7
食いついたって仕方の無い言語

9 ：

そうでもないよ

10 ：

Coq は、INRIA にて開発されている対話的定理証明支援系です。 Calculus of Inductive Construction (CIC) を基礎とし、Tactics と呼ばれるコマンドを駆使することにより証明を行います。
http://www.eva-01.jp/wiki/pukiwiki.php?Coq

11 ：

証明のゴルフ場があったぞ。ダレとくwww
http://d.hatena.ne.jp/kikx/20100807

12 ：

女子高生によるほんわかCoqチュートリアルキター！！！！
むねあつ！!!
http://www.iij-ii.co.jp/lab/techdoc/coqt/

13 ：

＊ 「Coq！Coq！Coq！ どいつもこいつもCoq！
　　なぜだ！　なぜやつを認めて　このおれを認めねえんだ！」

14 ：

>>13
誰だお前？

15 ：

>>13
Isabelle乙

16 ：

>>15
実はAgdaじゃね？
こっちも依存型なのにCoqよりマイナーなのが悔しいとか。

17 ：

>>16
Agdaの機能やシンタックスはかなりCoqにも影響を与えているよね。
id: forall {A: Type}, A -> A の{}とか。
国産の定理証明器だからぜひともがんばってほしいものだが。

18 ：

>>17
確かに日本の人も貢献してるけど、北欧モノだよね？

19 ：

Goal False <> True.

20 ：

>>12
2章が公開されたね。
問5がわからない……

21 ：

問5は apply (H (or P (~P))). がヒントかな

22 ：

>>19
intro.

23 ：

>>19
intro H.
symmetry in H.
induction H.
auto.

24 ：

>>22
rewrite H.

25 ：

>>12
読み始めたけど、素人っぽさはすごくあるな
初っぱなの"Definition"のDが大文字でなければならないことに注意が無かったり、
"Eval compute in"はプルダウンボックスから選ぶにもかかわらず、「左側のテキストボックスに……と打ち、」とか書いてあったり。
plus'やid'のアポストロフィが何の説明もなく出てきたり。

26 ：

>>25
確かに説明はちょっと素人っぽいな。
しかし、少なくともCoqの知識はすごいな。高校生でCoqできるってなんか別の意味で人生楽しそうでいいな。
大人になったらなんの仕事をするんだろうか？

27 ：

さては料理人だな

28 ：

>>26
高校三年でCoqについて書けるのがすごいと思う。
フリーソフトの大部分は、高校レベルでは何するソフトかも想像できないのが普通だから。
将来は大学教授かテクニカルライターかな？
初学者の引っかかりやすい部分に注意を払えるようになって一人前なんだろうと思う。
大学で着実に勉強を重ねていって欲しいね。

29 ：

俺も高校の時から英語の文献読んでたよ。
Coqは日本語の資料もあるし、それほど厳しくないと思われ

30 ：

>>29
> Coqは日本語の資料もあるし、それほど厳しくないと思われ
どれのことですか？
教えてプリーズ。
自分は、高校数学の範囲は大人が思い出すよりかなり狭いと思うけどね。
述語論理、微分方程式の数値解法、品質管理に使う統計解析など、どれも高校数学には含まれない。

31 ：

Coqで証明たてるのって、結構大変なんじゃないの？そこそこの経験者らしいよ。
相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。

32 ：

英語よりも、数学の基礎知識が不足するんじゃないかと思うのだけど。
>>31
> 相対論から量子コンピューターまでの英論文は、高校時代読むだけなら自分もやってたけど、使いこなしたことはない。
高校時代に偏微分方程式とか状態ベクトルとか推移行列とかヒルベルト空間とか？
内部進学者する人なら、高校時代に割と好きなこと勉強できるのかな？

33 ：

与えられたものを必死で勉強する人間と、
自分で楽しい物を探して勉強する人間の違い。
優劣ではなく、ただの違い。

34 ：

let と let recが違うのはカテゴリカルな意味が違うからだったはず。
CAMLってCategorical Abstract Machine Languageの略だし。
ソースは無い。

35 ：

ML誤爆っすにゃ？

36 ：

>>34
letrecの双対があるってこと？ほんまかいな。

37 ：

双対？意味が違うから分けているんじゃないか、と言ってるだけだぞ。
スレチすまそ。

38 ：

圏論でいう圏も哲学で使われる範疇も
どっちも英語としてはcategoryなんだよなややこしい

39 ：

少なくともこのスレの文脈では全くややこしいことはなかった。

40 ：

>>12
弱った。
vンカンプンだ。
説明が簡潔に過ぎる、ウルマンのMLの教科書などと比べて。
スタンフォード大学の偏差値の高い学生に教えるときですら、
ウルマンくらいの易しさが必要なのになあ。

41 ：

自己紹介上手だね

42 ：

山本和彦氏の指導の元で書かれたという前提で、さらに偏見を漏らしてみる。
山本和彦氏は自分がEngineerだと思っているようだ。
Educatorの発想が少し足りないのかもしれない。
Engineerは動くブラックボックスを作っていれば、
説明がテキトーでもバカにされることはない。
逆に、Educatorは理解できる説明をしなければならない。
ブラックボックスを作るとバカと呼ばれる。

43 ：

アルバイトとかで、会社として管理職がいるだけじゃね？
本人は何やるかだけ承諾もらって、自由にやってるんだろう。
coqに興味あるなら、文章覚えるんじゃなくて、手を動かして覚えましょう。

44 ：

教科書ほしいっていうのなら、
勉強会で使ってるのあるみたいだよ。
Certified Programming with Dependent Types
http://adam.chlipala.net/cpdt/html/toc.html
http://adam.chlipala.net/cpdt/cpdt.pdf

45 ：

上階層貼ったほうがよかったね。ゴメン
http://adam.chlipala.net/cpdt/

46 ：

>>44-45
ありがとう
とても面白そうだね
MIT Pressから本としてももうすぐ出版されるみたいだね
最近、この手の分野の本の出版がほとんどなかったから楽しみ
ひところはGunterとかWinskelとかMitchellとかBruceとかどんどん出たのに
やっぱり本の形の方がディスプレイよりも目も疲れなくて読みやすいから
本が出たら買うことにしよう

47 ：

>>44
英語は苦手ですが、ありがとうございます。
いろいろな試行をやってみるところまで、何とかたどり着きたいです。

48 ：

こんなところでformal semanticsの専門家にでくわすとは
Gunterいいよね。

49 ：

>>48
うん、Gunterのはとても良い本だよね

50 ：

Gunterってなんぞ？CPDTと関係あるのか？

51 ：

Winskel の方が整理されてて良い、という人も多いが、
あれの良さがわからん。英語も変だし。

52 ：

にわかだからYvesPierr、mathewぐらいしかわからん

53 ：

>>52
> にわかだからYvesPierr、mathewぐらいしかわからん
さらにニワカなんで質問するんだけど、この２人ってどんな仕事してる人？
ググったけどわからない。

54 ：

yvesはCoq'Artの著者の一人
matthieuは最近Coqに追加された機能Type Class, User defined　equialities and relations, Program等の中心開発者

55 ：

>>54
ありがとうございました。
52に"YvesPierr、mathew"って書いてるから "Yves Pierre"が一人の名前だと思ってググったんだけど
でもYvesとPierreは別々の２人それぞれのファーストネームということなんですね。
それじゃググってもわからなくて当たり前でした。

56 ：

正直、この歳になって女子大生の夏休みを心待ちにすることになるとは思わんかった

57 ：

>>50
> Gunterってなんぞ？CPDTと関係あるのか？
49を書いて久しく見てなかったんですまない、質問が出てたんだね
Gunterというのは次の本のことです
Carl A. Gunter "Semantics of Programming Languages" (MIT Press, 1992)
この本はプログラミング言語に対する表示的意味論の本なんだが
それに必要な領域理論（domain theory: cpoとかの構成法やその圏論的な定式化とか）を市販の教科書の中では一番詳しく書いてある
（その方面専門の数学の専門書ならもっと詳しいのはいくらでもあるが計算機屋向けだとこれが一番詳しい）
共立の朱色のシリーズから出ていた横内さんの『プログラム意味論』（もう品切れ放置プレーされてるのかな、それともまだ出てるか？）は
ある意味ではGunter本の基本部分を纏めたようなもの
横内さんの本が好きな人ならばGunter本も読んでとても楽しめると思う
ちなみにCPDTとは直接には無関係
90年代前半は社会全体もバブルの時代だったがフォーマルセマンティックスの分野も次々に良い本が出版されて一種のバブルみたいだったなあ
最近、そういう本の出版が少なくなって（フォーマルセマンティックスの出版バブルの後、型理論関係の本の出版が少し多かった時期はあるが）寂しかったので
CPDTが出るのは本当に楽しみ

58 ：

>>57 トンクス
>>56 女子大生の夏休みワロタwww でも俺も楽しみwww

59 ：

おねえさんの説明でさっぱりわからなかった俺用メモ
ttp://sunak2.cs.shinshu-u.ac.jp/~miyao/UD/Subjects/Kouri/logic.htm

60 ：

とてつもなく基本的な質問ではないかと思うのですが、
Definition prop1 : forall (A : Prop), A \/ ~A.
のような、仮定のない証明はどのようにすればいいのでしょうか？
プログラミングCoqの練習問題には
問3. forall (P : Prop), ~(P /\ ~P)
という、→のない証明の回答例がありますが、これは
一番外のnotを展開することで→Falseが発生しているのでそれを
使っているようです。
なにぶんCoqどころか論理学自体初心者なものですみません。

61 ：

Require Import Classical.
Definition prop1 : forall (A : Prop), A \/ ~A.
apply classic.
Defined.

62 ：

こらｗ

63 ：

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 ：

>>63
回答ありがとうございます。
「Proof-editing mode であそぼう」レベルの今の自分にはとても立ち向かえない
課題だったということがわかりました．．．
しかし、~(P /\ ~P) は割とあっさりできるのに、A \/ ~Aはいろいろ大変なあたり、
独学で自分で課題を決めて取り組む、というのがやりにくいですね。どの程度大変な
ものに向き合ってるのか、まだ読めないです。
学校で勉強したい・・・

65 ：

流石に直感主義論理とNDの初歩ぐらい知っておかないとこの問題を自力で解くのは難しいかもしれない
とはいうものの簡単な数理論理学の教科書一冊読めばそれぐらいの力付くと思うけどね
独学なら
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も課題の答えが著者のサイトで見れるから独学には向いてると思う

66 ：

Coq'Art 中国語版あんのかよ。
専門書もサイトもソフトも、日本語訳って以前より減ってない?

67 ：

>>65
ありがとうございます。とりあえずSoftware Foundationsから読み始めてみます。
Coq'Artが届いたらそちらにシフトしてみます。
もしよろしかったら、直感主義論理とかNDにたどり着けるような日本語の本も
ご教授いただけますか？
ちなみに今読んでいるのは、野崎先生の「不完全性定理（ちくま学芸文庫）」です。
とまぁ、こんなレベルなのですが・・・
持ってるだけですが、「論理と計算のしくみ」とか「圏論による論理学」とか
「計算可能性とラムダ計算」は手元にあります。
が、「この辺の本を読む前に読んでおくべき本があるはずだぁ」というのが素直な
感想です．．．
>>66
悲しいですがこれが現実なんですかね・・・
これ以上差をつめられないように（開かないように？）、がんばらないと。

68 ：

>>67
その三冊なら論理と計算のしくみを読むのがいいかな
というかその本の演習問題に全く同じような証明問題があるから

69 ：

>>68
今見直してみると、「論理と計算のしくみ」っていい本ですねこれ。
買ったときはラムダ計算のところが読みたかったので後半しか見てなかったのですが、
前半に論理学の基礎がてんこ盛りに整理されてますね。
一緒に取り組んでみます。ありがとうございます。

70 ：

サイモン博士とニューウェル博士が最初の定理証明システムを手がけたときのことを想像してみる。
論文を読んだ人はプリンシピア・マセマティカを横に並べて読み進んだんじゃないだろうか？
小学校レベルでも高校レベルでもかまわないから、
数学の教科書と並行してCoqの基礎を学んでいけるテキストが欲しい。

71 ：

時間があったんで、
Software Foundations
http://www.cis.upenn.edu/~bcpierce/sf/toc.html
の「Basics」の章を全訳したんですけど、
公開するとまずいですよねぇ・・・・きっと。
巷にもう少し日本語の解説があれば普及も進むのでは
ないかと思うのですが。

72 ：

Copyright書いてないね。
型理論の人たちは結構フリーで膨大なページ数のテキスト公開してるから聞いてみれば?

73 ：

>> 公開するとまずいですよねぇ・・・・きっと。
原文のドキュメント作成者たちは無償で公開している。多くの方に読んでもらうためだ。
それを翻訳して公開するのに喜びこそすれ、嫌とは言わないだろう
もちろん、ドキュメント作成者の了解が前提になるが。
メールを出してみるべき。

74 ：

ペンシルバニア大学の先生ですよね。ビビる・・・
CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
Software Foundationsのほうは、これをどうしたいのか、なんで
公開しているのか、どこにも書いてないんですよね。
メール出してもし許可がもらえたら、もう一度見直してボチボチ
公開したいところです。
まぁ、「４０代オッサンの夏休み」になりますが。

75 ：

>>74
> CPDTは、「出版間近」って感じなんでさすがにまずそうですが、
> Software Foundationsのほうは、これをどうしたいのか、なんで
> 公開しているのか、どこにも書いてないんですよね。
自分が担当している講義の為の資料を受講生以外の一般にも公開しているという事です。
このSoftware Foundationsに沿った形での講義をPierceさんらはやってますから。
（PierceさんのHPのTeachingの最初の科目、CIS500とかいう番号が付いてるやつです）
CPDTは明らかに本として出版するのを大前提として書かれてますし、本として読める単一ファイルの形でなっていますが、
こちらのSoftware Foundationsは少なくとも今の時点では紙に印刷される（か電子出版される）従来の書籍の形態にはなっていませんね。
マニュアルなどで良くあるWebページとリンクの集合体として現在は組織化されてますから、
当面は普通の書籍としては出版する予定はないように見えます。
もちろん、Pierceさんらが（少なからずが出版を最終目標とする）旧来型のPSやPDFの単一ファイルにしたものを
実は作っているが公開していないという可能性はゼロではありませんが、その可能性は少ないと思います。

76 ：

>>75
よく見ると、前書きにその辺のことがチラッと書いてありましたね。跳ばして読んでました。
これによると、この文書を誰かが自分の講義に使うことは否定してませんね。
使う場合には連絡しろとも書いていない。
「ただ、そうするとどこかに直したいところや加筆したいところが出てくるだろうから、
そういうのがあったら連絡してね。subversionのレポジトリ教えてあげるから。」
てなことは書いてありますが。
この雰囲気だと、翻訳の公開を拒絶されそうな気配は無さそうですね、なんとなく。

77 ：

あーそれだめだわ。
断られるわ。

78 ：

>>75
coqdocだからPDFにはすぐ出来る。-pdf付けるだけ。

79 ：

昨夜、Pierce先生にメールをしたところ、長文のお返事をいただき、
日本語版の公開を快諾していただきました。
ただ、公開間近の最新版がもうすぐ出来上がる予定で、今のとだいぶ変わって
いるので、それも考慮したほうがいいのではないのではとのことです。
ということなので、最新版とその差分が見られるよう、レポジトリの
アカウントを作っていただくことになりそうです。
とりあえず最新版を見せてもらって、あんまり変わってないようなら
今手元にあるのをさっさと公開しようと思っています。

80 ：

やるじゃん

81 ：

.vへのコピペに飽きてきたので暫定公開。
http://www.randmax.jp/sf/Basics_J.html
フォーマットがややオリジナルと異なりますが、二つ理由があります。
　1. 僕がCSSを少しいじっているため。主に日本語対応。
　2. sfのチームはcoqdocをカスタマイズして使っており、それを入手していないため。
単に「お前の翻訳はヘタ」というような批判は勘弁してください。「手伝ってください」としか言いようがありませんので。
具体的な「ここはたぶん誤解してる。正しくはこう」とか「この単語は普通こう訳す」というようなお話は歓迎します。
ここでやるのが不適切なようでしたら、どこかほかのところに場所を借りてもいいかと思っています。
「オレにもやらせろ」はもちろん「オレにやらせろ」も歓迎です。僕にとって翻訳は趣味でも仕事でもないので、日本語の文書が最初からあるなら（誰かが作ってくれるなら）、僕もそれに乗っかりたいぐらいです。
Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・

82 ：

>>81
翻訳Webページに、参加方法やリポジトリ閲覧方法や訳文投稿窓口を含めておくと、敷居が低くなるかもしれない。
たとえばwikiのようなものとか。

83 ：

>>81
> Pierce先生宛てのメールを書いているときにちょっと手がすべって「これから1章／月ぐらいのペースで翻訳を続けていくつもり」などと書いてしまったので・・・誰か助けて・・・
最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。

84 ：

>>82の案を推す
俺もこのページは読んだことあるから多少は助力できるかも

85 ：

>>81
誤字をなおしたりとかならお手伝いできるから、>>82みたいにしてくれるとうれしい

86 ：

みなさんいろいろありがとうございます。
Wikiについては、だいぶ更新がとまっているCoqWikiがなるものがあるので間借りすることも考えたのですが、
たいしたコストがかかるわけでもなさそうなので、どこか別に借りてみようかと思います。
準備ができたらそちらも追って公開します。
とりあえず明日には、Basicsの全体を暫定公開できると思います。
そうこうしているうちにSVNレポジトリのアカウントが届くのではないかと。
なんだか長い旅になりそうですが、ひとつ気長にお付き合いください。m(_ _)m
>>83
>最初に見栄切ってそれをふうふう言いながらも達成することで人は成長するもんだ。頑張れ。
僕もそう思うんですけど、本当言うと学生さんに頑張ってほしいんですよね。
こういう日本で開拓の進んでない分野に切り込んで貢献する体験を若い人に沢山積んで欲しいと思うのです。
僕など成長したところで先が知れてますんで。
だからといって若い人に「お前がやれ」というのもかっこ悪い大人だと思うので、自分でやってしまったのですが。
どこかで誰かが「しまった！僕が先にやっておけばよかった！」と後悔してくれていればいいなと。

87 ：

とりあえずWikiを借りてみました。
http://www16.atwiki.jp/sf_j/
特に制限などつけていませんが、できればWikiに参加してログインを行って書き込んでいただけると安心できます。
僕の身分は自己紹介のとこからリンクをたどっていくとわかるようになっています。
大した者ではありませんが、怪しい者でもありません。
皆様のご参加をお待ちしております。

88 ：

>>87
『ソフィーの世界』、関係ねぇwww
これも何かの縁だと思って、正義論とか心の哲学とかも読もうぜ

89 ：

今日いろいろ調べ物をしていて仰天しました。
僕が先月下旬ごろノートに一生懸命翻訳を書いている間に、
「プログラミング言語の基礎概念」という本が、サイエンス社から出版されていたのですね！
しかも著者は、ラクダ（OCaml）本の五十嵐淳先生。ペンシルバニア大でPierce先生と机を並べていたこともあるという。
一瞬、「Software Foundations」の翻訳が出たのかと思ったのですが、会社の帰りに日本橋丸善に寄って探すと、別の本でした。
とはいえ、内容的にはチョコチョコ重なっているところもあり（OCamlですが）、日本語で書き下されているものなので非常に読みやすいし、わかりやすいです。
これはお勧め。1850円というのもびっくりリーゾナブルです。
ここ見ているような人は内容的に目新しくないのかもしれませんが・・・

90 ：

とりあえずwikiの下の方の広告をクリックしまくっておいた。

91 ：

なんだそのブログみたいな文体は

92 ：

>>90
お気遣い、とてもありがたいのですが、
Wikiの広告をクリックしていただいても僕には１円も入りません・・・・単にWikiサーバの運営費と運営会社の利益になるだけでだと思います。
もちろんクリックしても何の問題もないとは思いますが。

93 ：

>>92
早とちりで失礼しました。

94 ：

本日、日本語版を一応リリースいたしました。Pierce先生にもその旨連絡しました。
Basicsまでは、そこそこの完成度の翻訳になっているつもりですが、何かお気づきの点がありましたらWikiにお願いします。
僕自身もこれを翻訳した後、自分の日本語を読みながら一通り課題をやりましたが、
難易度が上がっていくペースがなかなかいい教材なのではないかと思います。
未来嬢の「プログラミングCoq」と併せてとりくんでもらえるといいかなと。

95 ：

型定義、関数シグニチャを提供して、
ユーザーに関数の中身を定義してもらう枠組みを考えてるんだけど、
ある種の制約を守れば正しく動作する関数が定義できますよ、としたいんだけど、
そのときの制約として、
・関数シグニチャに沿っていること
・こちらで定義した補助関数のうち、絶対に使っちゃいけないものがある
・関数の中はCoqに通り、上2つの制約に矛盾しなければ何でもOK
というようにするには、どうしたらいいんでしょうか。
最初のは多分Classとして与え、
ユーザーにInstance化してもらえばいいんだけど、
2個目の条件が満されていることはどうやって確認したらいいんですかね?

96 ：

確かextraction機構はプラグインみたいな形でコア部分と別だったから
Extractionする段階で、定義済みの関数の式木を舐めて特定の名前の関数を使用しているかいないかで判定とかは可能だと思う

97 ：

RT @mzp #sfja http://proofcafe.org/sf/ SoftwareFoundation和訳(4章まで)

98 ：

もしし

99 ：

>> 60さん
あれ、Software Foundationsの場所変わったの？
作業場所もwikiからGithubに変わったみたいだけど、運営者かわったの？

100read 1read

1read 100read

TOP カテ一覧 スレ一覧 2ch元 削除依頼 ▲

【GPGPU】くだすれCUDAスレ part5【NVIDIA】 (750)
Visual Studio 2010 Part19 (122)
Coqスレ (140)
Embarcadero RAD Studio/Delphi/C++Builder その2 (173)
スレ立てるまでもない質問はここで 119匹目 (156)
CVS導入スレ〜 Rev.3 (836)
--log9.info------------------
東京及び近郊のダンプ屋スレ (684)
大型特殊免許 ７ (420)
【全自動】洗車の仕方【手洗い】 (645)
■ターレットを改造にした〜い■ (181)
キャンターについて語ろうPART2【DUONICvsMTvsAT】 (514)
灯油を入れて節約しよう (340)
海上コンテナ運転手スレッド (469)
★岩手のデコトラ★ (604)
やんちゃ姫companyと愉快な仲間達親衛隊 (795)
【業界世界一】☆ミック☆【ギネス5000t】 (760)
丸と山下隼○と山田祐○ (241)
『全国』クレーン屋稼業【ラフター】☆☆☆ (640)
トレーラー・トラックコレクション　第13弾 (192)
トラック運転手はドキュンのホームラン王です�F】 (882)
大型二種免許を取ろう（教習所取得者向け）Part5 (349)
海上コンテナの運転手の集うスレ (321)
--log55.com------------------
Xiaomi POCO Part18
Lenovoスマホ総合スレ Part.7
Y !mobiIe AndroidOneX5 byLG Part 4
SHARP AQUOS R2 Part27
ASUS ZenFone 6 Part28
HUAWEI P30 Series #12
Motorola Moto Z/Z Play/Z2 Play/Z3 Play part18
docomo arrows 5G F-51A Part2