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

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

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

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

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

**デフォルトの名無しさん** · 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
多分コンプレックスとかじゃなくて無駄なものを持ち込まずにシンプルにしておきたいってだけじゃない

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

>>865 数学が専門の人がどんどんCSに入ってきて内容が高度化してるって聞いたぞ俺は

**デフォルトの名無しさん** · 2025/01/18(土) 10:15:15.14

シンプレックスでコンプレックス

**デフォルトの名無しさん** · 2025/01/18(土) 11:19:59.28

なんでコンプレックスの話が出て来てるのかさっぱり判らん

>>869
それこそ >>865 の説を補強してるだけじゃないの

**デフォルトの名無しさん** · 2025/01/18(土) 11:57:14.53

>>868
イミフ

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

>>868
数学やCSを持ち込んで対象が複雑になると思ってるのは、
自分が理解できないものにコンプレックス持ってるからだよ
理論を作って対象が複雑になることはあり得ない

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

>>873
一筆書きして最初の場所に戻ってこられるか、は複雑な問題
グラフのすべての頂点から出ている辺の数が偶数、というのは単純な問題

グラフ理論を持ち込んで問題が複雑になったというのは、
頂点・辺・偶数・奇数などの概念が理解できないから
それは数学に対するコンプレックスにほかならない

**デフォルトの名無しさん** · 2025/01/18(土) 12:39:38.25

>>871 P=NP予想とかCSの問題も数学で扱われてるんだから知らんがな状態ではないと思う

**デフォルトの名無しさん** · 2025/01/18(土) 15:06:03.89

プログラミングに必要な数学は数値計算で使う数学くらいか？
微積と線形

圏論がプログラミングで無意味なのは誰でもわかるか

**デフォルトの名無しさん** · 2025/01/18(土) 15:34:34.81

>>876
プログラミングと数学を分けてる時点で、Qiitaのブログのサンプルコピペしてる雑魚と同レベル

**デフォルトの名無しさん** · 2025/01/18(土) 15:41:30.33

反論になってないなぁ

**デフォルトの名無しさん** · 2025/01/18(土) 16:26:51.31

プログラミングに数学はいくらでも使うことができる
プログラミングに使う数学とか言ってんのは、ただ単に自分が数学を学びたくないだけ

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

Felleisen 30年研究して「プログラミングには型が必要なことがわかった」←これ好き

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

型＝命題
項＝証明

この対応は、通常のプログラミングでも同様
そう思えないってことは、型の使い方が大雑把すぎるってこと

**デフォルトの名無しさん** · 2025/01/20(月) 06:41:50.30

>>881
お前のソースコード見せてくれよ
どんだけ立派なのか拝ませてくれ

**デフォルトの名無しさん** · 2025/01/20(月) 08:41:47.10

立派とは？

**デフォルトの名無しさん** · 2025/01/20(月) 08:45:50.71

int i=10;
char c='a';
printf("%d\n",i+c);
こんなのがかけるC++ではカリーハワード同型対応なりたたなさそう

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

C/C++の型付けは、メモリをなんぼ確保するかの目印でしかないからな

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

Rustの型はトレイト属性があって
マルチスレッドでも同期が保証される型など
抽象度の高い表現が型システムで扱えるようになってるね
それによりデータ競合が起きないことを型システムで保証してしまってるところが凄いと思った

**デフォルトの名無しさん** · 2025/01/24(金) 08:08:03.61

その代わりにmany shared XOR one mutableのキツいルールがあるけどな。

**デフォルトの名無しさん** · 2025/01/24(金) 08:08:50.30

自力で証明するよりも他者の言質を取るというか契約が成立することにより安全が保証される
という思考に人類は依存しすぎている
半導体は自作できないかもしれないが数学は紙媒体でもできる

**デフォルトの名無しさん** · 2025/01/24(金) 10:45:51.66

正直、Rustに心酔してる奴って、程度が低すぎ・・・
PythonやC#みたいなオモチャと比べたら、たしかにRustはマトモだ

だが、しょせんはまだ従来型のプログラミング言語
人間の思考ほどの表現力は無い

**デフォルトの名無しさん** · 2025/01/24(金) 10:51:55.41

言っちゃ悪いが、人間の知能は平等ではない
ある人にとってはRustは自分の思考よりも高機能だから、Rustに引き上げてもらえる
しかし、ある人にとってはRustを書くことは、Rustの書き方に思考を制限することになる

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

ある人は数論幾何学や場の量子論などがわかるが、ある人は中学校の連立方程式くらいしかわからない
連立方程式が世界で一番高度な学問と感じる人にとって、プログラミン言語はまるで魔法のようなのかも知れない
が、数論幾何の水準の人にはプログラミング言語は耐え難いほど低水準だ

**デフォルトの名無しさん** · 2025/01/24(金) 11:22:58.16

振舞いを自動化しろと言われるのと判断は人間の責任っていうのは
振舞いと判断を区別すれば矛盾しないんだけど
「証明する」というのは振舞いか判断かさっぱり分からんから矛盾だという批判がある

**デフォルトの名無しさん** · 2025/01/24(金) 22:28:54.69

>>887
single writer XOR multiple readers はデータ参照の競合バグを防ぐために役立つルール
これを守ると参照競合によるバグを防げるだけでなく
プログラムのスパゲッティ化を防ぐ効果も高い

さらにRustではそこに内部可変性が用意されているため
そのルールを守ったまま複数のデータ更新者(ex.マルチスレッド)が排他制御しながら同じデータを書き換えることも可能

**デフォルトの名無しさん** · 2025/01/25(土) 03:45:14.01

構ってもらえる相手を探し求めさまよう某

**デフォルトの名無しさん** · 2025/01/25(土) 10:55:48.38

>>891 その数論幾何の人にプログラミング言語を作ってもらえばいいんでね

**デフォルトの名無しさん** · 2025/01/25(土) 11:31:31.34

新商品を作ることにより今後の支障がなくなるといつから錯覚していた

**デフォルトの名無しさん** · 2025/01/25(土) 15:36:14.98

>>895
すでに表記の体系はある
CS畑のやつが処理系を作ればいい