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

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

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

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

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

**デフォルトの名無しさん** · 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畑のやつが処理系を作ればいい

**デフォルトの名無しさん** · 2025/01/25(土) 17:09:03.97

ここまでWolframの話題なし

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

rustがどうのとかいってるレベルだからね

**デフォルトの名無しさん** · 2025/01/25(土) 20:44:31.67

>>897 それはMathematicaじゃダメなん？
表記の体系って、プログラミングするには演算子の優先順位を決めないといけないがそれも決まってるの？
CSやってて数学のわからないところは記号の優先順位がわからなくて読み解けないことがある点

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

>>900
だめに決まってるじゃん

**デフォルトの名無しさん** · 2025/01/25(土) 22:33:12.05

>>900
Mathematicaは数式処理システムだ

**デフォルトの名無しさん** · 2025/01/25(土) 22:57:41.30

数論幾何用のソフトウェアがないってことかね、表記の体系はどこでみれるの
グレブナー基底とかならRisa/Asirとか群論ならgapとか
多分数学の分野ごとにソフトウェアがあるのが現状だと思う

**デフォルトの名無しさん** · 2025/01/25(土) 23:20:00.08

内容がわからないなら無理に書き込まなくていいのに

**デフォルトの名無しさん** · 2025/01/26(日) 01:21:09.90

必要なのはドリルではなく穴
記号ではなく意味
と思うじゃん？

**デフォルトの名無しさん** · 2025/01/26(日) 07:09:22.82

>>903
アホすぎて返す言葉もない

**デフォルトの名無しさん** · 2025/01/26(日) 07:29:10.83

ID:iLzbIZXE こういう現代文なら零点のレス返してくる人って、日々の生活相当苦労してそうだな

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

試験はギリギリ解けないレベルまで難化する
トーナメントは敗者で埋め尽くされる

**デフォルトの名無しさん** · 2025/01/26(日) 20:27:15.66

レベル、経験値、ポイント、HP、通貨、メッセージ数、フレンド数

4（死）、13（キリスト教における忌み数字）

18（嫌）、24（〜に死）、34（〜さん死）

40、42、44

56（殺）、64（無視）

71（無い）、74（無し）、79（無く、亡く）

84（〜は死）、94（〜君死）、96（黒）

このような数字と名前や生年月日、IDなどを組み合わせて執拗に強調することで、精神攻撃をする業者やストーカー、嫌がらせ組織がキモい。

**デフォルトの名無しさん** · 2025/01/26(日) 20:55:22.65

ドリル優子が大臣に

**デフォルトの名無しさん** · 2025/01/26(日) 22:29:07.43

経験的なデータはリセットできるからリセット不可能なものと分断されたり見下されたりする

**デフォルトの名無しさん** · 2025/01/26(日) 22:57:02.10

ごみはしんでもごみ

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

そう言えばPASCALのスレ無くなってるな
(ObjectPASCALやDelphi除く)

**デフォルトの名無しさん** · 2025/01/28(火) 00:55:22.49

スレタイ、レス件数、スレ作成日、投稿時刻に4や13、忌み数字を使って嫌がらせするネットストーカー、SNSストーカー業者がキモすぎ
4や13などの忌み数字と以下の情報、ポケベル暗号の数字などを（近い位置の並びで）組み合わせて使われていたら嫌がらせの可能性高し。

・名前やニックネーム
・生年月日
・住所、番地
・車のナンバー
・電話番号やメールアドレス

**デフォルトの名無しさん** · 2025/01/28(火) 00:57:38.03

業者の嫌がらせ数字組み合わせ

.204 〜に死
.214 21日生まれ（記念日の人）死
.224 夫婦死
.234 兄さん、爺さん死
.244 西死
.254 事故死、事後死、ニコ死
.264 〜に無視
.274 〜に無し、次男死
.284 〜には死
.294 〜29日生まれ（記念日の人）死

.304 〜さん死
.314
.324 〜さんに死
.334
.344
.354
.364 〜さん無視
.374 〜さん無し
.384 〜さんは無し
.394

執拗に強調することで精神攻撃になる業者の嫌がらせ手法がキモい

**デフォルトの名無しさん** · 2025/01/28(火) 06:05:44.47

閲覧171人とか174人、179人、180人、184人
／総視聴者数　（配信者の名前やID、誕生日などの語呂合わせ数字）

数字操作の嫌がらせがキモすぎ

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

暗号化技術とガロア体の関係を教えて下さい

**デフォルトの名無しさん** · 2025/01/28(火) 15:48:49.65

>>917
暗号化技術でガロアとの肉体関係

**デフォルトの名無しさん** · 2025/01/29(水) 21:16:18.67

忌み数字を踏ませる業者、アプリ、コンピュータプログラムの嫌がらせ

動画再生回数、表示回数、登録者数、フォロワー数、評価数、コメント数、レベル、経験値、ポイント、HP、通貨、価格、メッセージ数、通知数、フレンド数

4（死）、13（キリスト教における忌み数字）

18（嫌）、24（〜に死）、34（〜さん死）

40、42、44

56（殺）、64（無視）

71（無い）、74（無し）、79（無く、亡く）

84（〜は死）、94（〜君死）、96（黒）

このような数字と名前や生年月日、IDなどを組み合わせて執拗に強調することで、精神攻撃をする業者やストーカー、嫌がらせ組織がキモい。

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

サブタイピングは本当に必要なのか？

**デフォルトの名無しさん** · 2025/01/30(木) 06:49:31.93

サブタイピングはトポス

**デフォルトの名無しさん** · 2025/01/31(金) 21:06:58.24

閲覧171人とか174人、179人、180人、184人
／総視聴者数　（配信者の名前やID、誕生日などの語呂合わせ数字）

数字操作の嫌がらせがキモすぎ
競合配信者の名前、ポケベル数字、不吉数字の組み合わせ嫌がらせがキモすぎ

忌み数字が表示されやすくなる仕様のクソアプリ、数字操作がキモすぎ