「数学」をプログラミングするには

**デフォルトの名無しさん** · 2024/03/16(土) 19:41:45.98

たとえば、プログラミングで

π/4 = 1 - 1/3 + 1/5 - 1/7 + ...

を近似ではなく厳密に確かめるにはどうしたらいいの
人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど

**デフォルトの名無しさん** · 2024/12/11(水) 12:01:24.20

聞こえるな高卒の声が!

**デフォルトの名無しさん** · 2024/12/11(水) 12:05:21.25

誰でもできることには価値がないと判断しなかった者だけが
コタツでできる数学をやっている

**デフォルトの名無しさん** · 2024/12/11(水) 12:53:19.83

ポエム爺さんの代わりに考えてあげたのに酷い（笑）

**デフォルトの名無しさん** · 2024/12/11(水) 16:48:22.68

証明の正確さを検証するためのツールなのに、わかり切った証明（項の交換など）を明示的に書かなければいけない
なんつーか、退化してるよな

**デフォルトの名無しさん** · 2024/12/11(水) 16:58:43.02

>>1に言えよ

**デフォルトの名無しさん** · 2024/12/11(水) 17:49:58.78

>>751
退化しない答えをどうぞ

**デフォルトの名無しさん** · 2024/12/11(水) 21:55:37.54

自明な部分とそうでない部分は平等に検証されるべきか？

**デフォルトの名無しさん** · 2024/12/11(水) 21:59:14.97

自明をどうプログラムするんだ

**デフォルトの名無しさん** · 2024/12/11(水) 22:19:20.28

微積分レベルの問題をどう検証しろというのか？

**デフォルトの名無しさん** · 2024/12/11(水) 23:05:07.90

他人にケチつけられたら自画自賛すればいい

**デフォルトの名無しさん** · 2024/12/11(水) 23:49:27.18

俺ってスゲー

**デフォルトの名無しさん** · 2024/12/12(木) 05:18:25.46

こいつ数学板に連日粘着してるキチガイな

**デフォルトの名無しさん** · 2024/12/12(木) 07:40:20.49

自己紹介乙

**デフォルトの名無しさん** · 2024/12/12(木) 15:59:32.60

>>654
少数の表現を知らない素人

**デフォルトの名無しさん** · 2024/12/12(木) 17:39:01.48

数値計算の立場からすると・・・で無理だな

**デフォルトの名無しさん** · 2024/12/12(木) 17:39:21.03

解散

**デフォルトの名無しさん** · 2024/12/12(木) 18:55:56.72

>>761
じゃあ、正しく少数を表現できるコードをどうぞ。
前回の人は>685-686などというコードで信用無くした。

**デフォルトの名無しさん** · 2024/12/12(木) 19:13:14.19

ポエム爺

**デフォルトの名無しさん** · 2024/12/12(木) 19:23:46.43

>>764
アホすぎ

**デフォルトの名無しさん** · 2024/12/12(木) 19:33:03.74

空のバケツほどよく鳴る

**デフォルトの名無しさん** · 2024/12/13(金) 00:47:18.68

Ωをプログラムの表現しうる全データの集合
fを関数とするとf∈Ω
しかし、ΩからΩへの関数の集合の濃度はΩよりも大きいから矛盾

どういうことだ

**デフォルトの名無しさん** · 2024/12/13(金) 01:09:14.09

>>768
表示的意味論かよ。

**デフォルトの名無しさん** · 2024/12/13(金) 01:54:27.10

ゲーデルの不完全性を解けば人類は理論上次の次元に到達する
このスレの内容はちょっとだけ掠っているのでその調子でがんばって下さいね

**デフォルトの名無しさん** · 2024/12/13(金) 13:20:29.60

ゲバ本とゲバ棒を聴き間違えたことはある

**デフォルトの名無しさん** · 2024/12/13(金) 14:28:15.71

予言者
リーマン予想を解けば人類は理論上次の次元に到達する

**デフォルトの名無しさん** · 2024/12/13(金) 15:19:13.43

そういえばπの定義は微妙なので>>742の証明は形式的なものに過ぎない可能性がある

**デフォルトの名無しさん** · 2024/12/13(金) 23:05:29.33

>>762
任意精度数値計算ライブラリ

メモリに依存するみたいだけど

**デフォルトの名無しさん** · 2024/12/14(土) 14:08:54.29

言語論とか役に立たないからな
ソフトウェア工学学んだほうが役に立つよ

