14/11/08 15:17:42.64 N89Y1+Fh.net
connect4を集合論プログラミングの例題として使いたいんなら、
まずはconnect4のルールを集合論的に定義するのが先だ。
今のところ1がやってるのは単なる手続き的実装例の移植じゃん。
それで参考になるわけがない。
697:デフォルトの名無しさん
14/11/08 15:33:25.11 oJ3Se8B2.net
>>695
「教科書」は「離散数学とかアルゴリズムのやつ>>523」か集合論のものに限定。
挙げられなければ、また1の後出しジャンケンってことで。
>>425 >>559 >>655-665
698:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/08 15:40:24.89 ebCh2W7f.net
記述は日本語なのか英語なのか数学記号によるのか？
699:１
14/11/08 19:44:24.22 vsjOn1b1.net
>>695
connect4が載ってる教科書は見たことないな。
>>696
>>697
connect4は新しい言語を勉強するときに都合がいいから使ってるだけであって、
集合論プログラミングとは関係ないんだけどな。
というか、集合論プログラミングの題材としてどんなものがいいかは
まだよくわかってないんだよな。
正規言語とオートマトン、文脈自由言語とプッシュダウンオートマトン
あたりかなぁとは思っているんだが。
>>698
数学記号じゃね？
700:デフォルトの名無しさん
14/11/08 19:53:04.25 LHO3gvAT.net
>>693
プログラミングパラダイムごとに得意な領域、不得意な領域が存在するのに、なんで例題一個だけで言語を判断しようとするの？短絡的すぎない？
全部Prologで書くのはきついものがあるけど、部分的にPrologを採用してるプロジェクトはあるよ
(とはいえPrologがconnect4を作るのに向いているかどうかで言えばたぶん向いてないとは思うけどね)
701:１
14/11/08 20:18:34.70 vsjOn1b1.net
>>700
ぐう正論ですな。
まあ、そんな簡単に新しい言語は深く習得できないからな。
感触掴むくらいがせいぜいじゃね？
判断が早いというのは言われてみればそうだと思う。
ちなみにPrologで生産性が上がる問題があるなら教えてくれ。
702:デフォルトの名無しさん
14/11/08 21:02:07.77 7W78geqS.net
>>699 >>701
>集合論プログラミングとは関係ない
ならPrologスレでやれよ。
Prologに詳しい人はそっちのほうが多いはずだ。
【論理】Prolog【初心者】
ｽﾚﾘﾝｸ(tech板)
703:１
14/11/08 21:21:57.05 vsjOn1b1.net
connect4は直接関係ないけどprologは関係あるかもしれないだろ。
つか、なんでこのスレでやっちゃダメなんだ。
意味わからん。
704:デフォルトの名無しさん
14/11/08 21:29:37.77 7W78geqS.net
>>703
>なんでこのスレでやっちゃダメなんだ。
スレ違いだから。
Prologの勉強をPrologスレでやってみて、「集合論に基づいた言語の作成」に関する話になったらここに来ればいい。
705:デフォルトの名無しさん
14/11/08 21:35:40.48 LHO3gvAT.net
>>701
まあ実を言うとPrologについてそんなに詳しくはないので、文法とWIkipedia程度の知識しかない
歴史的には定理自動証明の分野で使われてきていて、
最近ではIBMの例のワトソンのコアに使われてたりするとか、まあやっぱ知識処理なのだろうか
あとユニフィケーションと並列化の相性がよく、派生言語がいくつか出てるらしいね、Erlangとか
>>702のスレも業務への適用の話とかしててまだ途中だけど読んでて結構おもしろい
まあ言いたかったことは、他のパラダイムは切り捨てるより取り入れたほうが自分の糧になるよということで
以前関数型あたりも簡単に切り捨ててたから、それじゃもったいないよ
706:１
14/11/08 21:55:42.68 vsjOn1b1.net
>>704
You can't connect the dots looking forward. You can only connect them looking backwardsだよ！
>>705
>あとユニフィケーションと並列化の相性がよく、派生言語がいくつか出てるらしいね、Erlangとか
ErlangってPrologの派生だったの？
なんか並列化が得意らしいというのは聞いたことがあったが。
> >>702のスレも業務への適用の話とかしててまだ途中だけど読んでて結構おもしろい
そういやPrologスレちゃんと読んでないな。読んでみるか。
>まあ言いたかったことは、他のパラダイムは切り捨てるより取り入れたほうが自分の糧になるよということで
>以前関数型あたりも簡単に切り捨ててたから、それじゃもったいないよ
またまたぐう正論ですな。
気を付けます。
707:デフォルトの名無しさん
14/11/09 06:16:58.35 co8RBkg8.net
>>706
だーかーらー、そのconnect4とやらのルールを集合論的に書けばいいって言ってるだろ。
さっさとやれ。
708:デフォルトの名無しさん
14/11/09 16:46:55.86 9LyR+5oz.net
1は何かものを作れる人間じゃないから。
709:１
14/11/09 18:17:59.58 Yrjok8yA.net
>>707
んーどうだろうな。
俺もスレたてた時はすべてを集合で表せば数学的にうまくいくんじゃね？とか思ってたんだけど、
やっぱリストはリスト、タプルはタプルなんだよな。
connect4も無理に集合的に扱わないで手続型で扱った方が自然かもしれないんだよな～
ぶっちゃけ、集合にこだわる意味が根底から揺らいでるｗ
数学の基礎的な部分が集合論でできてるってのはそうなんだろうけど、
応用問題解くときに些末な問題に煩わされたくないよね？
まあ、集合論でうまくいきそうな問題⇔教科書の章末問題かなぁとか思ってたんだけどさ。
その辺はあんまり整理できてない。
710:デフォルトの名無しさん
14/11/09 19:17:53.75 co8RBkg8.net
リストもタプルも集合論の枠組み内で普通に扱えるのだが、
もういいや、1に何かを期待するのはやめた。
711:デフォルトの名無しさん
14/11/09 19:30:26.31 FyV/3PpB.net
そろそろループ再開ですか？
712:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/09 19:44:15.77 XU91kGr5.net
算術演算＋－×÷！／√
括弧（）［］
等号不等号＝≠＜＞≦≧≒≪≫
無限大∞
集合∈∋⊆⊇⊂⊃∪∩｛｜｝＃
論理：∧∨￢⇒⇔∀∃→∴∵
パーセント％
その他の記号±≡…；？
713:デフォルトの名無しさん
14/11/09 20:00:10.30 NPL58Du1.net
1に餌を与えないでください。
>>425>>559 >>655-665
714:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/09 20:28:33.70 XU91kGr5.net
俺の研究内容が似ているので燃料投下する。国の生活保護と同様に、たとえ悪魔にもエサを与えよう。
715:デフォルトの名無しさん
14/11/09 21:17:29.34 b4iNH/wh.net
1「悪魔の餌 クレクレ」
716:１
14/11/10 21:45:18.40 AsAdiTVl.net
試しにRubyでconnect4書いてみた。
URLﾘﾝｸ(www.age2.tv)
行数的にはhaskellのほうが短いくらいなんだが^^;
オフサイドルールのせいかな？
717:デフォルトの名無しさん
14/11/11 04:23:27.89 m7WVeZhS.net
>>716
スレ違いだバカ
718:デフォルトの名無しさん
14/11/11 16:25:56.08 kmmZIWoZ.net
スレタイでHaskellで良いじゃんと思ってスレ開いたら１が馬鹿すぎてスレをそっと閉じることにした
719:１
14/11/17 21:47:20.82 IjeD6lYX.net
とりあえず、次の宿題は圏論かな～？
720:１
14/11/17 23:26:02.06 IjeD6lYX.net
とりあえず、ここ読んだけど。。。
URLﾘﾝｸ(ja.wikibooks.org)
ぃみゎかんなぃ。。
もぅﾏﾁﾞ無理。。
ﾘｽｶしょ・・・
ようするにdoが使いたいだけ？
721:デフォルトの名無しさん
14/11/18 00:04:28.78 e4RrhwW3.net
>>720
Haskellスレでやれ。
Haskellに詳しい人はそっちのほうが多いはずだ。
関数型プログラミング言語Haskell Part26
ｽﾚﾘﾝｸ(tech板)
722:デフォルトの名無しさん
14/11/18 00:07:08.02 l6oqTr0E.net
1に餌を与えないでください。
>>425 >>559 >>655-665
723:１
14/11/18 21:56:19.27 +WEtmfNy.net
URLﾘﾝｸ(d.hatena.ne.jp)
ここも読んでみたけどやっぱわからん。
というか、読んでも目が滑る。
だれか圏論のいい入門textプリーズ
724:デフォルトの名無しさん
14/11/19 19:50:12.10 dm216OYo.net
とりあえず『圏論の基礎』でも読んでみたら？
725:１
14/11/19 19:56:54.80 V2tDw9NJ.net
URLﾘﾝｸ(www.amazon.co.jp)
これ？
まあ本屋いってみてあったら立ち読みしてみるわ。
726:１
14/11/26 20:02:22.17 JT4BoUXj.net
圏論の基礎買ったけど早くも積読ｗ
727:デフォルトの名無しさん
14/11/29 18:24:47.22 8AtyRUwF.net
>>701 の話だけど、ドコモで prolog が動いてる的な記事をなんかで読んだことがある
728:１
14/11/30 19:47:48.77 O0/vTNqA.net
URLﾘﾝｸ(iiyu.asablo.jp)
これか。
コード量１０分の一は確かにすごい。
しかし2370万行とか正気の沙汰じゃないな。
729:デフォルトの名無しさん
14/11/30 22:28:37.23 mFsly3WX.net
Prolog で書くと「コード量１０分の一」となる例には、他にも型推論があるね
以下のblog記事では、単純な型推論をPrologで記述している
・Prolog で型チェック：Rainy Day Codings：So-net blog
URLﾘﾝｸ(rainyday.blog.so-net.ne.jp)
自分の知る範囲では、世界で最も簡潔な型推論の実装コードだね
これも、もし(型システムという)形式的なルールが定義されていれば、
それを直接的に表現できるという Prolog の特徴が活かされている
Haskell でもこんな芸当はできない
730:デフォルトの名無しさん
14/12/01 15:16:30.87 pglWaPo9.net
おおっと、Haskell信者に対して挑発だ～！
731:デフォルトの名無しさん
14/12/01 15:51:58.42 oEpuqve5.net
別にユニフィケーションがどっち方向にも働く、というのはPrologの特性だし、
Haskellにそんなものあっても困るだけだし。
732:１
14/12/01 19:25:13.06 TTRJBgwa.net
>>729
ふーむ。Rubyだとどうなるかな～。
ヨクワカラヌ。
733:デフォルトの名無しさん
14/12/01 20:27:28.82 pmQ3LQ8v.net
Prologのシンボル使ったユニフィケーションを実装するのは
Rubyに限らず手続き型言語ではライブラリ頼りでやらんと面倒い
むしろそれに特化され過ぎて、手続き的な書き方が面倒いって言語がProlog
734:デフォルトの名無しさん
14/12/01 22:36:56.45 oEpuqve5.net
そういったものをなんでもまぜこぜできるからLispは偉い、というのが
竹内先生@NUEの主張だったなw
735:デフォルトの名無しさん
14/12/01 23:52:04.88 6Gpd+bqZ.net
1に餌を与えないでください。
>>425>>559 >>655-665
1は推論や数式処理を扱うのは面倒くさいと思っている。
>>574-576
736:デフォルトの名無しさん
14/12/02 00:14:21.85 +stn5l+y.net
集合論だと逐次処理やりにくいしな
SQLとも違うみたいだし
737:デフォルトの名無しさん
14/12/03 15:47:19.25 C/BNzxz3.net
集合論だと、逐次処理は処理系の中でやる。
プログラムにはmapやらfilterやらが出てきて、逐次処理は隠蔽されるのでは？
それを考えると、１がlispで満足できないのが不思議でならない。
まぁ、文字通り「何も」考えていないのだろうな。
738:１
14/12/03 19:55:52.44 oIRBJSMm.net
lispってそんないいかなぁ。
ちょっとやったことあるけど、インデントつけても括弧の対応がすぐわかんなくなるんだが。
コード読みにくいったらありゃしない。
739:デフォルトの名無しさん
14/12/03 20:36:17.67 HSbdY3zj.net
>>738
ちょっとやってみただけで慣れようともせずケチつける。
>>700>>701>>705>>706
740:デフォルトの名無しさん
14/12/03 21:18:09.35 DVPNx2yH.net
>>734
S式を使っているからうまく混ぜられる、S式こそLisp最大の特長、とかいう主張だったな。
741:１
14/12/03 22:35:36.35 oIRBJSMm.net
>>740
詳しく
742:デフォルトの名無しさん
14/12/03 23:15:45.16 cePlsLqN.net
ほげ言語のパラドックスでも読んどけ
743:デフォルトの名無しさん
14/12/04 01:08:18.94 jHjIGczB.net
集合に順序があるのはむしろベクトルかタプルに見える
集合論って考えは好きだけどソートみたいな逐次処理でよく使うものはどうなるんだろうか
並列処理的なこと考えてるひとがいるみたいなんでそれに乗っかると
並列処理ならクイックソートよりマージソートのほうが速そうだがそれが集合論かと言われるとちょっと困る
でもソートが本来のやりたいことではなくてソートしたデータにまた何らかの処理をする要求のほうが多い気がするんでどうでもいいか
2分探索なり逐次処理の環境で考えだされたアルゴリズムはほとんど使えない気がするんでまた誰かが良さそうな手順を考えださないとな
744:デフォルトの名無しさん
14/12/05 09:26:36.60 I64sWIzc.net
数学できる人間に見られたいクズが集まるスレ
745:デフォルトの名無しさん
14/12/05 11:54:06.72 IjAdRY0C.net
自己紹介か？
746:１
14/12/05 20:20:24.20 b89FafAC.net
とりあえず、圏論からは戦術的転進するか。
別のネタを探そう。
747:デフォルトの名無しさん
14/12/05 20:55:48.99 B18WNnFt.net
1に餌を与えないでください。
>>425>>559 >>655-665
748:デフォルトの名無しさん
14/12/05 23:22:33.28 oLmzY7WJ.net
しかしまあスレタイ通りにはなかなかいってないけど総合的には良スレっぽい
749:デフォルトの名無しさん
14/12/06 01:07:31.28 tjNXDvF3.net
>>746
圏論を勉強する気など最初からなくて、ネタのつもりだったわけだ。
圏論以外に何をもってきても同じだろうな。
750:デフォルトの名無しさん
14/12/06 10:37:54.51 kt8GWotW.net
lisp の括弧は rainbow-parentheses 的なの入れるとマシになる
751:デフォルトの名無しさん
14/12/06 18:03:11.24 KgmhP8S/.net
lispで区切りに()だけ使うんじゃなくて集合を表す時は{}使うとかどうなの？
集合は{
752:１
14/12/06 18:04:03.49 KgmhP8S/.net
途中で書き込んじゃった。
集合は{}で表すってイメージあるんだけど。
753:デフォルトの名無しさん
14/12/06 18:56:15.26 dXBvUp0m.net
clojureは#{}が集合のリテラルとしてある
他のlispでもリードマクロかけばそういうことはできる
是非についてなら。その表記が存在することが対象のプログラミングに有効ならあり、そうでなきゃなし
754:１
14/12/06 18:59:55.68 KgmhP8S/.net
ほほう。
clojure検討してみる価値あり？
755:デフォルトの名無しさん
14/12/06 19:20:33.09 dXBvUp0m.net
まあlisp系はマクロ書けば簡単に構文拡張できるから、新しい言語を試行錯誤したいなら最適ではあるよ
756:デフォルトの名無しさん
14/12/06 19:20:42.39 5oGFUyw+.net
RubyとかJavaにもSetオブジェクトはあるし、リテラルの有無はソースコードの見た目の問題で、
たいして重要じゃない。
757:デフォルトの名無しさん
14/12/06 19:28:14.31 dXBvUp0m.net
マッチョすぎﾜﾛﾀ
数値や文字列リテラルのない言語でも頑張ってくれそう
758:１
14/12/06 19:49:14.64 KgmhP8S/.net
リテラルの有無は結構気になるな、俺は。
Rubyの配列やマップのリテラルは気に入ってる。
759:１
14/12/06 19:51:57.69 KgmhP8S/.net
clojureってjavaなのか。
クラスパスとかあんまわかってないんだよな～じつは
760:デフォルトの名無しさん
14/12/06 20:40:46.96 VB5mtD/4.net
>>748
VIPやシベリアだったらな。
761:１
14/12/06 21:05:36.24 KgmhP8S/.net
パッと見common lispよりclojureのほうがオサレにみえる。
あんまりcommon lisp知らんけど。
762:デフォルトの名無しさん
14/12/06 21:16:11.69 5oGFUyw+.net
なんでもいいから手を動かせ
763:１
14/12/07 00:04:16.45 2ooQYugx.net
OO言語だとobj.method(x)って書くけどlisp系だと(method obj x)って書くじゃん？
OO言語になれてるからかこの順番の違いが結構イラつく。
764:デフォルトの名無しさん
14/12/07 00:11:32.48 t9ahLiCr.net
ほんとこの１は駄目だなw
765:デフォルトの名無しさん
14/12/07 01:41:10.92 bfkTF4nN.net
lispでC風メソッド呼び出し構文開発したってのをどっかのブログでみたな
766:デフォルトの名無しさん
14/12/07 02:32:50.17 lyVqLM7u.net
リテラルでいろいろ指定できるのは便利だけどな
Clojureだと
{key1 obj1 , key2 obj2}でmap
#{obj1 obj2 obj3} でset
[obj1 obj2 obj3] でvector
'(obj1 obj2 obj3) でlist
地味にsetがありがたかったり(他の言語だとsetのリテラル滅多に無い)
767:デフォルトの名無しさん
14/12/07 12:08:48.39 mrRmmrII.net
>>726
圏論の和書として定評があり再版が望まれているのは
URLﾘﾝｸ(www.amazon.co.jp)
amazon 価格がすべてを物語っている
768:１
14/12/07 17:19:43.84 2ooQYugx.net
いつものようにclojureでconnect4書こうと思ったが、
>>763のことを差し引いても想像以上にモチベーション上がんない。
何のせいだ？
パッと見clojure良さそうに見えるのに。
Prologのときも苦戦したがモチベーションは保てた。
769:デフォルトの名無しさん
14/12/07 18:06:31.44 NlsKlGNA.net
>>768
このスレでは集合論に基づいた言語と関係ない話題はルール違反です。
770:デフォルトの名無しさん
14/12/07 19:50:11.74 npVck0tg.net
>>768
今度は「なぜか分からないけどモチベーションを保てない」かw
>>425>>559>>655-665
771:デフォルトの名無しさん
14/12/08 04:17:29.43 jYPMOE5Q.net
>>768
モチベーションを保てないってことだから続かないと思うけど
続けるならClojureスレに行け
【Lisp】プログラミング言語 Clojure #3【JVM】
ｽﾚﾘﾝｸ(tech板)
772:１
14/12/09 23:17:28.28 PZp4J+Rx.net
リアルが忙しくなりそうです。
しばらくこれなくなるかもだが、俺が留守の間おまえらでこのスレを盛り上げてくれよな。
よろしく。
773:デフォルトの名無しさん
14/12/10 21:31:22.32 7P/sQ89x.net
削除依頼していけよ
774:１
14/12/26 19:46:13.23 pkBFPf36.net
仕事納めだよ。
しかし見事にレスがついてないな。
お前らで盛り上げてくれていいのに。
775:片山博文MZ ◆T6xkBnTXz7B0
15/01/03 12:40:55.68 XgnEofgF.net
>>1さんよ、
Coqという言語を使えば、集合論を含む数学の証明や、プログラムの性質や品質保証ができるらしいぞ。
やってみないか？
776:デフォルトの名無しさん
15/01/03 14:07:47.18 MdLSAVWL.net
>>775
>>713-714
777:1
15/01/03 18:31:19.39 y8FDuePZ.net
とりあえず片山さんがCoqで一番成功してると思った例題を教えて
それで判断するわ。
778:片山博文MZ ◆T6xkBnTXz7B0
15/01/03 19:06:58.41 XgnEofgF.net
俺もCoqについては初心者だが、数学、グラフ理論の超難しい問題
「四色問題」の証明がCoqでできたらしい。
779:1
15/01/03 20:02:04.73 y8FDuePZ.net
手続き型言語とかに比べて完結に実装できるってこと？面白そうではある
780:１
15/01/03 20:38:21.69 rEeqS3sH.net
ID違うと思うけど１です。
簡潔に実装できるんじゃなくて、
実装はHaskellとかでやって、その正しさをCoqで保証するの？
よくわからん。
781:１
15/01/03 21:16:03.70 rEeqS3sH.net
Coq単体で動くのか。
prologに近いのか？
ぶっちゃけかなりむずいなこれは。
782:１
15/01/03 22:17:48.00 rEeqS3sH.net
わからんということがわかった。
底なし沼みたいな感じやなこれ。
783:デフォルトの名無しさん
15/01/03 23:44:50.02 Y5c4kVu7.net
今回のクレクレ・ループは終わりかな。
>>425>>559>>655-665
784:1
15/01/04 13:03:03.07 1dxkxQcz.net
片山さんはCoqどれくらい書けるの？
例えばド、モルガンの証明とか書けるの？
785:片山博文MZ ◆T6xkBnTXz7B0
15/01/04 21:15:57.30 izkph8nP.net
>>784
TutorialのPDFをコンビニで2in1pageで両面印刷して研究し始めたとこ。
数学と論理学と英語とプログラミングの知識が要求される地獄山だな。
786:１
15/01/04 21:40:34.76 7jAGFdTv.net
>>785
そのチュートリアルのURLくだしあ。
787:片山博文MZ ◆T6xkBnTXz7B0
15/01/04 21:45:09.09 izkph8nP.net
>>786
「Coq tutorial PDF」で検索
788:デフォルトの名無しさん
15/01/04 21:59:00.42 7jAGFdTv.net
URLﾘﾝｸ(coq.inria.fr)
これ？
結構分量ありますね。
789:１
15/01/06 00:03:50.53 iQ4UNt/k.net
Coqで任意の自然数nに対してn*(n+1)が偶数であることを証明しようとしたがどうしてもできない。
だれかHELP.
790:１
15/01/06 00:34:25.70 iQ4UNt/k.net
定義はこれで。
Theorem t:
forall (n:nat),exists m , (n*(n+1) = 2 * m).
791:デフォルトの名無しさん
15/01/06 05:55:25.49 Gduz5N96.net
偶数+1は奇数
奇数+1は偶数
遇数*奇数も奇数*遇数も遇数
自然数は奇数か偶数かどちらかである
792:１
15/01/06 21:04:14.92 iQ4UNt/k.net
「nが奇数ならn+1は偶数」を証明しようとして詰まってる。
Require Import Even.
Lemma l:
forall (n : nat), odd n -> even (n+1).
intros.
induction n.
simpl.
apply even_S.
これでodd 0とかいうのが出てくるけど、ここからどうしていいかわからない。
793:１
15/01/06 21:10:59.52 iQ4UNt/k.net
「自然数nに対してn*(n+1)が偶数である」
本題のこっちはここまで進んだ。
Require Import Even.
Theorem t:
forall (n:nat), even (n*(n+1)).
intros.
apply even_mult_aux.
794:１
15/01/06 23:17:17.43 iQ4UNt/k.net
Coq難しすぎんよ～
もう寝る。
795:１
15/01/07 19:22:04.95 DdlkDaa+.net
URLﾘﾝｸ(www.iij-ii.co.jp)
このページによるとforall (P : Prop), P \/ ~ Pは証明できなんだそうだ。
forall (n:nat), even (n*(n+1)).も証明できないのかもしれないな。
796:デフォルトの名無しさん
15/01/07 20:14:30.38 zH4wOwdk.net
1に餌を与えないでください。
>>425>>559>>655-665
797:1
15/01/07 21:02:58.84 DdlkDaa+.net
odd 0 -> Falseは証明できたっぽい。
これをどう活用すればいいのかわからない。
Lemma l2:
odd 0 -> False.
apply not_even_and_odd.
apply even_O.
798:デフォルトの名無しさん
15/01/08 15:50:20.90 FouB2F9v.net
S
799:デフォルトの名無しさん
15/01/08 18:29:26.11 qFLJfmjp.net
O
800:デフォルトの名無しさん
15/01/08 19:09:01.13 XNa5H7Wz.net
S
801:１
15/01/08 20:07:08.21 9tH8cNHX.net
ハルヒか？
802:１
15/01/08 22:27:11.24 9tH8cNHX.net
そもそもodd n -> even (S n)って定義そのものなんだよなぁ。
803:1
15/01/11 19:52:52.15 zln55Xsd.net
ギブアップ。
だれか正解しってたら教えて。
804:1
15/01/13 18:35:43.03 7YFvdf+i.net
片山さん答え知ってたら教えて
805:デフォルトの名無しさん
15/01/13 20:23:10.10 ElusS0xD.net
ｽﾚﾘﾝｸ(tech板:23番)
> 23 名前：片山博文MZ ◆T6xkBnTXz7B0 [sage]： 2015/01/13(火) 18:53:35.00 ID:gURRjQHf
> 私はお下品
806:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 21:52:38.35 gURRjQHf.net
ヒント。
Require Import Even.
Lemma eSr: forall n:nat, even (1 + n) -> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
807:１
15/01/13 22:46:33.61 ld5ZWEPI.net
Lemma l : forall (n:nat), even (1+n)-> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
apply odd_S.
apply even_O.
Qed.
こう？
nを偶数と奇数に場合分けする方法がわからんとです。
808:１
15/01/13 23:04:11.48 ld5ZWEPI.net
even(1+n)にeven(1+n) -> odd nをapplyして odd nにならんのか？
よくわからん。
809:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 23:09:34.67 gURRjQHf.net
Lemma oS: forall n:nat, even n -> odd (S n).
intros.
apply odd_S.
apply H.
Qed.
810:１
15/01/13 23:38:41.86 ld5ZWEPI.net
証明済みのLemmaの活用の仕方がわからんです。
applyじゃないの？
811:片山博文MZ ◆T6xkBnTXz7B0
15/01/13 23:39:26.18 gURRjQHf.net
replace (even (S n)) with (odd n).
apply even_or_odd.
もう少しだな。
812:1
15/01/14 00:05:14.20 upPMt0VH.net
A=Bを示したかったらA->BかつB->Aで方針あってますか?
813:１
15/01/14 00:09:20.78 upPMt0VH.net
もう寝ます。
また明日よろしくお願いします。
814:片山博文MZ ◆T6xkBnTXz7B0
15/01/14 19:03:17.31 lWtQJ7uI.net
聞きたいことがあれば、俺の掲示板に来いよ。待ってるぜ。
815:片山博文MZ ◆T6xkBnTXz7B0
15/01/15 14:58:59.94 OiYOltU9.net
URLﾘﾝｸ(katahiromz.bbs.fc2.com)
816:デフォルトの名無しさん
15/01/15 18:04:49.36 UYCK2hGt.net
>>814-815
1がそっちに行ってくれればいいけど。
1はCoqとか本当はどうでもよくて、このスレに書くこと自体が目的になってるだろうから・・・
817:デフォルトの名無しさん
15/01/15 20:46:59.13 QgJ4DA/V.net
>>816
雑談はこちらの412に書いてるな。
戻ってくるなよ ＞1
818:１
15/01/15 21:04:35.89 RCkerH2f.net
お前らこのスレが伸びちゃ困る理由でもあるのかｗ
819:デフォルトの名無しさん
15/01/15 22:49:41.86 5ppshwSd.net
>>818
1が「集合論に基づいた言語を作る」話をしないからな。
>>425>>559>>655-665
どうせエサをくれるのは片山博文MZだけなんだから、ずっとあっちに行ってろよ。
820:1
15/01/15 23:03:37.94 RCkerH2f.net
このスレはお前らで盛り上げてくれてもかまわないんだぜ？
821:デフォルトの名無しさん
15/01/16 00:08:32.30 q80wbXpz.net
このスレ見てるの結構楽しい（煽りとかではなくいろんな話が出てくるし）から盛り上がって欲しい
822:１
15/01/16 00:10:36.55 tbQRRWp6.net
できたっぽい。
片山さんに教えてもらったページみた。
Require Import Even.
Theorem t:forall n:nat,even (n * (1+n)).
intros.
apply even_mult_aux.
elim n.
left.
apply even_O.
intros.
elim H.
right.
apply even_S.
apply odd_S.
apply H0.
left.
apply H0.
Qed.
Coq相当親切なチュートリアルがないと勉強できんわ。
どのタクティク使えばいいのかとかわからんすぎる。
823:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 01:05:01.69 IPI8U3lP.net
>>822
なかなかやるじゃん。
ついでに「片山QZの定理」の証明でもやってみる？
片山QZの定理
URLﾘﾝｸ(katahiromz.web.fc2.com)
824:１
15/01/16 18:38:49.28 tbQRRWp6.net
MZとかQZとかって何なの？
別にいいんだけど。
片山QZの定理はなんかえらい難しそうなのでやめとく。
825:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 18:52:49.05 IPI8U3lP.net
QZというのはC/C++宿題スレに生息している人だよ。
そうだな。2n＝n＋nの証明なんかどうかな？ 楽勝？
826:１
15/01/16 19:09:16.59 tbQRRWp6.net
掛け算の定義がどこにあるのかわからん。
証明もいいけどコードの自動生成のほうが面白そうかな～
827:片山博文MZ ◆T6xkBnTXz7B0
15/01/16 22:32:01.39 IPI8U3lP.net
>>826
英語では、掛け算がmultiplicationで、自然数がnatural numbersだろ？
それを略すればmul,natになるだろ？
SearchAbout mul.
SearchAbout nat.
で検索できるから。
828:１
15/01/16 23:47:30.80 tbQRRWp6.net
>>827
結構むずかしい。
仮にできたとしても時間かかると思う。
829:１
15/01/17 00:13:16.15 e9PIZEl5.net
ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。
早めに身を引いた方がよさそうかな～とも思う。
830:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 01:27:28.08 PPUSm5YO.net
数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。
では、そなたはどのような言語が希望か申し上げてみよ。
831:１
15/01/17 02:12:55.60 e9PIZEl5.net
いや～確かにCoq面白いんだけど。
勉強するのに時間かかり過ぎるっていうか
もうちょっと市民権を得て入門書とか充実してからの方がいいかな～と。
証明も紙なら簡単にできることが結構難しかったりで、
実利を得るところまで勉強進めるのがしんどい。
実用までいかなくてただのパズルで終わりそう。
Coq参考になるところは多いと思うんだけどね。
どこまで時間費やすか見極めたほうがよさげ。
片山さんはCoqにどの程度手ごたえ感じてるの？
832:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 02:59:53.32 PPUSm5YO.net
麿は、この素晴らしきCoqを使えば、不具合のないソフトウェアが作れると見ては、
これをマスターすれば世界征服も夢ではないと、そのような所存でおじゃるよ。
833:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 03:31:41.14 PPUSm5YO.net
Coqと人工知能を組み合わせたら……、金融取引に活かせば……とか楽しい妄想が広がるでおじゃる。
834:１
15/01/18 22:30:12.77 Pnbu8M/I.net
人工知能といえばdeep learningとかいうのが流行らしいんだが。
835:１
15/01/20 23:02:01.33 RE29itzd.net
2n=n+nはomegaで一発っぽい。
omegaなしだとどうやるかわからん。
836:デフォルトの名無しさん
15/01/21 01:37:31.40 +/NZ76QF.net
1に餌を与えないでください。
>>425>>559>>655-665
837:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 08:55:01.51 y20qOxOP.net
n＝1×nを使う
838:1
15/01/21 19:32:48.10 83hEDbKu.net
途中よけいなことしてるかもだができたっぽい。
Require Import Arith.
Theorem t:forall n:nat,2*n=n+n.
intros.
replace (2*n) with (n*(S 1)).
symmetry.
replace (n+n) with (n*1+n).
apply mult_n_Sm.
replace (n*1) with (1*n).
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
apply mult_comm.
apply mult_comm.
Qed.
839:１
15/01/21 19:37:49.38 83hEDbKu.net
Coqは一日一時間までにする。
それ以上は自重。
840:１
15/01/21 20:33:19.47 83hEDbKu.net
片山さんの模範解答うｐ希望
841:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 22:08:31.55 OPHJ2hAi.net
>>840
Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.
842:１
15/01/21 22:49:05.70 83hEDbKu.net
ふーむ。確かに片山さんのほうが自然な証明ですな。
843:片山博文MZ ◆T6xkBnTXz7B0
15/01/23 02:17:55.54 22/uje4h.net
布教のために数学板でも展開するぞ。
【Coq】コンピューターで証明しよう【コック】･2ch.net
ｽﾚﾘﾝｸ(math板)
844:デフォルトの名無しさん
15/10/21 21:08:46.20 qGjQS7QU.net
URLﾘﾝｸ(connect4.game-solver.org)
845:デフォルトの名無しさん
15/10/21 21:49:58.99 kanshW5q.net
ほう、4並べのソルバですか。面白い
なぜこのスレなのかは気にしないでおこう
thx
846:デフォルトの名無しさん
16/05/01 11:01:21.14 tKi6j9CT.net
匿名通信（Tor、i2p等）ができるファイル共有ソフトBitComet（ビットコメット）みたいな、
BitTorrentがオープンソースで開発されています
言語は何でも大丈夫だそうなので、P2P書きたい！って人居ませんか？
Covenantの作者（Lyrise）がそういう人と話したいそうなので、よろしければツイートお願いします
URLﾘﾝｸ(twitter.com)
ちなみにオイラはCovenantの完成が待ち遠しいプログラミングできないアスペルガーｗ
The Covenant Project
概要
Covenantは、純粋P2Pのファイル共有ソフトです
目的
インターネットにおける権力による抑圧を排除することが最終的な目標です。 そのためにCovenantでは、中央に依存しない、高効率で検索能力の高いファイル共有の機能をユーザーに提供します
特徴
Covenant = Bittorrent + Abstract Network + DHT + (Search = WoT + PoW)
接続は抽象化されているので、I2P, Tor, TCP, Proxy, その他を利用可能です
DHTにはKademlia + コネクションプールを使用します
UPnPによってポートを解放することができますが、Port0でも利用可能です(接続数は少なくなります)
検索リクエスト、アップロード、ダウンロードなどのすべての通信はDHT的に分散され、特定のサーバーに依存しません
ｃ