72(4): デフォルトの名無しさん [sage] 2024/03/23(土) 14:11:05.89 ID:O64Y227M(2/5) AAS
>>70
普通mapは配列に対してではなく
もっと一般的にイテレータに対して適用
結果もイテレータとする

その結果を例えばfor文で使う場合
わざわざ結果を配列に入れても無意味だったことになるからだ
mapを多段にした使った場合も同様で中間結果配列は無意味になる
だからmapの入力も出力もイテレータが使われる

230(5): デフォルトの名無しさん [sage] 2024/04/12(金) 11:00:23.24 ID:n/WEiCkF(1/5) AAS
厳密に求められないからπという記号を用いたわけで
コンピュータで扱う場合はπという記号定数を使えばいいだけ
無限に続くので3.14...を厳密に求めることはできないのは数学もコンピュータも一緒
1がしたいことが何なのかよくわからん

306(4): デフォルトの名無しさん [sage] 2024/04/15(月) 12:44:15.61 ID:scEUff9F(4/17) AAS
>>305
だから存在をどうやって示すんだ

308(2): デフォルトの名無しさん [] 2024/04/15(月) 14:37:35.85 ID:ANhhwFml(5/5) AAS
>>306
微分積分の教科書読めよ

345(1): デフォルトの名無しさん [sage] 2024/04/16(火) 17:35:24.46 ID:Ng40HiX6(4/5) AAS
カリー・ハワード対応 (Curry-Howard correspondence) は、数学と計算理論の分野で重要な関係性を表す概念です。この対応は、論理学と型理論の間の深い関連を示しています。

カリー・ハワード対応は、次のような三つの分野間の関係を表しています。

1. 論理学: 論理的な命題や証明体系
2. 型理論: プログラミング言語や計算の型システム
3. 圏論: 数学的構造を研究する分野

これらの分野の対応関係は次のようになります。

1. 論理学の命題や証明は、型理論の型とプログラムに対応する。
2. 論理学の証明の形式は、型理論のプログラムの構造に対応する。
3. 圏論における対象や射は、型理論における型や関数と対応する。

この対応関係は、論理学の証明とプログラミング言語のプログラムの間に類似性があり、その間の数学的な形式的関係を示しています。これは、プログラムの正しさや証明の正当性を検証するための形式手法に関連しており、特に依存型や型理論に基づく証明支援系で重要な役割を果たしています。

346(1): デフォルトの名無しさん [sage] 2024/04/16(火) 18:01:37.43 ID:fFCD5orj(1/2) AAS
n乗根のアルゴリズムは選択公理みたいに解の集合から一つ選択するんだよね
ここで空集合と空でない集合という、なんというか
反なめらか勢力？

340(7): デフォルトの名無しさん [sage] 2024/04/16(火) 16:09:15.10 ID:X3z51ZSN(1) AAS
>>337,339
そんなことより、これを大学数学初年度の回答レベルで解いてみてよ
画像ﾘﾝｸ

1(16): デフォルトの名無しさん [] 2024/03/16(土) 19:41:45.98 ID:nuwGv9us(1) AAS
たとえば、プログラミングで

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

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

596(5): デフォルトの名無しさん [sage] 2024/11/12(火) 04:10:14.19 ID:15KCzjek(2/5) AAS
x^2 = 2をみたす正の実数xは一意的に存在する
なら、それを√2というシンボルで扱えるようにすべきだ
計算は必要なときにだけすればいい
x = 1.4142云々という数値にしなければ扱えないのは不要な制約

これは誤差があるとかそういう問題ではない
人間の思考をコンピュータの都合に合わせようとしているのが問題