**デフォルトの名無しさん** · 2024/12/14(土) 16:08:00.44

計算可能実数というのがあってπは扱えるけど実数全体は無理

**デフォルトの名無しさん** · 2024/12/14(土) 17:28:54.01

終了

**デフォルトの名無しさん** · 2024/12/27(金) 06:43:26.62

球面上で風や海流などの分布を考えると、かならず流れが無い点Pが存在する
このことから、たとえば浮き輪の表面のようなハンドルのある曲面を球面座標でパラメータ付けできないことなどが分かる

数学では上のような性質をみたす点Pを具体的に構成せずに扱えるし、Pの性質だけから後者の命題を導くことも可能
こういうことが実用レベルでできるプログラミング言語は現状無い

**デフォルトの名無しさん** · 2024/12/27(金) 06:48:54.79

縮小写像はかならず不動点をもつ
このことから線形微分方程式の解の存在が言える
非自明な解を一個とってくるだけなら数値解析をする必要はない

**デフォルトの名無しさん** · 2024/12/27(金) 06:55:54.24

テンソル積、射影加群、入射加群、逆極限、順極限、……などはすべて普遍性で特徴づけられる
つまり、集合として具体的に構成をしなくても、他のすべての対象に対して射がみたす性質で一意的に定まる
しかも、これらのほとんどの議論は具体的構成を使わず、普遍性だけから従う

このような議論をするには、すべての加群のあつまりのような、無限集合にすらならない膨大な概念を考える必要がある
当然、構成に頼っていてはこのような概念をプログラミングで扱うことは不可能

**デフォルトの名無しさん** · 2024/12/27(金) 07:32:04.93

不動点定理は不動点を持たない関数(特に否定演算)がある領域では成り立たないよね。

不動点定理を前提にするのは「コンピュータの扱いやすい領域のみ扱う」と言っているようなものかと。

**デフォルトの名無しさん** · 2024/12/27(金) 07:49:18.68

>>781
それは不動点定理ではない

**デフォルトの名無しさん** · 2024/12/27(金) 07:50:43.08

掛け算の可換性は非可換群では成り立たないよねとか当たり前のことを言ってるようなもん
馬鹿丸出し

**デフォルトの名無しさん** · 2024/12/27(金) 15:58:43.91

爺のポエムは不変

**デフォルトの名無しさん** · 2024/12/27(金) 18:06:53.40

数学とプログラミングを対立構造で見てる時点で何もわかってない

**デフォルトの名無しさん** · 2024/12/27(金) 18:46:23.72

>>785
具体的にどのレスを指して「数学とプログラミングを対立構造で見てる」と言ってる？

ただの独り言？ならごめん。

**デフォルトの名無しさん** · 2024/12/27(金) 23:43:23.45

単一継承ならせいぜい親と子の対立しかない
多重継承なら親と親の対立もありえる
ドメインとドメインの対立

**デフォルトの名無しさん** · 2024/12/29(日) 17:37:12.88

命題⇔型
理論⇔ライブラリ

**デフォルトの名無しさん** · 2024/12/29(日) 17:42:01.70

物理とプログラミングは対立構造か

**デフォルトの名無しさん** · 2024/12/29(日) 17:51:31.87

言葉に酔ってるだけだろ

**デフォルトの名無しさん** · 2024/12/29(日) 18:41:16.54

自分が理解できないからと言って難癖をつけるのはやめましょう

**デフォルトの名無しさん** · 2024/12/29(日) 19:34:52.40

国語を勉強してくれ

**デフォルトの名無しさん** · 2024/12/29(日) 23:31:21.70

正しい言葉遣いをしたら綺麗事しか言わなくなると思うよ
オールドメディアを超越することと可読性は両立しない

**デフォルトの名無しさん** · 2024/12/30(月) 06:05:18.87

オールドメディアガー

**デフォルトの名無しさん** · 2024/12/30(月) 07:54:23.09

SNSで炎上商売

**デフォルトの名無しさん** · 2024/12/30(月) 23:30:57.09

商売なら買い手に責任がある
商品や作品の側に罪はないという理屈で変な物が作られる
買い手の方は責任を果たすために優れた物を買い、自然淘汰されるべき物には不買運動をする

**デフォルトの名無しさん** · 2025/01/09(木) 12:47:55.94

炎上商売にエンジョイ

**デフォルトの名無しさん** · 2025/01/12(日) 02:01:35.37

型に対してプログラミングすべき

