[過去ﾛｸﾞ] 「数学」をプログラミングするには (1002ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
10: デフォルトの名無しさん [] 2024/03/17(日) 19:26:02.03 ID:OVnjvt7h(1) AAS
証明支援系で証明を書いても、それを再利用してべつの定理を自動で証明できるわけでもないし、ソフトウェアとして全く無意味だよね……
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(ﾋﾞｽｹｯﾄ)は写像というか変換のみで言語作ってる。
（ビスケットの中の人曰く「書き換え型言語」）
203: デフォルトの名無しさん [] 2024/04/02(火) 20:02:04.03 ID:GZPLkX8A(1) AAS
>>202202(1): デフォルトの名無しさん [] 2024/04/02(火) 20:00:28.70 ID:E9gZLeha(1/2) AAS
罵り愛が一段落下っぽいね。
まあ、何にせよ「数学」をそのままプログラミング出来てたら離散数学は今ほど重宝されてないと思う。
プログラミング言語の浮動小数点数も結局は離散数学だから、実数を浮動小数点数に、そして、CGとかだとさらに浮動小数点数を画面上のドット…つまり自然数(に0を加えたもの)の組(x,y)に変換しなきゃいけない。
アホ
207: デフォルトの名無しさん [sage] 2024/04/02(火) 20:54:29.03 ID:U2//VB/q(1) AAS
printf("数学をプログラミングする\n");
321: デフォルトの名無しさん [] 2024/04/15(月) 19:39:20.03 ID:NsRnPyj0(2/6) AAS
Q = 有理数の全体
Qの部分集合A, Bの組(A, B)で以下をみたすものをQの切断という
A ≠ ∅, B ≠ ∅
A∪B = Q
a∈A, b∈B ⇒ a < b
462: デフォルトの名無しさん [sage] 2024/04/26(金) 12:23:42.03 ID:BpYBau1Z(2/3) AAS
淵さんの悪口は止めてー
539: デフォルトの名無しさん [sage] 2024/05/07(火) 13:52:05.03 ID:pdFuXZMq(1/4) AAS
黒体輻射
554: デフォルトの名無しさん [] 2024/06/14(金) 19:32:02.03 ID:J8nW31cj(1) AAS
乗除算の近似解を加減算のみで求める技術
外部ﾘﾝｸ:qiita.com
580: デフォルトの名無しさん [sage] 2024/11/03(日) 23:55:07.03 ID:H5/A1U4T(4/4) AAS
でも、問題はプログラミング言語のいろんな特徴を反映させたデータ領域というのが、機能をひとつ追加するごとにその
定義の記述がめちゃくちゃ複雑になるというところにあると思う。つまり原理的にはできるかもしれないけれど、
現実的には不可能ってやつ。
結局、プログラミングでできる部分を数学にするにも、結局プログラミングしないといけないとかいう状況になる。
表示的意味論はそのプログラミングでできる部分をプログラミングするという意味のプログラミングの機能が乏しい。特にモジュール性がない。
584: デフォルトの名無しさん [sage] 2024/11/04(月) 20:20:29.03 ID:GSVf3MJi(1) AAS
表示的意味論
外部ﾘﾝｸ[pdf]:repository.kulib.kyoto-u.ac.jp
595: デフォルトの名無しさん [sage] 2024/11/12(火) 04:03:57.03 ID:15KCzjek(1/5) AAS
マシンや処理系の仕様に合わせてキーを打つのは人間様のすることではない
601(1): デフォルトの名無しさん [sage] 2024/11/12(火) 15:48:13.03 ID:3FuqnzdR(1) AAS
>>596596(5): デフォルトの名無しさん [sage] 2024/11/12(火) 04:10:14.19 ID:15KCzjek(2/5) AAS
x^2 = 2をみたす正の実数xは一意的に存在する
なら、それを√2というシンボルで扱えるようにすべきだ
計算は必要なときにだけすればいい
x = 1.4142云々という数値にしなければ扱えないのは不要な制約
これは誤差があるとかそういう問題ではない
人間の思考をコンピュータの都合に合わせようとしているのが問題
マジレスするとsympyとか使ってxのまま計算して
最後にsolveさせると良いよ
724(1): デフォルトの名無しさん [] 2024/12/05(木) 06:54:57.03 ID:Rf9rE6qz(1) AAS
O(n logn)のソートアルゴリズムいくつあると思ってんだ(笑)
763: デフォルトの名無しさん [sage] 2024/12/12(木) 17:39:21.03 ID:rgUDNRxT(4/6) AAS
解散
824(2): デフォルトの名無しさん [] 2025/01/14(火) 12:50:51.03 ID:1hGtsoWq(1) AAS
水の呼吸、壱の型
846: デフォルトの名無しさん [sage] 2025/01/15(水) 08:56:17.03 ID:3W/U+R8x(1) AAS
アキュームレータを再帰的に更新していくようなのはF代数に抽象化できる
847: デフォルトの名無しさん [sage] 2025/01/15(水) 19:07:44.03 ID:8y1isLBr(1) AAS
オブジェクト指向はオワコン
855: デフォルトの名無しさん [sage] 2025/01/16(木) 22:19:04.03 ID:FAOk1woG(2/2) AAS
研究者の名前がなかなか思い出せなかったがGriffinだな POPL 1990
915: デフォルトの名無しさん [] 2025/01/28(火) 00:57:38.03 ID:IzCMkZvk(2/3) AAS
業者の嫌がらせ数字組み合わせ
.204 〜に死
.214 21日生まれ（記念日の人）死
.224 夫婦死
.234 兄さん、爺さん死
.244 西死
.254 事故死、事後死、ニコ死
.264 〜に無視
.274 〜に無し、次男死
.284 〜には死
.294 〜29日生まれ（記念日の人）死
.304 〜さん死
.314
.324 〜さんに死
.334
.344
.354
.364 〜さん無視
.374 〜さん無し
.384 〜さんは無し
.394
執拗に強調することで精神攻撃になる業者の嫌がらせ手法がキモい
933: デフォルトの名無しさん [sage] 2025/02/04(火) 02:03:30.03 ID:axINJClc(1) AAS
装飾と結合
964: デフォルトの名無しさん [sage] 2025/02/08(土) 20:35:20.03 ID:r1W4t8Yl(1) AAS
>>962962(1): デフォルトの名無しさん [sage] 2025/02/08(土) 17:15:11.47 ID:2KjsmU3G(1) AAS
自然数論を含む、というのは選択公理に匹敵する非常に強い仮定だと思えば
何が起きようがあまり違和感はない
その仮定がない場合、たとえば
0 != 1
を肯定も否定もできないとかいうのはありふれた話で全然問題ない
定義を正確に述べよ
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.048s