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

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

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

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

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

**デフォルトの名無しさん** · 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

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

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

抽象データ型、凝集度、関心の分離などの既存の概念だけで簡潔かつ正確に説明できることをわざわざバズワードに言い換えただけのクソ概念

**デフォルトの名無しさん** · 2025/01/16(木) 03:23:35.34

形式論理とかまじで役に立たんからな

**デフォルトの名無しさん** · 2025/01/16(木) 08:27:28.13

実は当たり前にやっていること。関数適用はmodus ponensに相当する

**デフォルトの名無しさん** · 2025/01/16(木) 18:56:00.70

でも役に立たないでしょ
少しは文章読めよガイジ

**デフォルトの名無しさん** · 2025/01/16(木) 20:35:27.89

型情報からあまり使ったことない関数でも使い方にあたりがつくのは便利だと思うけどお前はそうではないんだな

**デフォルトの名無しさん** · 2025/01/16(木) 20:51:11.29

複素数型も四元数型も定義可能だし、GPUに組み込んで高速で並列演算できるようにしてやれば科学界に革命を起こせるな

**デフォルトの名無しさん** · 2025/01/16(木) 21:51:56.76

処理系がcall/ccをサポートすることは、直観主義論理に背理法を加えることに相当する

**デフォルトの名無しさん** · 2025/01/16(木) 22:19:04.03

研究者の名前がなかなか思い出せなかったがGriffinだな POPL 1990

**デフォルトの名無しさん** · 2025/01/16(木) 22:28:22.29

イマドキ型のない言語なんて、即席のスクリプトくらいにしか使わんでしょ

**デフォルトの名無しさん** · 2025/01/16(木) 22:31:22.46

代数的データ型やパラメータ多相を使えばプログラムのかなり多くの性質をコンパイラが保証できるのに、わざわざ型検査なしで注意してコード書くとか馬鹿のすること

**デフォルトの名無しさん** · 2025/01/16(木) 22:36:34.50

人類未曾有のソフトウェアを書くならともかく、巷のプログラムの9割近くのコードはただデータを整形してマッピングしてるだけ
あとの一割は既存のライブラリの呼び出し
現代のプログラミング言語の型システムがあれば、IDEの入力補完に従ってるだけでバグの無いコードが書ける
画面にらみつけてロジック確認なんかしてんのはただのアホ

**デフォルトの名無しさん** · 2025/01/16(木) 22:51:04.55

しかし、それができるなら動的型付けの言語でもエディタが構文から型推論すれば同じことができるのでは？

**デフォルトの名無しさん** · 2025/01/16(木) 23:35:14.70

ところがどっこい
型注釈無しでは型推論ができない、あるいはエラーにすべきか型チェッカが判定できないケースが存在する

まず簡単なのは、ユニオン型だ
f:: () -> Int | Str
みたいな関数は注釈なしでは、ふたつの箇所で異なる型を返してるのが間違いなのかどうか型チェッカには判定できない

パラメータ多相を使う高階関数も型推論が困難だ
map :: (a -> b) -> [a] -> [b]
これがたとえば二カ所で
map :: (Str -> Int) -> [Str] -> [Int]
map :: (Str -> Str) -> [Str] -> [Str]
と使われていたら、型チェッカは
map :: (Str -> Int|Str) -> [Str] ->[Int]|[Str]
だと推論するかも知れない。もしそうなると、
map :: (Str -> Str) -> [Str] -> [Int]
という使われ方をしていても、チェックに通ってしまうことになる

リフレクションやメタプログラミングをしている場合も勿論、コードだけから型推論するのは困難だ

逆に言えば、このようなケースに適切に型注釈をつければ、その他の部分は推論できるようになるので、生産性が格段に上がる

**デフォルトの名無しさん** · 2025/01/17(金) 04:10:24.01

なんかグダグダ言ってるけどそれ形式論理なしでできるよね
この話の発端は形式論理が役に立たないってことであって，型が役に立たないって話じゃないよ

**デフォルトの名無しさん** · 2025/01/17(金) 06:49:41.95

単純に、お前の話に誰も興味ないから話題が変わっただけでは

**デフォルトの名無しさん** · 2025/01/17(金) 09:10:34.70

ocamlなんかは型推論の健全性と完全性を備えているから
どんな式でも型がつくし、型エラーがでなければ正しいプログラムになるというのが保証されてる
健全性と完全性をどちらか捨てるとしたら完全性なので、そういう言語は型注釈が必要になる

**デフォルトの名無しさん** · 2025/01/17(金) 16:31:58.98

まぁ形式論理も時相論理もプログラミングには何の恩恵もないわな

**デフォルトの名無しさん** · 2025/01/17(金) 16:59:57.91

CSは数学を一部利用するが
数学はCSなんて知らんがな状態

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

学問にコンプレックス持ってる人って、みっともないね。

**デフォルトの名無しさん** · 2025/01/17(金) 20:14:27.37

>>857
パラメータ多相のジェネリックな型は特に制約を指定しなければ任意の型がOK何でもありだけど
何の型でもありということは使える範囲も極めて狭いというか
言語によってはprintすることすら任意の型が可能派と必ずしも可能とは限らない派もあり曖昧で
何らかの制約を指定しないと何の処理もできないためその型の値をそのまま返すことしかできなくなってしまう
つまりジェネリック型パラメータに対する制約記述がカギとなる

**デフォルトの名無しさん** · 2025/01/18(土) 08:09:37.99

>>866
多分コンプレックスとかじゃなくて無駄なものを持ち込まずにシンプルにしておきたいってだけじゃない