**デフォルトの名無しさん** · 2025/01/12(日) 07:50:15.14

それやってもすぐ人間の能力限界にぶつかるから

**デフォルトの名無しさん** · 2025/01/12(日) 10:12:06.95

バリアントで統一

**デフォルトの名無しさん** · 2025/01/12(日) 10:51:45.53

空手型

**デフォルトの名無しさん** · 2025/01/12(日) 15:49:20.69

科学をプログラミングするのは難しいが
プログラミングを科学するのは可能では？

**デフォルトの名無しさん** · 2025/01/12(日) 16:35:24.05

主語がでかい

**デフォルトの名無しさん** · 2025/01/13(月) 02:34:19.05

オブジェクト指向って、コンピュータサイエンスじゃないんだよな
単に（一部の）人間にとって理解しやすくモジュール化しようってだけのことで、それで技術的に出来ることが増えるわけじゃないから

**デフォルトの名無しさん** · 2025/01/13(月) 02:37:56.75

構造化プログラミングや、関数プログラミングは、それ以前より高レベルの抽象化をもたらしたけど、オブジェクト指向は単に書き方の問題
科学論文で例えれば、構造化プログラミングや関数プログラミングは理論の内容に相当するが、オブジェクト指向は論文の体裁のこと

**デフォルトの名無しさん** · 2025/01/13(月) 02:40:56.25

そして、科学論文の体裁は重要だが、オブジェクト指向はいまや重要ではない

**デフォルトの名無しさん** · 2025/01/13(月) 05:24:15.88

型
並行性
最適化

この3つだよ
今求められてんのは

**デフォルトの名無しさん** · 2025/01/13(月) 09:04:54.93

求めてないよ

**デフォルトの名無しさん** · 2025/01/13(月) 09:12:00.23

俺が大学生だった20年前はオブジェクト指向もCSの一部だったが
教授はカプセル化が一番重要だといってた
研究はされてたけど、アスペクト指向は流行らなかったなー

**デフォルトの名無しさん** · 2025/01/13(月) 09:12:18.64

で、出ｗｗｗｗインターネットあまのじゃく君ｗｗｗｗｗｗｗ

**デフォルトの名無しさん** · 2025/01/13(月) 09:13:20.48

>>809
君、勉強できなそうだね

**デフォルトの名無しさん** · 2025/01/13(月) 09:42:56.67

>>809
たった三行でここまで頭悪そうな文章書けるのってある意味才能だな

**デフォルトの名無しさん** · 2025/01/13(月) 10:20:57.19

オブジェクト志向の次はデザインパターンだろ

**デフォルトの名無しさん** · 2025/01/13(月) 10:42:06.79

カプセル化も全否定されてるけど
いまだにアンダースコアの変数はモヤモヤする

**デフォルトの名無しさん** · 2025/01/13(月) 10:43:00.59

それも宗教
振り子が逆に振れてるだけ

**デフォルトの名無しさん** · 2025/01/13(月) 11:39:54.56

デザインパターン20数個のうち10数個ぐらいはただの高階関数でかけるという研究もある

**デフォルトの名無しさん** · 2025/01/13(月) 11:55:37.97

魔法はなかった

**デフォルトの名無しさん** · 2025/01/13(月) 13:02:05.46

>>816
そして残りの10個はただのアンチパターン

**デフォルトの名無しさん** · 2025/01/13(月) 17:18:23.47

岩波講座ソフトウェア科学 [基礎]1
計算システム入門
著者　所真理雄著
刊行日 1988/10/06

ソフトウェアの作成は人間的な作業で，信頼性や生産性の点でいまだに手工業の域にある．こうした現状をふまえ，ソフトウェア作成の方法を示すとともに，その理論と知識を整理し，新しい学問体系として提示する

**デフォルトの名無しさん** · 2025/01/14(火) 00:54:16.56

なぜ高階関数を使わないのか
εδ論法はなぜεの関数を具体的に構成しないのか
こういうのを体系的に整理したら特定の勢力だけが得をして他は損するんじゃないか
だから整理しない

**デフォルトの名無しさん** · 2025/01/14(火) 08:02:07.96

Foo = Bar | Baz

**デフォルトの名無しさん** · 2025/01/14(火) 08:15:31.11

型⊂クロージャ

**デフォルトの名無しさん** · 2025/01/14(火) 12:10:31.19

型なんて特別なものじゃない
0や1はInt型のオブジェクト、IntはType型のオブジェクト

