- 1 名前：デフォルトの名無しさん [2024/03/16(土) 19:41:45.98 ID:nuwGv9us.net]
- たとえば、プログラミングで
π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
を近似ではなく厳密に確かめるにはどうしたらいいの
人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど
- 741 名前：デフォルトの名無しさん mailto:sage [2024/12/05(木) 19:14:20.85 ID:2vtwGPgw.net]
- こんな過疎地で持論書き込んで楽しいか？
- 742 名前：デフォルトの名無しさん mailto:sage [2024/12/05(木) 19:41:07.77 ID:0lWk1Gz/.net]
- 事実のみを指摘した
- 743 名前：デフォルトの名無しさん mailto:sage [2024/12/05(木) 20:22:08.32 ID:wt4vQ/2p.net]
- Haskell厨かな
妄想も大概に
- 744 名前：デフォルトの名無しさん mailto:sage [2024/12/05(木) 22:23:42.65 ID:nFy0adPc.net]
- 効率って短時間という意味だよな
たとえば疑わしきを3秒くらいで罰するとか
- 745 名前：デフォルトの名無しさん mailto:sage [2024/12/06(金) 11:22:43.20 ID:x1xEzr8K.net]
- >>1
プログラムでかすぎｗ
- 746 名前：デフォルトの名無しさん mailto:sage [2024/12/07(土) 20:49:06.54 ID:tbnxnovb.net]
- >>1
この数式の意味がわからん
- 747 名前：デフォルトの名無しさん mailto:sage [2024/12/08(日) 04:36:47.48 ID:hBOt4r+U.net]
- >>738
https://ja.wikipedia.org/wiki/ライプニッツの公式
- 748 名前：デフォルトの名無しさん mailto:sage [2024/12/08(日) 06:34:59.65 ID:X+KuZzcS.net]
- >>738
高卒がプログラミングなんかすんなよ
- 749 名前：デフォルトの名無しさん mailto:sage [2024/12/08(日) 18:25:16.09 ID:BmTfINn6.net]
- >>740
こんなのプログラミングに使わないけどw
中高生がプログラミングするのは今や当たり前だけどw
- 750 名前：デフォルトの名無しさん mailto:sage [2024/12/09(月) 18:37:31.14 ID:URePCLgA.net]
- グレゴリー・ライプニッツ級数の２通りの証明
https://manabitimes.jp/math/775
- 751 名前：デフォルトの名無しさん mailto:sage [2024/12/10(火) 17:38:45.30 ID:r/rGR6/m.net]
- Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明
https://mathlog.info/articles/1405
- 752 名前：デフォルトの名無しさん mailto:sage [2024/12/10(火) 21:35:24.14 ID:r/rGR6/m.net]
- グレゴリー・ライプニッツ級数の収束をCoqで証明する際には、Realsライブラリを用いて実数の扱いを行い、級数の定義を元に収束の証明を組み立てます。証明の詳細は、数列の部分和の収束を示すために必要な補題や定理を適宜導入し、論理的に証明を進めていく必要があります。
- 753 名前：デフォルトの名無しさん mailto:sage [2024/12/10(火) 23:33:12.40 ID:v+7nHz1f.net]
- いくらなんでもめんどくさすぎる
- 754 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 09:58:45.55 ID:9ebR4E1i.net]
- 数学とはそういうもんだ
- 755 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 11:46:13.42 ID:9ebR4E1i.net]
- 馬鹿でもケチは付けられる
- 756 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 12:01:24.20 ID:/aZNYiYX.net]
- 聞こえるな高卒の声が!
- 757 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 12:05:21.25 ID:DIyj35fU.net]
- 誰でもできることには価値がないと判断しなかった者だけが
コタツでできる数学をやっている
- 758 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 12:53:19.83 ID:9ebR4E1i.net]
- ポエム爺さんの代わりに考えてあげたのに酷い（笑）
- 759 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 16:48:22.68 ID:CTc5DRpT.net]
- 証明の正確さを検証するためのツールなのに、わかり切った証明（項の交換など）を明示的に書かなければいけない
なんつーか、退化してるよな
- 760 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 16:58:43.02 ID:9ebR4E1i.net]
- >>1に言えよ
- 761 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 17:49:58.78 ID:9ebR4E1i.net]
- >>751
退化しない答えをどうぞ
- 762 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 21:55:37.54 ID:DIyj35fU.net]
- 自明な部分とそうでない部分は平等に検証されるべきか？
- 763 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 21:59:14.97 ID:9ebR4E1i.net]
- 自明をどうプログラムするんだ
- 764 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 22:19:20.28 ID:9ebR4E1i.net]
- 微積分レベルの問題をどう検証しろというのか？
- 765 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 23:05:07.90 ID:DIyj35fU.net]
- 他人にケチつけられたら自画自賛すればいい
- 766 名前：デフォルトの名無しさん mailto:sage [2024/12/11(水) 23:49:27.18 ID:9ebR4E1i.net]
- 俺ってスゲー
- 767 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 05:18:25.46 ID:2xpeWo94.net]
- こいつ数学板に連日粘着してるキチガイな
- 768 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 07:40:20.49 ID:rgUDNRxT.net]
- 自己紹介乙
- 769 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 15:59:32.60 ID:rgUDNRxT.net]
- >>654
少数の表現を知らない素人
- 770 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 17:39:01.48 ID:rgUDNRxT.net]
- 数値計算の立場からすると・・・で無理だな
- 771 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 17:39:21.03 ID:rgUDNRxT.net]
- 解散
- 772 名前：デフォルトの名無しさん [2024/12/12(木) 18:55:56.72 ID:JJ7UILYB.net]
- >>761
じゃあ、正しく少数を表現できるコードをどうぞ。
前回の人は>685-686などというコードで信用無くした。
- 773 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 19:13:14.19 ID:rgUDNRxT.net]
- ポエム爺
- 774 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 19:23:46.43 ID:382kTtAh.net]
- >>764
アホすぎ
- 775 名前：デフォルトの名無しさん mailto:sage [2024/12/12(木) 19:33:03.74 ID:rgUDNRxT.net]
- 空のバケツほどよく鳴る
- 776 名前：デフォルトの名無しさん mailto:sage [2024/12/13(金) 00:47:18.68 ID:HhuErboB.net]
- Ωをプログラムの表現しうる全データの集合
fを関数とするとf∈Ω
しかし、ΩからΩへの関数の集合の濃度はΩよりも大きいから矛盾
どういうことだ
- 777 名前：デフォルトの名無しさん mailto:sage [2024/12/13(金) 01:09:14.09 ID:zE9P8o7z.net]
- >>768
表示的意味論かよ。
- 778 名前：デフォルトの名無しさん mailto:sage [2024/12/13(金) 01:54:27.10 ID:XDI5kMlm.net]
- ゲーデルの不完全性を解けば人類は理論上次の次元に到達する
このスレの内容はちょっとだけ掠っているのでその調子でがんばって下さいね
- 779 名前：デフォルトの名無しさん [2024/12/13(金) 13:20:29.60 ID:ouGUX1+B.net]
- ゲバ本とゲバ棒を聴き間違えたことはある
- 780 名前：デフォルトの名無しさん mailto:sage [2024/12/13(金) 14:28:15.71 ID:eXnQCWqo.net]
- 予言者
リーマン予想を解けば人類は理論上次の次元に到達する
- 781 名前：デフォルトの名無しさん mailto:sage [2024/12/13(金) 15:19:13.43 ID:eXnQCWqo.net]
- そういえばπの定義は微妙なので>>742の証明は形式的なものに過ぎない可能性がある
- 782 名前：デフォルトの名無しさん mailto:sage [2024/12/13(金) 23:05:29.33 ID:eXnQCWqo.net]
- >>762
任意精度数値計算ライブラリ
メモリに依存するみたいだけど
- 783 名前：デフォルトの名無しさん mailto:sage [2024/12/14(土) 14:08:54.29 ID:jFwYZGRF.net]
- 言語論とか役に立たないからな
ソフトウェア工学学んだほうが役に立つよ
- 784 名前：デフォルトの名無しさん mailto:sage [2024/12/14(土) 16:08:00.44 ID:yzVhe68F.net]
- 計算可能実数というのがあってπは扱えるけど実数全体は無理
- 785 名前：デフォルトの名無しさん mailto:sage [2024/12/14(土) 17:28:54.01 ID:yzVhe68F.net]
- 終了
- 786 名前：デフォルトの名無しさん [2024/12/27(金) 06:43:26.62 ID:3cQLuAQG.net]
- 球面上で風や海流などの分布を考えると、かならず流れが無い点Pが存在する
このことから、たとえば浮き輪の表面のようなハンドルのある曲面を球面座標でパラメータ付けできないことなどが分かる
数学では上のような性質をみたす点Pを具体的に構成せずに扱えるし、Pの性質だけから後者の命題を導くことも可能
こういうことが実用レベルでできるプログラミング言語は現状無い
- 787 名前：デフォルトの名無しさん [2024/12/27(金) 06:48:54.79 ID:3cQLuAQG.net]
- 縮小写像はかならず不動点をもつ
このことから線形微分方程式の解の存在が言える
非自明な解を一個とってくるだけなら数値解析をする必要はない
- 788 名前：デフォルトの名無しさん [2024/12/27(金) 06:55:54.24 ID:jx54xMU+.net]
- テンソル積、射影加群、入射加群、逆極限、順極限、……などはすべて普遍性で特徴づけられる
つまり、集合として具体的に構成をしなくても、他のすべての対象に対して射がみたす性質で一意的に定まる
しかも、これらのほとんどの議論は具体的構成を使わず、普遍性だけから従う
このような議論をするには、すべての加群のあつまりのような、無限集合にすらならない膨大な概念を考える必要がある
当然、構成に頼っていてはこのような概念をプログラミングで扱うことは不可能
- 789 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 07:32:04.93 ID:dJ9yt+4u.net]
- 不動点定理は不動点を持たない関数(特に否定演算)がある領域では成り立たないよね。
不動点定理を前提にするのは「コンピュータの扱いやすい領域のみ扱う」と言っているようなものかと。
- 790 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 07:49:18.68 ID:hlvzD05r.net]
- >>781
それは不動点定理ではない
- 791 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 07:50:43.08 ID:hlvzD05r.net]
- 掛け算の可換性は非可換群では成り立たないよねとか当たり前のことを言ってるようなもん
馬鹿丸出し
- 792 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 15:58:43.91 ID:qzYOmgeu.net]
- 爺のポエムは不変
- 793 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 18:06:53.40 ID:gyqBnIsN.net]
- 数学とプログラミングを対立構造で見てる時点で何もわかってない
- 794 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 18:46:23.72 ID:jSY0DGfh.net]
- >>785
具体的にどのレスを指して「数学とプログラミングを対立構造で見てる」と言ってる？
ただの独り言？ならごめん。
- 795 名前：デフォルトの名無しさん mailto:sage [2024/12/27(金) 23:43:23.45 ID:QY/IdYVY.net]
- 単一継承ならせいぜい親と子の対立しかない
多重継承なら親と親の対立もありえる
ドメインとドメインの対立
- 796 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 17:37:12.88 ID:1/gaPmQa.net]
- 命題⇔型
理論⇔ライブラリ
- 797 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 17:42:01.70 ID:0n60WVz7.net]
- 物理とプログラミングは対立構造か
- 798 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 17:51:31.87 ID:R/JuY1We.net]
- 言葉に酔ってるだけだろ
- 799 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 18:41:16.54 ID:1/gaPmQa.net]
- 自分が理解できないからと言って難癖をつけるのはやめましょう
- 800 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 19:34:52.40 ID:0n60WVz7.net]
- 国語を勉強してくれ
- 801 名前：デフォルトの名無しさん mailto:sage [2024/12/29(日) 23:31:21.70 ID:Ettja4KR.net]
- 正しい言葉遣いをしたら綺麗事しか言わなくなると思うよ
オールドメディアを超越することと可読性は両立しない
- 802 名前：デフォルトの名無しさん mailto:sage [2024/12/30(月) 06:05:18.87 ID:AFoxKaw/.net]
- オールドメディアガー
- 803 名前：デフォルトの名無しさん mailto:sage [2024/12/30(月) 07:54:23.09 ID:AFoxKaw/.net]
- SNSで炎上商売
- 804 名前：デフォルトの名無しさん mailto:sage [2024/12/30(月) 23:30:57.09 ID:djpp6m1u.net]
- 商売なら買い手に責任がある
商品や作品の側に罪はないという理屈で変な物が作られる
買い手の方は責任を果たすために優れた物を買い、自然淘汰されるべき物には不買運動をする
- 805 名前：デフォルトの名無しさん [2025/01/09(木) 12:47:55.94 ID:iZ6OsWgm.net]
- 炎上商売にエンジョイ
- 806 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 02:01:35.37 ID:8Ab7i+tr.net]
- 型に対してプログラミングすべき
- 807 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 07:50:15.14 ID:aNPLoHWH.net]
- それやってもすぐ人間の能力限界にぶつかるから
- 808 名前：デフォルトの名無しさん [2025/01/12(日) 10:12:06.95 ID:l8rSJlAD.net]
- バリアントで統一
- 809 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 10:51:45.53 ID:iqj2UdGG.net]
- 空手型
- 810 名前：デフォルトの名無しさん [2025/01/12(日) 15:49:20.69 ID:DO5vWwuf.net]
- 科学をプログラミングするのは難しいが
プログラミングを科学するのは可能では？
- 811 名前：デフォルトの名無しさん mailto:sage [2025/01/12(日) 16:35:24.05 ID:iqj2UdGG.net]
- 主語がでかい
- 812 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 02:34:19.05 ID:scTw5na7.net]
- オブジェクト指向って、コンピュータサイエンスじゃないんだよな
単に（一部の）人間にとって理解しやすくモジュール化しようってだけのことで、それで技術的に出来ることが増えるわけじゃないから
- 813 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 02:37:56.75 ID:scTw5na7.net]
- 構造化プログラミングや、関数プログラミングは、それ以前より高レベルの抽象化をもたらしたけど、オブジェクト指向は単に書き方の問題
科学論文で例えれば、構造化プログラミングや関数プログラミングは理論の内容に相当するが、オブジェクト指向は論文の体裁のこと
- 814 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 02:40:56.25 ID:XXChvl3U.net]
- そして、科学論文の体裁は重要だが、オブジェクト指向はいまや重要ではない
- 815 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 05:24:15.88 ID:elRKgauc.net]
- 型
並行性
最適化
この3つだよ
今求められてんのは
- 816 名前：デフォルトの名無しさん [2025/01/13(月) 09:04:54.93 ID:PzkYuqRH.net]
- 求めてないよ
- 817 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:12:00.23 ID:J7wtrzSF.net]
- 俺が大学生だった20年前はオブジェクト指向もCSの一部だったが
教授はカプセル化が一番重要だといってた
研究はされてたけど、アスペクト指向は流行らなかったなー
- 818 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:12:18.64 ID:6+/RYvQh.net]
- で、出ｗｗｗｗインターネットあまのじゃく君ｗｗｗｗｗｗｗ
- 819 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:13:20.48 ID:wtvPYUbh.net]
- >>809
君、勉強できなそうだね
- 820 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 09:42:56.67 ID:94WYo5Du.net]
- >>809
たった三行でここまで頭悪そうな文章書けるのってある意味才能だな
- 821 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 10:20:57.19 ID:Ymx2LteG.net]
- オブジェクト志向の次はデザインパターンだろ
- 822 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 10:42:06.79 ID:LSOaiCCa.net]
- カプセル化も全否定されてるけど
いまだにアンダースコアの変数はモヤモヤする
- 823 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 10:43:00.59 ID:P3ktA6B0.net]
- それも宗教
振り子が逆に振れてるだけ
- 824 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 11:39:54.56 ID:J7wtrzSF.net]
- デザインパターン20数個のうち10数個ぐらいはただの高階関数でかけるという研究もある
- 825 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 11:55:37.97 ID:Ymx2LteG.net]
- 魔法はなかった
- 826 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 13:02:05.46 ID:DTY38xVU.net]
- >>816
そして残りの10個はただのアンチパターン
- 827 名前：デフォルトの名無しさん mailto:sage [2025/01/13(月) 17:18:23.47 ID:Ymx2LteG.net]
- 岩波講座 ソフトウェア科学 [基礎]1
計算システム入門
著者 所真理雄 著
刊行日 1988/10/06
ソフトウェアの作成は人間的な作業で，信頼性や生産性の点でいまだに手工業の域にある．こうした現状をふまえ，ソフトウェア作成の方法を示すとともに，その理論と知識を整理し，新しい学問体系として提示する
- 828 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 00:54:16.56 ID:eoA7bUR4.net]
- なぜ高階関数を使わないのか
εδ論法はなぜεの関数を具体的に構成しないのか
こういうのを体系的に整理したら特定の勢力だけが得をして他は損するんじゃないか
だから整理しない
- 829 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 08:02:07.96 ID:WvheYWow.net]
- Foo = Bar | Baz
- 830 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 08:15:31.11 ID:BEZztBwJ.net]
- 型⊂クロージャ
- 831 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 12:10:31.19 ID:ygjj3afU.net]
- 型なんて特別なものじゃない
0や1はInt型のオブジェクト、IntはType型のオブジェクト
- 832 名前：デフォルトの名無しさん [2025/01/14(火) 12:50:51.03 ID:1hGtsoWq.net]
- 水の呼吸、壱の型
- 833 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 13:27:13.44 ID:2ZQOZttA.net]
- >>824
咄嗟にアニメの話出せるとか
おまえすげえ最先端行ってるな
才能の塊かよ
- 834 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 13:30:47.33 ID:5ok8hMJ2.net]
- >>824
それ知ってるわ
煉獄さんの映画のやつだろ
お前マジでおもしれーな
- 835 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 13:58:17.70 ID:L1ZxvYgu.net]
- 型が第一級オブジェクトなら、クロージャを使えば状態つきの型を作れるわけか
- 836 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 14:18:33.81 ID:x8Aql6YT.net]
- 有理数型や小数型も作れるのか？
- 837 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 14:29:34.08 ID:S4iOQtDV.net]
- >>827
わざわざ型情報を実行時に変化させてどうすんだ
- 838 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 14:29:54.43 ID:S4iOQtDV.net]
- >>828
お前は低レベルすぎ
- 839 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 20:10:44.55 ID:6b3bLxyH.net]
- 有理数型はHaskellやMathematicaにもうある
状態付きの型、考えただけで恐ろしい
- 840 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 20:32:44.91 ID:A8xCzIhU.net]
- そうやって進化していくものよ
- 841 名前：デフォルトの名無しさん mailto:sage [2025/01/14(火) 21:00:24.45 ID:6b3bLxyH.net]
- 状態付きの計算を行う手順を持った型なら純粋だから許せるけど
状態付きの型なんていらないよ
|
 |
