14/10/26 21:24:52.33 cZX7ddvm.net
>>615
有限集合限定でよければHaskellのリストで代用できるだろ。重複要素を取り除くようにすればいいだけで。
「生産性が上がらないからHaskell等は却下」ということなら集合を扱う言語を新たに作っても生産性は上がらない。
1は「集合を扱う言語を作れば高い生産性をもつはずだ」と具体案も示さずに言っているだけ。
617:１
14/10/26 21:39:05.82 bR5aD7tI.net
>>616
リストで集合の代用できるのは確かにそうだが、それを言ったらいろんなデータ構造が無意味になっちゃうだろ。
代用できるだけじゃやっぱダメなんだよ。
具体案を出してないのは認める。
618:デフォルトの名無しさん
14/10/26 22:12:04.35 lx1fz+FP.net
「生産性」とかいいながらやっぱり効率の面で却下してるね
もいっぺん>>615-617を冷静に読みかえしてみて。
>>616は一言も効率(やデータ構造)の話はしてないよ
せめて自分の頭んなかくらい整理して書いてくれ
整理せずに断片的に書きちらしてるから後出しって言われんだよ
619:１
14/10/26 22:24:04.14 bR5aD7tI.net
>>618
俺も効率の話はしてないつもりだったが。
例えばキューやスタックなんかはリストで簡単に代用できるが、
専用のクラスを用意しておくことは意味があると思ってる。
620:デフォルトの名無しさん
14/10/26 22:37:21.48 lx1fz+FP.net
なんでそこでキューやスタックがでてくるんだｗ
有限集合の話じゃないのかよｗｗｗｗ
621:１
14/10/26 22:40:47.72 bR5aD7tI.net
集合とリストは本質的に異なるという立場。
まあ、代用はできるんだが。
622:デフォルトの名無しさん
14/10/26 22:51:49.39 lx1fz+FP.net
では>>616が書いて>>1も同意したように
"重複要素を取り除く"ような薄いラッパーをかませばhaskellのリストは有限集合の代用になるのに
それ以外に効率とは関係なく「生産性」の上で課題になる「集合とリストの本質的な違い」ってなんだ？
623:１
14/10/26 23:02:30.10 bR5aD7tI.net
ぶっちゃけラッパーかませば問題ないなｗ
そういう薄いラッパーみたいなこまごまとした小道具がきっちりそろってるのがRubyの魅力だったりする。
でもまあ、今更だけど効率的に計算オーダーが変わっちゃうのはやっぱちょっと気になるかな。
624:デフォルトの名無しさん
14/10/26 23:09:02.90 uNWVyTps.net
Rubyしかしらないだけでしょ
625:デフォルトの名無しさん
14/10/26 23:16:23.07 lx1fz+FP.net
効率以外の面では既存言語(例えばhaskell)に集合操作ぽいラッパーがあればそれで充分と認めたんだよな？
問題は有限集合を扱う効率だけだということになってかなり整理されたな。
じゃお前さんが「生産性」の上では充分だと思うようなラッパーを既存言語の上で定義してくれよ。
haskellでもrubyでもいいよ
それがあれば効率よく処理する必要があるターゲットがみんなにも具体的によくわかる。
626:１
14/10/27 00:02:38.69 hKk3OxSM.net
>「生産性」の上では充分だと思うようなラッパー
ここが一番難しい。
ぶっちゃけ、まだこれだというアイディアはない。
普通に考えると集合論で定義されている一般的な演算をインプリメントすることになるんだろうけど、
それで生産性どの程度あがるかなぁ。
まあ、>>59>>62でも言ってるけど、なんか面白いアイディアがないとダメかなと思ってる。
627:デフォルトの名無しさん
14/10/27 00:16:15.58 xsoB8LA3.net
ここまで短時間で主張を二転三転されると笑うしかないな
あえて好意的に解釈しても正気かどうか心配になるレベル
628:デフォルトの名無しさん
14/10/27 00:50:39.76 UstcwDIj.net
関数型で生産性上がらないみたいなこといってるけど、例えば商集合演算を書く時はどうすんの。
集合論に基づいた言語を作るなら、少なくとも関数がファーストクラスであることは生産性に大きく関わると思うんだけど。
あと数学の関数は状態を持たないから、全ての関数が参照透明であるかどうかはともかくとして、
数学の意味での関数を使う場合には参照透明な関数であることを制約するような記述ができる必要があるかもね。
629:デフォルトの名無しさん
14/10/27 03:06:19.81 S1pbHk8f.net
>>623
「集合論に基づいた言語」を新たにつくっても、その言語に「こまごまとした小道具」はそろってないわけだが、
そうするとその新言語は1にとって魅力がないってことになるんじゃないか?
Rubyだったら簡単にできることが新言語では簡単にはできないのだから。
630:デフォルトの名無しさん
14/10/27 04:05:38.32 dHQizD3i.net
>>420
>>409のリンク先にあるような、集合や列の内包表記を使ったプログラムを読むのは1にはしんどいってことだな。
631:デフォルトの名無しさん
14/10/27 05:43:19.35 Rvvlh30F.net
結局、ルビー以外を提案しても全部却下して
「ここがルビーのいいところ」とか書いちゃうんだよ。
関数型言語の生産性の高さも知らずにね。
632:デフォルトの名無しさん
14/10/27 06:55:54.77 9dCb0Lih.net
そもそも「作りたい」ってスレタイが間違ってんじゃね
こいつ絶対作る気ないだろ
633:デフォルトの名無しさん
14/10/27 11:42:55.16 VoSGhOqg.net
そんなことはどうでもいい
634:１
14/10/27 20:16:20.56 hKk3OxSM.net
>>627
まあ、確固たる主張があるわけではないからな。
>>628
関数はファーストクラスの方がいいだろうな。
参照透明性は微妙。
あるに越したことはないけど、そこ頑張りどころかなぁ？という気はする。
>>629
ぶっちゃけ、Rubyは最強言語なので。
そんな簡単には超えられないでしょう。
>>630
正直、かなりしんどい。
あれ以上は簡単にできないのかもしれんが。
>>631
関数型言語で生産性が上がる問題があるなら教えてくれ。
>>632
まだネタ出しの段階だからな。実装ははるか先の話だ。
635:１
14/10/27 20:19:14.66 hKk3OxSM.net
それにしてもprolog動かんなぁ。
センスないわ俺。
636:デフォルトの名無しさん
14/10/27 21:05:20.40 K1rstjve.net
>>634
>関数型言語で生産性が上がる問題があるなら教えてくれ。
で、相手が何か例を挙げたらケチつけるんだろw
自分は「集合論に基づいた言語」で生産性が上がる例を示さずにw
637:１
14/10/27 21:22:05.89 hKk3OxSM.net
俺がケチつけられないほど明確に生産性の上がってる問題を頼む。
638:１
14/10/27 21:25:15.63 hKk3OxSM.net
まあ、集合論に基づいた言語は絵空事で終わる可能性があるからな。
関数型言語はそんなことないんだろ？
639:デフォルトの名無しさん
14/10/27 21:40:34.27 xsoB8LA3.net
ほんとに何言ってんのかねこの人はｗｗｗ
640:デフォルトの名無しさん
14/10/27 21:48:32.99 K1rstjve.net
>>637
そうした例を挙げても1に餌を与えるだけだし。
関数型言語でも論理型言語でもその他でも同じこと。
641:デフォルトの名無しさん
14/10/27 22:01:34.98 UstcwDIj.net
高階関数によるチェインなんかは生産性のあがる例じゃないの。並列化も簡単でしょ。
まあ関数型のスレではないけど、集合論というか数学ってまさに関数型言語なのに、
よくわかってなさそうだからつっこまれるんだろうけど。
642:デフォルトの名無しさん
14/10/27 22:37:28.46 K1rstjve.net
>>300
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。
>>305
>集合論に基づいた言語では狭い領域の問題に限り（教科書の章末問題とか）
>高い生産性を発揮することを目標にしてる。
「サクサクっとインプリメント」できるどうか、「高い生産性を発揮」しているかどうかは、1の主観で判断される。
643:１
14/10/27 22:42:25.97 hKk3OxSM.net
>>641
確かに高階関数はカッコいい気がするが、具体的にどんな問題で使われてるか知らない。
並列化は簡単というが、まだ実現はしてなかったような。
まあ、俺は関数型言語も数学も造詣はないな。
644:デフォルトの名無しさん
14/10/27 22:54:12.79 CRLCLkYm.net
jqueryのメソッドチェーンは便利だね
645:デフォルトの名無しさん
14/10/27 22:57:50.25 UstcwDIj.net
>>643
個人的な経験でいえば、DBからデータを取ってきて加工したりするときに非常に書きやすいかな。
とにかく、コレクションのデータを加工して流すときに非常に簡潔に書ける。
他にもあるけど、今すぐに思いついたのはこれかな。
並列化はClojureなんかは簡単に書ける。Javaも8からできたんじゃなかったっけ。まあJavaのあれは関数型と言うには気持ち悪いけど。
というか、適用する関数が副作用を持たないと仮定するなら、作用させるデータを分割して再結合すればいいっていう単純な話でそ。
646:デフォルトの名無しさん
14/10/27 23:02:23.54 UstcwDIj.net
あ、メソッドチェーンにおける並列化が簡単にできるという意味ね。
プログラム自動並列化は詳しくないけどまだ発展途上じゃないかな。
647:１
14/10/27 23:32:47.45 hKk3OxSM.net
>>645
ふーむ。確かにコレクションのデータを加工して流すのは出現頻度が高そう。
勉強になりました。
Clojuerちょっとぐぐってみたけど、ソフトウェア・トランザクション・メモリーとかよくわからんかった。
とりあえず簡単に並列化できそうな雰囲気は伝わってきたｗ
648:デフォルトの名無しさん
14/10/28 00:54:20.05 2moDL6+C.net
>>とにかく、コレクションのデータを加工して流すときに非常に簡潔に書ける。
>ふーむ。確かにコレクションのデータを加工して流すのは出現頻度が高そう。
>勉強になりました。
このスレでHaskellの名前が出てから2ヶ月たつけど、2ヶ月の間に自分で調べたりはしなかったんだな。
649:デフォルトの名無しさん
14/10/28 01:22:16.19 F9KmtOQp.net
この言語が最強っていう信念のある人だからね
650:デフォルトの名無しさん
14/10/28 01:46:36.67 2moDL6+C.net
Ruby最強と思っているらしいけど、それなら新しい言語を作ろうなんて思わければ良さそうなものだがな。
新しい言語を作っても、Rubyにあるような、お気に入りの便利な機能なんかないから、「Rubyなら簡単にできるのに」
って不満がたまるだけだろうに。
集合を使った表記法のプログラムを読むのもかなりしんどいそうだし。>>634
651:デフォルトの名無しさん
14/10/28 13:51:55.51 /Y9XnqU0.net
>>638
ちょっと待った。
絵空事で終わらない可能性がゼロでないことを説明してくれ。
>>643
C++ やるんじゃなかったけ？ <functional> とか高階関数だらけじゃん。
Javascript とかでも良く使うよ。Ruby では使わないの？
652:デフォルトの名無しさん
14/10/28 14:27:02.71 BaOL+HSr.net
>>643
高階関数って名前じゃ無くても同じ事させてるのは体験してるだろ？
あるオブジェクトのリストを(必要な要素だけ抽出(filter)してデータ変換(map)して集約(reduce)させるとか
653:デフォルトの名無しさん
14/10/28 15:52:04.32 g7PPMDyH.net
関数型の生産性の証拠は求めるけど
もちろんルビー最強の証拠なんて知らんぷり
654:デフォルトの名無しさん
14/10/28 15:53:32.28 g7PPMDyH.net
典型的なルビ厨
655:デフォルトの名無しさん
14/10/28 16:20:55.17 mPN7Yd+C.net
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。
>集合論に基づいた言語では狭い領域の問題に限り（教科書の章末問題とか）
>高い生産性を発揮することを目標にしてる。
1の言う「生産性」はこういうことだから、教科書やそれに載ってる問題を具体的に挙げて、
この問題をこういうふうに書きたいんだけど、Rubyではこんなふうにしか書けない、
Haskellではこんなふうにしか書けない…、そのためにサクサクっとインプリメントすることができず、
生産性が上がらない
って話を1がしないとどうしようもないんだよな。
Rubyその他、既存の言語で「サクサクっとインプリメントすること」ができるのなら
新しい言語をつくる意味がないんだから。
656:デフォルトの名無しさん
14/10/28 20:20:01.18 sNcgfmnM.net
>>655
結局それにつきるな
それに対して1は具体的はアイディアがないからとか
返答になってないことをうだうだ言うだけで問題意識を明らかにしようとはせず
そのうちまた新しいループがはじまる、と。
657:１
14/10/28 21:27:06.97 Eyw4r4/G.net
>>648
まあな
>>651
>絵空事で終わらない可能性がゼロでないことを説明してくれ。
それはむずかしいな。
数学っぽくプログラムできたらいいんじゃね。とか
教科書の記述がそのまま実装になったらいいんじゃね、とか
そういう曖昧なイメージがあるだけで、見切り発車でスレたてたからな。
>C++ やるんじゃなかったけ？ <functional> とか高階関数だらけじゃん。
functionalって使ったことないかも。
setやmapでoperator<を定義することはあるけどそれとは違う？
>Ruby では使わないの？
Enumerableのメソッドならよく使うが。
>>652
Rubyのcollectとかはよく使う。
>>655
>>656
まあ、サクサクインプリメントできない問題が具体的にあったわけじゃないんだよな。
数学的な記述がそのまんま実装になったら楽しいかなぁとかその程度の問題意識しかなかった。
プログラミングの素養がなくても教科書丸コピで動いちゃうみたいな？
そんな感じ。
ちなみに、教科書丸コピは後付けなんだよなぁ。
いろいろやってるうちにこのスレを立てた時の最初の気持ちは何だったのかもう忘れてしまった。
658:デフォルトの名無しさん
14/10/28 22:13:27.20 SAcW2ukT.net
>>657
教科書の演習問題を丸コピすれば答を出してくれるソフトをつくろうと
してたのか? w
ごまかそうとしないで、どの教科書のどの演習問題をどのように実装できる
言語をつくろうとしているのかちゃんと書け。
659:デフォルトの名無しさん
14/10/28 23:02:45.22 SAcW2ukT.net
>>575
こんなことを書くぐらいだから、推論や数式処理の機能をもつ言語を考えていたわけじゃないよな。
660:デフォルトの名無しさん
14/10/29 01:09:17.84 7WbuvXm2.net
プログラミング言語に有限集合を扱う機能を持たせさえすれば
離散数学やアルゴリズムの教科書の
「数学的な記述がそのまんま実装になった」り
「プログラミングの素養がなくても教科書丸コピで動」かせるようになると
1は思っているということだな。
661:デフォルトの名無しさん
14/10/29 07:51:54.82 uFHhP6NK.net
>>657
>数学っぽくプログラムできたらいいんじゃね。とか
いい言語を教えてやろう。FORTRAN (FORmula TRANslator) だ。
662:デフォルトの名無しさん
14/10/29 15:03:48.76 +dOdWCkt.net
>>655
ヤフーニュースのコメント欄の私もそう思うボタンを探してしまった。
>>657
> setやmapでoperator<を定義することはあるけどそれとは違う？
std::set<int, std::less<int> > s;
const size_t c = std::count_if( s.begin(), s.end(), std::bind2nd(std::greater<int>(), 5) );
例えば後者。関数を返す関数を呼んで、戻された関数を別の関数が呼んでる。
663:デフォルトの名無しさん
14/10/29 20:53:26.55 0HNaGJ1I.net
当の本人がどうしたいのかハッキリしてない以上
「顧客が本当に必要だったもの」のあの絵の状態になる可能性は非常に高い
本人はプログラマのつもりかも知れんが、実際は顧客の物言いをしてる
しかも、注文とダメ出しだけ多くて、かつ本人は解ってる(つもり)というタイプの
この板は「こんなソフト作ってよ」と頼む場所ではないと思うのだが
664:デフォルトの名無しさん
14/10/29 21:05:16.16 ITcKex6d.net
まだ構想（＝夢）の段階であれこれと夢想し構想し、その過程が文字で見える過程を、傍からみている私は楽しんでいる
>>1 続けてくれ
665:１
14/10/29 23:04:45.80 6KDieIbJ.net
>>658
むりぽ
>>662
bind2ndとか知らなかったわ。テンプレート恐るべし。
まあ、勉強になりました。
>>664
ぶっちゃけ、毎日書き込むのつらくなってきたわ。
このスレは今後不定期更新になりますｗ
666:デフォルトの名無しさん
14/10/30 00:38:38.53 HxKeCYce.net
>>665
1が書き込んだあとには
1に餌を与えないでください
>>559 >>655-665
と書いたほうがいいな。
そうしないと同じことの繰り返しになるだろうから。
667:デフォルトの名無しさん
14/10/30 03:27:37.45 sggd5tBz.net
>>666
>>425も追加で。
668:１
14/10/31 20:03:03.95 g6D744er.net
prologのconnect4がどうしても動かん。
誰か俺のコードをデバッグしてくれ。現状のコードは以下。
get_atでリストのN番目の要素を返す。
get_stoneでBOARDの(X,Y)の位置にある石を返す。盤の外を指定したときは3を返す。
straightで連続した石の数を数える。DX,DYは連続した石を探索する方向。
board([[],[],[],[],[],[],[]]).
myboard([[1,2],[1,1],[1,1,1],[1,1,1,2],[],[],[1,2,1]]).
get_at(_,[],_):- fail.
get_at(0,[X|_],X).
get_at(N,[_|Ls],Y):-
N1 is N -1,
get_at(N1,Ls,Y).
get_stone(_,X,_,3):- X<0,!.
get_stone(_,X,_,3):- 6<X,!.
get_stone(_,_,Y,3):- Y<0,!.
get_stone(BOARD,X,Y,0):-
get_at(X,BOARD,Xs),
length(Xs,L),
Y >= L,!.
get_stone(BOARD,X,Y,S):-
get_at(X,BOARD,Xs),
get_at(Y,Xs,S),!.
straight(BOARD,X,Y,_,_,S,0):-
get_stone(BOARD,X,Y,S1),
S1 \== S,!.
straight(BOARD,X,Y,DX,DY,Stn,Len):-
X1 is X + DX,
Y1 is Y + DY,
Len1 is Len + 1,
straight(BOARD,X1,Y1,DX,DY,Stn,Len1),!.
669:デフォルトの名無しさん
14/10/31 20:34:56.87 eFG4AR46.net
>>668
それと「集合論に基づいた言語を作る」のとどういう関係があるんだ?
>>666-667
670:デフォルトの名無しさん
14/10/31 20:42:19.57 eFG4AR46.net
>>668
↓で教えてもらえ
【論理】Prolog【初心者】
ｽﾚﾘﾝｸ(tech板)
671:デフォルトの名無しさん
14/11/01 00:21:10.18 QdACbqof.net
>>670
その結果。
ｽﾚﾘﾝｸ(tech板:786番)
|全般的な感想として、1)..3) を見るに (Prolog 以前に)一般的なプログラミングの基礎が身に付いていないと思う
|おそらく集合理論言語スレの 1 だと思うけど、大学で情報系を専攻していたのなら情けない結果だ
|学生時代に遊んでいたのか、当時はできたけど今はその感覚が戻っていないだけなのか、わからないけどね
|現状のレベルでは、言語処理系を自作するなんてのは、夢物語か妄想のたぐいと判断せざるをえない
672:片山博文MZ次期CEO ◆T6xkBnTXz7B0
14/11/01 20:55:00.77 jtBHZTX6.net
Boost.Iclを参照せよ。
673:１
14/11/02 00:06:07.92 WfQoOxnP.net
>>672
情報はありがたいんだが、レスするのペースダウンするつもりなので宿題にさせてくれ。
674:デフォルトの名無しさん
14/11/02 14:33:07.98 2+jwxmIt.net
>>673
>宿題
集合論に基づいた言語の作成に関係があるからこのスレに書くべきだと示せるのでなければ
宿題はBoost総合スレにでも行ってやれ。
Boostに興味がある人・詳しい人はそっちのスレのほうが多くいるはずだ。
他の言語・ライブラリのことでも同様。その言語・ライブラリに興味がある人・詳しい人が多そうなスレを選んで書け。
>>425 >>559 >>655-665
675:1
14/11/02 18:33:09.61 WfQoOxnP.net
>>674
このスレの基本スタンスは雑談なので面白そうなトピックスは適宜拾っていったらいいんだぜ？
そうじゃなきゃ尺が稼げんだろうがｗ
676:デフォルトの名無しさん
14/11/02 20:08:03.24 4mhasaGI.net
>>425
今度は『ここは雑談スレだ』と言い出した。
677:１
14/11/02 21:55:00.94 WfQoOxnP.net
あと、このスレは俺中心に進めていく必要はないんだぜ？
みんなで雑談してくれて構わないんだぜ？
678:デフォルトの名無しさん
14/11/02 22:45:12.36 2oaHueQb.net
>>676
雑談スレはすでにあるのにな。
ｽﾚﾘﾝｸ(tech板)
>>559
1は「何でもいいから話題クレクレ」に路線変更。
679:デフォルトの名無しさん
14/11/03 08:07:42.94 FKymKC8X.net
>>1
> 徹底的に集合論的思想で言語仕様を考えるスレです。
どう読んでも雑談スレじゃないよね
680:デフォルトの名無しさん
14/11/03 11:16:05.33 C9Z/RfTt.net
それでもいいんじゃない‥雑談スレはすぐに話題が収束するからね‥
681:１
14/11/05 21:01:40.21 aXYuBMMC.net
prolog版connect4できたっぽいのであげます。
URLﾘﾝｸ(www.age2.tv)
長かった…！
prologでプログラミングするには…
なんと多くの辛抱が必要なものかと…！
あんまりテストしてないのでバグがあるかも。
682:１
14/11/05 21:29:06.77 aXYuBMMC.net
prolog識者がいたら添削たのむ
683:デフォルトの名無しさん
14/11/06 01:04:11.78 i9pGGwTT.net
>>681-682
>>669-670
>>425 >>559 >>655-665
684:デフォルトの名無しさん
14/11/06 01:47:04.84 TxZPnLvK.net
>>682
TwitterにPrologおじさんがいるからみてもらえ
685:１
14/11/06 20:03:55.57 1yGaI9pi.net
>>454
>>456
>>587
なんかコメントくれ。
>>684
Prologおじさんてその道で飯くってるひとじゃね？
こちらからタダで見てくれとは頼みづらいわな。
お前らみたいに自発的にスレ見てくれてる人とは訳が違う。
686:デフォルトの名無しさん
14/11/06 21:01:27.80 C8/OFtDI.net
>>685
>>454 >>456 >>587の3人にコメントを求める前に>>655-665。
1はプログラムを添削してほしいのに添削できる人が集まってそうなところを避けるようなバカだしな。
687:１
14/11/06 22:26:58.78 1yGaI9pi.net
Boost.Iclちらっとぐぐってみたけど、実装の大変さの割に活躍する場面があんまりないようなｗ
いつ使うかな～コレ。
たしかに集合っちゃ集合なんだけど正直微妙。
688:デフォルトの名無しさん
14/11/07 04:13:14.72 QM030TJs.net
>>685
>>1の「クレクレ」が不快だと言っている>>587に対してコメント「クレクレ」w
689:デフォルトの名無しさん
14/11/07 04:36:31.62 Nfw1pK0/.net
>>454 >>456 >>587が言ってるのは「集合論に基づいた言語」を作るのならPrologが参考になるはずということだろうから、
1がPrologで書いたプログラムにコメントしなけりゃいけないというものではないな。
690:デフォルトの名無しさん
14/11/07 17:32:05.33 eCqmNoes.net
実装が大変かどうかは問題にならん。
691:１
14/11/07 20:05:41.11 FWyIh5H/.net
>>690
まあ、ユーザーからすれば問題にならないけど。
Boostの人たちももうやり尽しちゃったて感じかなｗ。
692:デフォルトの名無しさん
14/11/08 05:55:33.54 N89Y1+Fh.net
これが集合論の何に参考になるのかサッパリわからんわ。
添削するだけ無駄。結局文句だけ言ってルビー最高って結論出すだけw
693:１
14/11/08 10:50:24.96 vsjOn1b1.net
>>692
おれもサッパリわからんわｗ
文句は>>454 >>456 >>587に言ってくれ。
prologでconnect4作ってみて思ったのは
connect4は習作として優れているってことと、
prologはconnect4作るのに向いてないってことだなｗ
prologでプログラム組むにはかなり慣れが必要。
ぶっちゃけ特殊技能やなこれ。
発想は面白いとおもうがこれで真面目にプログラム組もうと思う人がどれだけいることか。
しかし、prologの変数は参照透過なのかな。
haskellよりプログラム書きづらかったわ。
まあ、Ruby最強だな。
694:１
14/11/08 12:45:40.20 vsjOn1b1.net
×connect4は習作として優れている
○connect4は習作の題材として優れている
695:デフォルトの名無しさん
14/11/08 15:02:48.96 PXfop+Ut.net
>>693-694
>>300
>集合論に基づいた言語は教科書の章末問題をサクサクっとインプリメントすることを目的としてる。
>実用性はあんまり求めない。
connect4は、どの教科書の章末問題なんだ?
696:デフォルトの名無しさん
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的に分散され、特定のサーバーに依存しません
ｃ