[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
19: デフォルトの名無しさん [sage] 2024/03/18(月) 10:16:03.73 ID:pTevW9jL(2/3) AAS
おっさんのポエム
20: デフォルトの名無しさん [] 2024/03/18(月) 10:19:41.06 ID:HmpJvDlJ(2/2) AAS
あとArctanのテイラー展開
もしくは項別積分
項別積分する場合は、べき級数の収束半径とか、境界での連続性とかも
21: デフォルトの名無しさん [sage] 2024/03/18(月) 11:21:23.44 ID:dVjvry4m(2/2) AAS
積分変数を別名に変えても積分の結果が変わらないこと
などを証明することに興味無さすぎて
変数を使わない技術だけが発達しているんじゃないか
22(1): デフォルトの名無しさん [sage] 2024/03/18(月) 17:26:37.63 ID:pTevW9jL(3/3) AAS
道師様のお言葉
外部ﾘﾝｸ[pdf]:terrytao.files.wordpress.com
23(1): デフォルトの名無しさん [sage] 2024/03/18(月) 20:14:54.78 ID:nsefbItQ(1) AAS
>>4そしてあんたはプログラムができない
永久にすれ違いだなｗ
>>5実際に計算しない限りプログラムの世界では完成したとは言えない
できたような気になってるだけだｗ
24: デフォルトの名無しさん [] 2024/03/18(月) 20:38:29.54 ID:8wq33qzx(1) AAS
>>23
ふつうに証明支援系で証明できるが
25: デフォルトの名無しさん [sage] 2024/03/18(月) 20:59:25.05 ID:zv8Td5xB(1/2) AAS
変数に別の変数 (を含む式) を代入するのは嫌なので、右辺を実際に計算してしまった値を代入する
計算してない式を代入するのが何故そんなに嫌なのかを理解しない限り話が進まない
26: デフォルトの名無しさん [] 2024/03/18(月) 21:35:55.83 ID:fpvRWfHG(1) AAS
コード書けない奴が必死に妄想でレスバするクソスレ
ＮＧ決定
27: デフォルトの名無しさん [sage] 2024/03/18(月) 23:20:36.59 ID:zv8Td5xB(2/2) AAS
しかし、何も書かないより悪いコードを書く方がマシみたいな保証が
あると思うならそれこそ妄想なのでは
28: デフォルトの名無しさん [] 2024/03/19(火) 04:11:20.65 ID:YAmi9Hnz(1) AAS
数学を記述するには一階述語論理があれば十分
しかし処理系側は特殊なケースに特化するよりも自然に実装できる範囲で一般化したほうがいいだろう
命題の記述は依存型による
29(1): デフォルトの名無しさん [] 2024/03/19(火) 12:34:54.32 ID:pUZ6M7m/(1) AAS
動的型付けの証明支援系ってのは何をしてるんだ？
30: デフォルトの名無しさん [sage] 2024/03/19(火) 14:33:42.20 ID:NSxYSp14(1) AAS
○○を支援する言語と○○が可能な言語を分断するパラダイムはたしかにオワコンだ
逆に支援を語りえない所謂unsafeを書けるやつが比較的新しい
31(1): デフォルトの名無しさん [] 2024/03/19(火) 15:02:06.03 ID:YRVQB5Qs(1) AAS
>22(2): デフォルトの名無しさん [sage] 2024/03/16(土) 20:29:40.05 ID:TBzj9DHS(1) AAS
>>1
証明を記述するための言語がある。CoqとかAgdaとか
あと単発質問はスレを立てるまでもない質問スレでどうぞ
の紹介しているCoqとか、純粋関数型言語HaskellもPCで動く数学って感じではあるけども、そもそもメモリが有限なので連続を表現できない。
どんなに小さい数を表現できても有限である以上は離散的なのよねん。
離散数学の範囲ならHaskell良いよ。
子供向けだけど、Viscuit(ﾋﾞｽｹｯﾄ)は写像というか変換のみで言語作ってる。
（ビスケットの中の人曰く「書き換え型言語」）
32: デフォルトの名無しさん [] 2024/03/19(火) 15:24:32.49 ID:3KaIc7lk(1) AAS
>>31
ポエムは日記に書いてろ
33(2): デフォルトの名無しさん [] 2024/03/19(火) 16:20:03.06 ID:Q+qUW8xc(1) AAS
leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか？
34: デフォルトの名無しさん [] 2024/03/19(火) 16:58:20.60 ID:WY0TXEXb(1/3) AAS
>>33
勉強にはなるんじゃない？
35: デフォルトの名無しさん [] 2024/03/19(火) 16:59:03.63 ID:WY0TXEXb(2/3) AAS
ほんとうに教科書に載ってる定理の証明がぜんぶ正しく書かれてるなら、それは教科書読んでるのと同じわけだし
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の中でモナドの評価が低いよね
それはもったいないから言語を競争させる原理はよくない
上下前次1-新書関写板覧索設栞歴
あと 959 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.022s