集合論に基づいた言語を作りたいat TECH
集合論に基づいた言語を作りたい - 暇つぶし2ch707:デフォルトの名無しさん
14/11/09 06:16:58.35 co8RBkg8.net
>>706
だーかーらー、そのconnect4とやらのルールを集合論的に書けばいいって言ってるだろ。
さっさとやれ。

708:デフォルトの名無しさん
14/11/09 16:46:55.86 9LyR+5oz.net
1は何かものを作れる人間じゃないから。

709:1
14/11/09 18:17:59.58 Yrjok8yA.net
>>707
んーどうだろうな。
俺もスレたてた時はすべてを集合で表せば数学的にうまくいくんじゃね?とか思ってたんだけど、
やっぱリストはリスト、タプルはタプルなんだよな。
connect4も無理に集合的に扱わないで手続型で扱った方が自然かもしれないんだよな~
ぶっちゃけ、集合にこだわる意味が根底から揺らいでるw
数学の基礎的な部分が集合論でできてるってのはそうなんだろうけど、
応用問題解くときに些末な問題に煩わされたくないよね?

まあ、集合論でうまくいきそうな問題⇔教科書の章末問題かなぁとか思ってたんだけどさ。
その辺はあんまり整理できてない。

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:1
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で良いじゃんと思ってスレ開いたら1が馬鹿すぎてスレをそっと閉じることにした

719:1
14/11/17 21:47:20.82 IjeD6lYX.net
とりあえず、次の宿題は圏論かな~?

720:1
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:1
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:1
14/11/19 19:56:54.80 V2tDw9NJ.net
URLリンク(www.amazon.co.jp)
これ?
まあ本屋いってみてあったら立ち読みしてみるわ。

726:1
14/11/26 20:02:22.17 JT4BoUXj.net
圏論の基礎買ったけど早くも積読w

727:デフォルトの名無しさん
14/11/29 18:24:47.22 8AtyRUwF.net
>>701 の話だけど、ドコモで prolog が動いてる的な記事をなんかで読んだことがある

728:1
14/11/30 19:47:48.77 O0/vTNqA.net
URLリンク(iiyu.asablo.jp)
これか。
コード量10分の一は確かにすごい。
しかし2370万行とか正気の沙汰じゃないな。

729:デフォルトの名無しさん
14/11/30 22:28:37.23 mFsly3WX.net
Prolog で書くと「コード量10分の一」となる例には、他にも型推論があるね
以下の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:1
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やらが出てきて、逐次処理は隠蔽されるのでは?

それを考えると、1がlispで満足できないのが不思議でならない。

まぁ、文字通り「何も」考えていないのだろうな。

738:1
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:1
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:1
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:1
14/12/06 18:04:03.49 KgmhP8S/.net
途中で書き込んじゃった。
集合は{}で表すってイメージあるんだけど。

753:デフォルトの名無しさん
14/12/06 18:56:15.26 dXBvUp0m.net
clojureは#{}が集合のリテラルとしてある
他のlispでもリードマクロかけばそういうことはできる
是非についてなら。その表記が存在することが対象のプログラミングに有効ならあり、そうでなきゃなし

754:1
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:1
14/12/06 19:49:14.64 KgmhP8S/.net
リテラルの有無は結構気になるな、俺は。
Rubyの配列やマップのリテラルは気に入ってる。

759:1
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:1
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:1
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
ほんとこの1は駄目だな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:1
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:1
14/12/09 23:17:28.28 PZp4J+Rx.net
リアルが忙しくなりそうです。
しばらくこれなくなるかもだが、俺が留守の間おまえらでこのスレを盛り上げてくれよな。
よろしく。

773:デフォルトの名無しさん
14/12/10 21:31:22.32 7P/sQ89x.net
削除依頼していけよ

774:1
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:1
15/01/03 20:38:21.69 rEeqS3sH.net
ID違うと思うけど1です。
簡潔に実装できるんじゃなくて、
実装はHaskellとかでやって、その正しさをCoqで保証するの?
よくわからん。

781:1
15/01/03 21:16:03.70 rEeqS3sH.net
Coq単体で動くのか。
prologに近いのか?
ぶっちゃけかなりむずいなこれは。

782:1
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:1
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:1
15/01/06 00:03:50.53 iQ4UNt/k.net
Coqで任意の自然数nに対してn*(n+1)が偶数であることを証明しようとしたがどうしてもできない。
だれかHELP.

790:1
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:1
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:1
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:1
15/01/06 23:17:17.43 iQ4UNt/k.net
Coq難しすぎんよ~
もう寝る。

795:1
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:1
15/01/08 20:07:08.21 9tH8cNHX.net
ハルヒか?

802:1
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:1
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:1
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:1
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:1
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:1
15/01/15 21:04:35.89 RCkerH2f.net
お前らこのスレが伸びちゃ困る理由でもあるのかw

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:1
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:1
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:1
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:1
15/01/16 23:47:30.80 tbQRRWp6.net
>>827
結構むずかしい。
仮にできたとしても時間かかると思う。

829:1
15/01/17 00:13:16.15 e9PIZEl5.net
ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。
早めに身を引いた方がよさそうかな~とも思う。

830:片山博文MZ ◆T6xkBnTXz7B0
15/01/17 01:27:28.08 PPUSm5YO.net
数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。
では、そなたはどのような言語が希望か申し上げてみよ。

831:1
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:1
15/01/18 22:30:12.77 Pnbu8M/I.net
人工知能といえばdeep learningとかいうのが流行らしいんだが。

835:1
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:1
15/01/21 19:37:49.38 83hEDbKu.net
Coqは一日一時間までにする。
それ以上は自重。

840:1
15/01/21 20:33:19.47 83hEDbKu.net
片山さんの模範解答うp希望

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:1
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の完成が待ち遠しいプログラミングできないアスペルガーw


The Covenant Project
概要

Covenantは、純粋P2Pのファイル共有ソフトです

目的

インターネットにおける権力による抑圧を排除することが最終的な目標です。 そのためにCovenantでは、中央に依存しない、高効率で検索能力の高いファイル共有の機能をユーザーに提供します

特徴

Covenant = Bittorrent + Abstract Network + DHT + (Search = WoT + PoW)

接続は抽象化されているので、I2P, Tor, TCP, Proxy, その他を利用可能です
DHTにはKademlia + コネクションプールを使用します
UPnPによってポートを解放することができますが、Port0でも利用可能です(接続数は少なくなります)
検索リクエスト、アップロード、ダウンロードなどのすべての通信はDHT的に分散され、特定のサーバーに依存しません



最新レス表示
レスジャンプ
類似スレ一覧
スレッドの検索
話題のニュース
おまかせリスト
オプション
しおりを挟む
スレッドに書込
スレッドの一覧
暇つぶし2ch