[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
36(2): デフォルトの名無しさん [] 2024/03/19(火) 17:00:04.15 ID:WY0TXEXb(3/3) AAS
lean4はプログラミング言語としても、haskellやrustくらいパワフルな言語なので、cだのfortranだの勉強するよりプログラミングの勉強にもなる
37: デフォルトの名無しさん [] 2024/03/19(火) 17:06:08.09 ID:50xBt2sS(1) AAS
>>29推論規則にしたがって項を削除したり、条件をみたす要素を深さ優先探索したり
38: デフォルトの名無しさん [] 2024/03/19(火) 17:54:01.83 ID:/7JjNXd8(1) AAS
証明支援系っつっても、ふつうにプログラム書くのと同じで、特定の問題の解法をプログラムしてるだけ
ようは論理のピタゴラスイッチ作ってるだけ
べつに未知の証明を自動で発見してくれるわけではない（もちろん、問題によっては自動的に解決できる場合もあるが）
39: デフォルトの名無しさん [] 2024/03/19(火) 17:56:38.86 ID:P1OcOpxu(1) AAS
証明支援系Lean4
数式処理システムSage
組版システムLaTeX
を組み合わせたオープンソースの統合数学環境と、黒板の文字や図を認識する入力インタフェースがあればいいと思う
40: デフォルトの名無しさん [] 2024/03/19(火) 18:04:10.23 ID:qttME5ET(1) AAS
>>36
「プログラミングの勉強」を「プログラム言語」の勉強だと思ってるバカ
「program」の意味を調べてみろ。言語はただの手法の一つ
41: デフォルトの名無しさん [sage] 2024/03/19(火) 18:56:00.18 ID:5dhARo0o(1) AAS
バカが必死で草
42: デフォルトの名無しさん [] 2024/03/19(火) 19:15:14.75 ID:IwEkPQSo(1) AAS
この馬鹿は何がしたいんだろ……
43(1): デフォルトの名無しさん [sage] 2024/03/20(水) 10:18:59.26 ID:ea1o2Ub5(1/4) AAS
>>36
CやFortranの評価が低いということはHaskellの中でモナドの評価が低いよね
それはもったいないから言語を競争させる原理はよくない
44: デフォルトの名無しさん [] 2024/03/20(水) 12:54:23.96 ID:VbUXRLzi(1) AAS
>>43
ポエムはよそで書いてろ
45: デフォルトの名無しさん [sage] 2024/03/20(水) 13:10:38.35 ID:ea1o2Ub5(2/4) AAS
ミサイルでも撃たれたならともかく
ポエムなるものを書き込まれたことへの反応が過剰なのが気になる
現実世界にポエムが存在しなくなれば消去法で「数学」になるってことなのかな
46: デフォルトの名無しさん [] 2024/03/20(水) 14:27:47.20 ID:I+zqr01r(1) AAS
スレタイが悪い
専門用語や英語を入れておかないと、自分も話題に参加できると勘違いした馬鹿が書き込む
47(1): デフォルトの名無しさん [sage] 2024/03/20(水) 15:26:54.49 ID:4PdbE3xv(1/3) AAS
仲よき事は美しき哉 志賀直哉
48: デフォルトの名無しさん [sage] 2024/03/20(水) 15:27:56.00 ID:4PdbE3xv(2/3) AAS
>>22これに反応できないお前ら
49: デフォルトの名無しさん [] 2024/03/20(水) 15:50:55.08 ID:vNXgKg89(1) AAS
>>47 武者小路実篤じゃなかったっけ
50(1): デフォルトの名無しさん [] 2024/03/20(水) 16:42:40.04 ID:ZN9vgvDp(1) AAS
>>3333(2): デフォルトの名無しさん [] 2024/03/19(火) 16:20:03.06 ID:Q+qUW8xc(1) AAS
leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか？
すでに解けてる問題を特定の処理系の言語に書き直すのが一大プロジェクトというのがくだらないと思う
51: デフォルトの名無しさん [sage] 2024/03/20(水) 16:54:28.92 ID:4PdbE3xv(3/3) AAS
>>12これにも反応できない雑魚ども
52(1): デフォルトの名無しさん [sage] 2024/03/20(水) 17:51:55.09 ID:ea1o2Ub5(3/4) AAS
>>50
すでに常識になっていることを「先入観にとらわれている」と思う人はいる
先入観をリセットしてやり直したい需要は多少はある
53: デフォルトの名無しさん [sage] 2024/03/20(水) 18:02:21.59 ID:Snv2Tioi(1) AAS
ポエム連発は草
54: デフォルトの名無しさん [] 2024/03/20(水) 21:22:26.43 ID:qwgU2fnR(1) AAS
>>52
馬鹿すぎて話にならない
わざとやってるならむしろお笑い番組の脚本とか考えるセンスあると思うよ
55: デフォルトの名無しさん [sage] 2024/03/20(水) 23:28:22.46 ID:ea1o2Ub5(4/4) AAS
わざと馬鹿になったのではないが
数学の範囲内の定理を厳密に証明しても、内か外かの判断は厳密にならないので
「プログラミングならなんでも数学」のような馬鹿な意見も厳密に全否定できないんだよな
56(3): デフォルトの名無しさん [] 2024/03/22(金) 15:38:04.26 ID:m8Pakijg(1) AAS
現代数学は集合と写像の言葉で書かれている
写像は関数の一般化だからC言語やHaskellなどの関数型言語では数学をプログラミングできない
RubyやPythonなどにはsetやmapといった機能があるから
これで数学をプログラミングできると思われる
57: デフォルトの名無しさん [sage] 2024/03/22(金) 15:41:43.35 ID:BpbPyhcF(1/2) AAS
厨二の夢だったのさ
58: デフォルトの名無しさん [] 2024/03/22(金) 22:21:33.16 ID:LL1SYasV(1/2) AAS
>>56
それは違う
数学ができるプログラミング言語のコンパイラをCで書くことができる
そもそもすべてのプログラム言語はチューリング完全だからCで書けてハスケルに書けないなどということは無い
59: デフォルトの名無しさん [sage] 2024/03/22(金) 22:53:17.07 ID:BpbPyhcF(2/2) AAS
所詮プログラムは人が書くもの
60(1): デフォルトの名無しさん [sage] 2024/03/22(金) 23:30:06.22 ID:CJ8mvd1G(1) AAS
>>56
それ逆だね
mapは関数型言語で登場した
そのRubyやPythonといったスクリプト言語は後からそれを導入した
上下前次1-新書関写板覧索設栞歴
あと 942 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.025s