計算機科学の基礎は集合論であるという。
ならば、集合論に基づいた言語を作れば美しい言語になるのでは?
そんな発想から徹底的に集合論的思想で言語仕様を考えるスレです。
探検
集合論に基づいた言語を作りたい
■ このスレッドは過去ログ倉庫に格納されています
1デフォルトの名無しさん
2014/08/10(日) 21:27:16.56ID:x7G32Sd08391
2015/01/21(水) 19:37:49.38ID:83hEDbKu Coqは一日一時間までにする。
それ以上は自重。
それ以上は自重。
8401
2015/01/21(水) 20:33:19.47ID:83hEDbKu 片山さんの模範解答うp希望
841片山博文MZ ◆T6xkBnTXz7B0
2015/01/21(水) 22:08:31.55ID: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.
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.
8421
2015/01/21(水) 22:49:05.70ID:83hEDbKu ふーむ。確かに片山さんのほうが自然な証明ですな。
843片山博文MZ ◆T6xkBnTXz7B0
2015/01/23(金) 02:17:55.54ID:22/uje4h 布教のために数学板でも展開するぞ。
【Coq】コンピューターで証明しよう【コック】・2ch.net
http://wc2014.2ch.net/test/read.cgi/math/1421944863/
【Coq】コンピューターで証明しよう【コック】・2ch.net
http://wc2014.2ch.net/test/read.cgi/math/1421944863/
844デフォルトの名無しさん
2015/10/21(水) 21:08:46.20ID:qGjQS7QU845デフォルトの名無しさん
2015/10/21(水) 21:49:58.99ID:kanshW5q ほう、4並べのソルバですか。面白い
なぜこのスレなのかは気にしないでおこう
thx
なぜこのスレなのかは気にしないでおこう
thx
846デフォルトの名無しさん
2016/05/01(日) 11:01:21.14ID:tKi6j9CT 匿名通信(Tor、i2p等)ができるファイル共有ソフトBitComet(ビットコメット)みたいな、
BitTorrentがオープンソースで開発されています
言語は何でも大丈夫だそうなので、P2P書きたい!って人居ませんか?
Covenantの作者(Lyrise)がそういう人と話したいそうなので、よろしければツイートお願いします
https://twitter.com/Lyrise_al
ちなみにオイラは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的に分散され、特定のサーバーに依存しません
c
BitTorrentがオープンソースで開発されています
言語は何でも大丈夫だそうなので、P2P書きたい!って人居ませんか?
Covenantの作者(Lyrise)がそういう人と話したいそうなので、よろしければツイートお願いします
https://twitter.com/Lyrise_al
ちなみにオイラは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的に分散され、特定のサーバーに依存しません
c
847デフォルトの名無しさん
2018/02/28(水) 18:29:32.35ID:F8/eMdWm やぁ
848デフォルトの名無しさん
2018/05/23(水) 22:19:44.05ID:Au5e7VGg 僕の知り合いの知り合いができたパソコン一台でお金持ちになれるやり方
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法 モニアレフヌノ』
TQ9W4
役に立つかもしれません
グーグルで検索するといいかも『ネットで稼ぐ方法 モニアレフヌノ』
TQ9W4
849デフォルトの名無しさん
2018/07/04(水) 23:44:36.75ID:gFgZc5FG 6HI
850デフォルトの名無しさん
2018/11/23(金) 11:17:18.34ID: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
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
851デフォルトの名無しさん
2018/11/23(金) 11:18:01.12ID:lDkmAROy sum (x:xs) = x + sum xs
852デフォルトの名無しさん
2018/11/25(日) 12:00:26.30ID:mrb3Dvz9 もう許してやれよ
853デフォルトの名無しさん
2019/06/19(水) 05:01:29.66ID:tVNS+22r 【出資】松本卓朗 人工知能詐欺【注意】
https://rio2016.5ch.net/test/read.cgi/rikei/1560859403/
https://rio2016.5ch.net/test/read.cgi/rikei/1560859403/
854デフォルトの名無しさん
2019/09/20(金) 10:28:23.43ID:4f4Q+09G Haskellじゃないの?
集合とか要素に型、集合にも型名を与えて処理する
Haskellとモナドの動画見てたけど少しだけ理解
計算は集合が状態遷移で形態(形状)変化した結果だと思う
[1 1]->sum->[1]みたいな
モナドの適当な感想
モナドは状態遷移を行う処理手続き関数の中に
バグや矛盾が入り込みにくい小さなプログラム単位を数珠つなぎに連鎖させ
エラーなり問題点の発生場所を明確化する手法な気がした
scalaのモナドは読むの辛いね(慣れ?)
集合とか要素に型、集合にも型名を与えて処理する
Haskellとモナドの動画見てたけど少しだけ理解
計算は集合が状態遷移で形態(形状)変化した結果だと思う
[1 1]->sum->[1]みたいな
モナドの適当な感想
モナドは状態遷移を行う処理手続き関数の中に
バグや矛盾が入り込みにくい小さなプログラム単位を数珠つなぎに連鎖させ
エラーなり問題点の発生場所を明確化する手法な気がした
scalaのモナドは読むの辛いね(慣れ?)
855デフォルトの名無しさん
2020/01/09(木) 12:03:21.50ID:Ydnkghao >>1
Z言語ではだめですか
Z言語ではだめですか
■ このスレッドは過去ログ倉庫に格納されています
ニュース
- 鈴木農相「おこめ券はお米しか買えないわけではない。例えば卵、味噌、しょうゆ、こうした購入に利用可能」 [Hitzeschleier★]
- なぜリベラルは人気がないのか 斎藤幸平さんが指し示す未来への道筋:朝日新聞 [少考さん★]
- なぜリベラルは人気がないのか 斎藤幸平さんが指し示す未来への道筋:朝日新聞 ★2 [少考さん★]
- 【日本人の旅行離れ】国内旅行すら行けなくなった……オーバーツーリズムだけじゃない 旅行者減少の異常事態 ★2 [ぐれ★]
- ベトナムのバイク「脱ガソリン」、シェア8割のホンダに打撃…政府が電動二輪普及を主導 [煮卵★]
- “ひとり焼肉”でおなじみ「焼肉ライク」が閉店ラッシュ。なぜ「コスパが悪い」と言われてしまうのか [Gecko★]
- トランプ「高市ちょっと飛んでみて」高市「?ぴょんぴょん(チャリンチャリン)」トランプ「よし、まだ金あるから防衛費増額な」 [931948549]
- 「台湾の女子アナ」ってよくね?※参考イメージあり
- 小泉防衛大臣「レーダー照射がサァ!中国がサァ!」米国「そう・・・(無関心)」 [834922174]
- ニート、無職、精神障害集まれ
- 【実況】博衣こよりのえちえちドラクエ1&2リメイク🧪
- ちびまる子ちゃんで一番可愛い子wwwww