**デフォルトの名無しさん** · 2025/01/14(火) 12:50:51.03

水の呼吸、壱の型

**デフォルトの名無しさん** · 2025/01/14(火) 13:27:13.44

>>824
咄嗟にアニメの話出せるとか
おまえすげえ最先端行ってるな
才能の塊かよ

**デフォルトの名無しさん** · 2025/01/14(火) 13:30:47.33

>>824
それ知ってるわ
煉獄さんの映画のやつだろ
お前マジでおもしれーな

**デフォルトの名無しさん** · 2025/01/14(火) 13:58:17.70

型が第一級オブジェクトなら、クロージャを使えば状態つきの型を作れるわけか

**デフォルトの名無しさん** · 2025/01/14(火) 14:18:33.81

有理数型や小数型も作れるのか？

**デフォルトの名無しさん** · 2025/01/14(火) 14:29:34.08

>>827
わざわざ型情報を実行時に変化させてどうすんだ

**デフォルトの名無しさん** · 2025/01/14(火) 14:29:54.43

>>828
お前は低レベルすぎ

**デフォルトの名無しさん** · 2025/01/14(火) 20:10:44.55

有理数型はHaskellやMathematicaにもうある
状態付きの型、考えただけで恐ろしい

**デフォルトの名無しさん** · 2025/01/14(火) 20:32:44.91

そうやって進化していくものよ

**デフォルトの名無しさん** · 2025/01/14(火) 21:00:24.45

状態付きの計算を行う手順を持った型なら純粋だから許せるけど
状態付きの型なんていらないよ

**デフォルトの名無しさん** · 2025/01/14(火) 21:07:31.89

君に要るかどうかは関係ない

**デフォルトの名無しさん** · 2025/01/15(水) 00:39:06.33

`f1 = Foo 1`なら、f1の型は`Foo 1`
基本的にはこれでいい
`Foo 1`は `{n: Nat} Foo n`のサブタイプ
`f1`を`Bar :: t -> s`に渡せるのは、`Foo 1`に変換する規則が存在するとき
型検査はそれをコンパイラがチェックすればいい

**デフォルトの名無しさん** · 2025/01/15(水) 00:39:55.88

`f1 = Foo 1`なら、`f1`の型は`Foo 1`
基本的にはこれでいい
`Foo 1`は `{n: Nat} Foo n`のサブタイプ
`f1`を`Bar :: t -> s`に渡せるのは、`Foo 1`を`t`に変換する規則が存在するとき
型検査はそれをコンパイラがチェックすればいい

**デフォルトの名無しさん** · 2025/01/15(水) 00:45:33.23

ユーザー定義関数から値返せないじゃん

**デフォルトの名無しさん** · 2025/01/15(水) 00:50:21.44

型は実体ではなく注釈か

**デフォルトの名無しさん** · 2025/01/15(水) 01:13:53.96

型っつっても所詮は構造体に名前がついただけ

計算の過程や性質に型付けをしたいんだ

「関数fを抜けたタイミングで、ポインタpは必ず指定の条件をみたす場所を指していなければならない」

こういうのを型で保証したいんだ

**デフォルトの名無しさん** · 2025/01/15(水) 01:33:23.91

ぬるぽは実行前に排除する

**デフォルトの名無しさん** · 2025/01/15(水) 06:39:48.90

>>839
理解浅すぎ
数学勉強してないでしょ

**デフォルトの名無しさん** · 2025/01/15(水) 08:07:10.18

>>841
君が数学で研究職に就いているのでなければ、まず間違いなく君よりは理解してるよ

**デフォルトの名無しさん** · 2025/01/15(水) 08:10:12.30

>>839
実行時のアサーションで書けることは、型にできる

**デフォルトの名無しさん** · 2025/01/15(水) 08:19:11.22

二分探索やクイックソートのロジックが正しいことを型で証明できるか

**デフォルトの名無しさん** · 2025/01/15(水) 08:32:18.93

数学的帰納法で証明できる
（長さ1の配列に対しては自明
長さ1, 2, ..., k-1に対して正しいと仮定して、長さkに対して証明する）
そのような構造はF代数で定式化できる

**デフォルトの名無しさん** · 2025/01/15(水) 08:56:17.03

アキュームレータを再帰的に更新していくようなのはF代数に抽象化できる

**デフォルトの名無しさん** · 2025/01/15(水) 19:07:44.03

オブジェクト指向はオワコン