[過去ﾛｸﾞ]
「数学」をプログラミングするには (1002ﾚｽ)
「数学」をプログラミングするには http://mevius.5ch.net/test/read.cgi/tech/1710585705/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
29: デフォルトの名無しさん [] 2024/03/19(火) 12:34:54.32 ID:pUZ6M7m/ 動的型付けの証明支援系ってのは何をしてるんだ？ http://mevius.5ch.net/test/read.cgi/tech/1710585705/29
30: デフォルトの名無しさん [sage] 2024/03/19(火) 14:33:42.20 ID:NSxYSp14 ○○を支援する言語と○○が可能な言語を分断するパラダイムはたしかにオワコンだ 逆に支援を語りえない所謂unsafeを書けるやつが比較的新しい http://mevius.5ch.net/test/read.cgi/tech/1710585705/30
31: デフォルトの名無しさん [] 2024/03/19(火) 15:02:06.03 ID:YRVQB5Qs >2 の紹介しているCoqとか、純粋関数型言語HaskellもPCで動く数学って感じではあるけども、そもそもメモリが有限なので連続を表現できない。 どんなに小さい数を表現できても有限である以上は離散的なのよねん。 離散数学の範囲ならHaskell良いよ。 子供向けだけど、Viscuit(ﾋﾞｽｹｯﾄ)は写像というか変換のみで言語作ってる。 （ビスケットの中の人曰く「書き換え型言語」） http://mevius.5ch.net/test/read.cgi/tech/1710585705/31
32: デフォルトの名無しさん [] 2024/03/19(火) 15:24:32.49 ID:3KaIc7lk >>31 ポエムは日記に書いてろ http://mevius.5ch.net/test/read.cgi/tech/1710585705/32
33: デフォルトの名無しさん [] 2024/03/19(火) 16:20:03.06 ID:Q+qUW8xc leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか？ http://mevius.5ch.net/test/read.cgi/tech/1710585705/33
34: デフォルトの名無しさん [] 2024/03/19(火) 16:58:20.60 ID:WY0TXEXb >>33 勉強にはなるんじゃない？ http://mevius.5ch.net/test/read.cgi/tech/1710585705/34
35: デフォルトの名無しさん [] 2024/03/19(火) 16:59:03.63 ID:WY0TXEXb ほんとうに教科書に載ってる定理の証明がぜんぶ正しく書かれてるなら、それは教科書読んでるのと同じわけだし http://mevius.5ch.net/test/read.cgi/tech/1710585705/35
36: デフォルトの名無しさん [] 2024/03/19(火) 17:00:04.15 ID:WY0TXEXb lean4はプログラミング言語としても、haskellやrustくらいパワフルな言語なので、cだのfortranだの勉強するよりプログラミングの勉強にもなる http://mevius.5ch.net/test/read.cgi/tech/1710585705/36
37: デフォルトの名無しさん [] 2024/03/19(火) 17:06:08.09 ID:50xBt2sS >>29 推論規則にしたがって項を削除したり、条件をみたす要素を深さ優先探索したり http://mevius.5ch.net/test/read.cgi/tech/1710585705/37
38: デフォルトの名無しさん [] 2024/03/19(火) 17:54:01.83 ID:/7JjNXd8 証明支援系っつっても、ふつうにプログラム書くのと同じで、特定の問題の解法をプログラムしてるだけ ようは論理のピタゴラスイッチ作ってるだけ べつに未知の証明を自動で発見してくれるわけではない（もちろん、問題によっては自動的に解決できる場合もあるが） http://mevius.5ch.net/test/read.cgi/tech/1710585705/38
39: デフォルトの名無しさん [] 2024/03/19(火) 17:56:38.86 ID:P1OcOpxu 証明支援系Lean4 数式処理システムSage 組版システムLaTeX を組み合わせたオープンソースの統合数学環境と、黒板の文字や図を認識する入力インタフェースがあればいいと思う http://mevius.5ch.net/test/read.cgi/tech/1710585705/39
40: デフォルトの名無しさん [] 2024/03/19(火) 18:04:10.23 ID:qttME5ET >>36 「プログラミングの勉強」を「プログラム言語」の勉強だと思ってるバカ 「program」の意味を調べてみろ。言語はただの手法の一つ http://mevius.5ch.net/test/read.cgi/tech/1710585705/40
41: デフォルトの名無しさん [sage] 2024/03/19(火) 18:56:00.18 ID:5dhARo0o バカが必死で草 http://mevius.5ch.net/test/read.cgi/tech/1710585705/41
42: デフォルトの名無しさん [] 2024/03/19(火) 19:15:14.75 ID:IwEkPQSo この馬鹿は何がしたいんだろ…… http://mevius.5ch.net/test/read.cgi/tech/1710585705/42
43: デフォルトの名無しさん [sage] 2024/03/20(水) 10:18:59.26 ID:ea1o2Ub5 >>36 CやFortranの評価が低いということはHaskellの中でモナドの評価が低いよね それはもったいないから言語を競争させる原理はよくない http://mevius.5ch.net/test/read.cgi/tech/1710585705/43
44: デフォルトの名無しさん [] 2024/03/20(水) 12:54:23.96 ID:VbUXRLzi >>43 ポエムはよそで書いてろ http://mevius.5ch.net/test/read.cgi/tech/1710585705/44
45: デフォルトの名無しさん [sage] 2024/03/20(水) 13:10:38.35 ID:ea1o2Ub5 ミサイルでも撃たれたならともかく ポエムなるものを書き込まれたことへの反応が過剰なのが気になる 現実世界にポエムが存在しなくなれば消去法で「数学」になるってことなのかな http://mevius.5ch.net/test/read.cgi/tech/1710585705/45
46: デフォルトの名無しさん [] 2024/03/20(水) 14:27:47.20 ID:I+zqr01r スレタイが悪い 専門用語や英語を入れておかないと、自分も話題に参加できると勘違いした馬鹿が書き込む http://mevius.5ch.net/test/read.cgi/tech/1710585705/46
47: デフォルトの名無しさん [sage] 2024/03/20(水) 15:26:54.49 ID:4PdbE3xv 仲よき事は美しき哉 志賀直哉 http://mevius.5ch.net/test/read.cgi/tech/1710585705/47
48: デフォルトの名無しさん [sage] 2024/03/20(水) 15:27:56.00 ID:4PdbE3xv >>22 これに反応できないお前ら http://mevius.5ch.net/test/read.cgi/tech/1710585705/48
49: デフォルトの名無しさん [] 2024/03/20(水) 15:50:55.08 ID:vNXgKg89 >>47 武者小路実篤じゃなかったっけ http://mevius.5ch.net/test/read.cgi/tech/1710585705/49
50: デフォルトの名無しさん [] 2024/03/20(水) 16:42:40.04 ID:ZN9vgvDp >>33 すでに解けてる問題を特定の処理系の言語に書き直すのが一大プロジェクトというのがくだらないと思う http://mevius.5ch.net/test/read.cgi/tech/1710585705/50
51: デフォルトの名無しさん [sage] 2024/03/20(水) 16:54:28.92 ID:4PdbE3xv >>12 これにも反応できない雑魚ども http://mevius.5ch.net/test/read.cgi/tech/1710585705/51
52: デフォルトの名無しさん [sage] 2024/03/20(水) 17:51:55.09 ID:ea1o2Ub5 >>50 すでに常識になっていることを「先入観にとらわれている」と思う人はいる 先入観をリセットしてやり直したい需要は多少はある http://mevius.5ch.net/test/read.cgi/tech/1710585705/52
53: デフォルトの名無しさん [sage] 2024/03/20(水) 18:02:21.59 ID:Snv2Tioi ポエム連発は草 http://mevius.5ch.net/test/read.cgi/tech/1710585705/53
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 949 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.019s