[過去ﾛｸﾞ]
集合論に基づいた言語を作りたい (854ﾚｽ)
集合論に基づいた言語を作りたい http://mevius.5ch.net/test/read.cgi/tech/1407673636/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
1: デフォルトの名無しさん [] 2014/08/10(日) 21:27:16.56 ID:x7G32Sd0 計算機科学の基礎は集合論であるという。 ならば、集合論に基づいた言語を作れば美しい言語になるのでは？ そんな発想から徹底的に集合論的思想で言語仕様を考えるスレです。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/1
825: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/16(金) 18:52:49.05 ID:IPI8U3lP QZというのはC/C++宿題スレに生息している人だよ。 そうだな。2n＝n＋nの証明なんかどうかな？ 楽勝？ http://mevius.5ch.net/test/read.cgi/tech/1407673636/825
826: １ [sage] 2015/01/16(金) 19:09:16.59 ID:tbQRRWp6 掛け算の定義がどこにあるのかわからん。 証明もいいけどコードの自動生成のほうが面白そうかな〜 http://mevius.5ch.net/test/read.cgi/tech/1407673636/826
827: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/16(金) 22:32:01.39 ID:IPI8U3lP >>826 英語では、掛け算がmultiplicationで、自然数がnatural numbersだろ？ それを略すればmul,natになるだろ？ SearchAbout mul. SearchAbout nat. で検索できるから。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/827
828: １ [sage] 2015/01/16(金) 23:47:30.80 ID:tbQRRWp6 >>827 結構むずかしい。 仮にできたとしても時間かかると思う。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/828
829: １ [sage] 2015/01/17(土) 00:13:16.15 ID:e9PIZEl5 ぶっちゃけCoqやってると無限に時間を吸われる可能性がある。 早めに身を引いた方がよさそうかな〜とも思う。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/829
830: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/17(土) 01:27:28.08 ID:PPUSm5YO 数学に基づいた言語としてCoqは最適の例かと思われたが、御気に召さないとはこれ如何に。 では、そなたはどのような言語が希望か申し上げてみよ。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/830
831: １ [sage] 2015/01/17(土) 02:12:55.60 ID:e9PIZEl5 いや〜確かにCoq面白いんだけど。 勉強するのに時間かかり過ぎるっていうか もうちょっと市民権を得て入門書とか充実してからの方がいいかな〜と。 証明も紙なら簡単にできることが結構難しかったりで、 実利を得るところまで勉強進めるのがしんどい。 実用までいかなくてただのパズルで終わりそう。 Coq参考になるところは多いと思うんだけどね。 どこまで時間費やすか見極めたほうがよさげ。 片山さんはCoqにどの程度手ごたえ感じてるの？ http://mevius.5ch.net/test/read.cgi/tech/1407673636/831
832: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/17(土) 02:59:53.32 ID:PPUSm5YO 麿は、この素晴らしきCoqを使えば、不具合のないソフトウェアが作れると見ては、 これをマスターすれば世界征服も夢ではないと、そのような所存でおじゃるよ。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/832
833: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/17(土) 03:31:41.14 ID:PPUSm5YO Coqと人工知能を組み合わせたら……、金融取引に活かせば……とか楽しい妄想が広がるでおじゃる。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/833
834: １ [sage] 2015/01/18(日) 22:30:12.77 ID:Pnbu8M/I 人工知能といえばdeep learningとかいうのが流行らしいんだが。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/834
835: １ [sage] 2015/01/20(火) 23:02:01.33 ID:RE29itzd 2n=n+nはomegaで一発っぽい。 omegaなしだとどうやるかわからん。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/835
836: デフォルトの名無しさん [sage] 2015/01/21(水) 01:37:31.40 ID:+/NZ76QF 1に餌を与えないでください。 >>425>>559>>655-665 http://mevius.5ch.net/test/read.cgi/tech/1407673636/836
837: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/21(水) 08:55:01.51 ID:y20qOxOP n＝1×nを使う http://mevius.5ch.net/test/read.cgi/tech/1407673636/837
838: 1 [sage] 2015/01/21(水) 19:32:48.10 ID:83hEDbKu 途中よけいなことしてるかもだができたっぽい。 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. http://mevius.5ch.net/test/read.cgi/tech/1407673636/838
839: １ [sage] 2015/01/21(水) 19:37:49.38 ID:83hEDbKu Coqは一日一時間までにする。 それ以上は自重。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/839
840: １ [sage] 2015/01/21(水) 20:33:19.47 ID:83hEDbKu 片山さんの模範解答うｐ希望 http://mevius.5ch.net/test/read.cgi/tech/1407673636/840
841: 片山博文MZ ◆T6xkBnTXz7B0 [] 2015/01/21(水) 22:08:31.55 ID:OPHJ2hAi >>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. http://mevius.5ch.net/test/read.cgi/tech/1407673636/841
842: １ [sage] 2015/01/21(水) 22:49:05.70 ID:83hEDbKu ふーむ。確かに片山さんのほうが自然な証明ですな。 http://mevius.5ch.net/test/read.cgi/tech/1407673636/842
843: 片山博文MZ ◆T6xkBnTXz7B0 [sage] 2015/01/23(金) 02:17:55.54 ID:22/uje4h 布教のために数学板でも展開するぞ。 【Coq】コンピューターで証明しよう【コック】･2ch.net http://wc2014.2ch.net/test/read.cgi/math/1421944863/ http://mevius.5ch.net/test/read.cgi/tech/1407673636/843
844: デフォルトの名無しさん [sage] 2015/10/21(水) 21:08:46.20 ID:qGjQS7QU http://connect4.game-solver.org/?pos= http://mevius.5ch.net/test/read.cgi/tech/1407673636/844
845: デフォルトの名無しさん [sage] 2015/10/21(水) 21:49:58.99 ID:kanshW5q ほう、4並べのソルバですか。面白い なぜこのスレなのかは気にしないでおこう thx http://mevius.5ch.net/test/read.cgi/tech/1407673636/845
846: デフォルトの名無しさん [] 2016/05/01(日) 11:01:21.14 ID:tKi6j9CT 匿名通信（Tor、i2p等）ができるファイル共有ソフトBitComet（ビットコメット）みたいな、 BitTorrentがオープンソースで開発されています 言語は何でも大丈夫だそうなので、P2P書きたい！って人居ませんか？ Covenantの作者（Lyrise）がそういう人と話したいそうなので、よろしければツイートお願いします https://twitter.com/Lyrise_al ちなみにオイラはCovenantの完成が待ち遠しいプログラミングできないアスペルガーｗ The Covenant Project 概要 Covenantは、純粋P2Pのファイル共有ソフトです 目的 インターネットにおける権力による抑圧を排除することが最終的な目標です。 そのためにCovenantでは、中央に依存しない、高効率で検索能力の高いファイル共有の機能をユーザーに提供します 特徴 Covenant = Bittorrent + Abstract Network + DHT + (Search = WoT + PoW) 接続は抽象化されているので、I2P, Tor, TCP, Proxy, その他を利用可能です DHTにはKademlia + コネクションプールを使用します UPnPによってポートを解放することができますが、Port0でも利用可能です(接続数は少なくなります) 検索リクエスト、アップロード、ダウンロードなどのすべての通信はDHT的に分散され、特定のサーバーに依存しません ｃ http://mevius.5ch.net/test/read.cgi/tech/1407673636/846
847: デフォルトの名無しさん [sage] 2018/02/28(水) 18:29:32.35 ID:F8/eMdWm やぁ http://mevius.5ch.net/test/read.cgi/tech/1407673636/847
848: デフォルトの名無しさん [] 2018/05/23(水) 22:19:44.05 ID:Au5e7VGg 僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方 役に立つかもしれません グーグルで検索するといいかも『ネットで稼ぐ方法 モニアレフヌノ』 TQ9W4 http://mevius.5ch.net/test/read.cgi/tech/1407673636/848
849: デフォルトの名無しさん [] 2018/07/04(水) 23:44:36.75 ID:gFgZc5FG 6HI http://mevius.5ch.net/test/read.cgi/tech/1407673636/849
850: デフォルトの名無しさん [] 2018/11/23(金) 11:17:18.34 ID:lDkmAROy >>118 Haskellのクイックソートはリスト内包表記使った方が美しい。 qsort [] = [] qsort (x:xs) = small ++ [x] ++ leage where small = qsort [a|a <- xs,a <= x] leage = qsort [a|a <- xs,a > x] >>1 が求めるのってHaskellやPythonのリスト内包表記だけでプログラミングしたいとか？ SQLやC#のLinqにも通じるけど。 集合論的なのがあれば便利だけど、「だけ」と言うのはプログラミング上もキツイと思うな。 文字数を求める関数 再帰版 length [] = [] length (_:xs) = 1 + length xs リスト内包表記版 length xs = sum [1 | _ <- xs] ― リスト内包表記で1行になるけど、結局sum関数は必要。(チャレンジしたけど、リスト内包表記だけでsum関数は無理ぽ) sum [] = 0 sum (x:xs) = x + sum xs http://mevius.5ch.net/test/read.cgi/tech/1407673636/850
851: デフォルトの名無しさん [] 2018/11/23(金) 11:18:01.12 ID:lDkmAROy sum (x:xs) = x + sum xs http://mevius.5ch.net/test/read.cgi/tech/1407673636/851
852: デフォルトの名無しさん [] 2018/11/25(日) 12:00:26.30 ID:mrb3Dvz9 もう許してやれよ http://mevius.5ch.net/test/read.cgi/tech/1407673636/852
853: デフォルトの名無しさん [] 2019/06/19(水) 05:01:29.66 ID:tVNS+22r 【出資】松本卓朗 人工知能詐欺【注意】 https://rio2016.5ch.net/test/read.cgi/rikei/1560859403/ http://mevius.5ch.net/test/read.cgi/tech/1407673636/853
854: デフォルトの名無しさん [sage] 2019/09/20(金) 10:28:23.43 ID:4f4Q+09G Haskellじゃないの？ 集合とか要素に型、集合にも型名を与えて処理する Haskellとモナドの動画見てたけど少しだけ理解 計算は集合が状態遷移で形態(形状)変化した結果だと思う [1 1]->sum->[1]みたいな モナドの適当な感想 モナドは状態遷移を行う処理手続き関数の中に バグや矛盾が入り込みにくい小さなプログラム単位を数珠つなぎに連鎖させ エラーなり問題点の発生場所を明確化する手法な気がした scalaのモナドは読むの辛いね(慣れ？) http://mevius.5ch.net/test/read.cgi/tech/1407673636/854
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.227s*