◎正当な理由による書き込みの削除について： 生島英之 とみられる方へ:「数学」をプログラミングするには YouTube動画>1本 ->画像>1枚
動画、画像抽出 ｜｜
この掲示板へ
類似スレ
掲示板一覧 人気スレ 動画人気順
このスレへの固定リンク： http://5chb.net/r/tech/1710585705/ ヒント： 5chスレのurlに http ://xxxx.5chb .net/xxxx のようにb を入れるだけでここでスレ保存、閲覧できます。
たとえば、プログラミングで
>>1 証明を記述するための言語がある。CoqとかAgdaとか
あと単発質問はスレを立てるまでもない質問スレでどうぞ
>>1 アルゴリズムではなくメモリ容量の問題
無限小数を求めるには無限のメモリが必要で世界中のメモリを集めても無限にはならないので不可能なだけ
>>3 この問題解くのに無限小数計算してる奴なんかおらんわ（笑）
数学をプログラミングする方法は、使用するプログラミング言語によって異なりますが、一般的なアプローチは次の通りです。
ランベルト関数(近似精度がヤヴァくてもヨシ)
基礎論以外の命題の証明を証明支援系で一から書くのは現実的ではないから、既存の有名命題がライブラリとして使えるような処理系を使うことになるんだろう
証明支援系で証明を書いても、それを再利用してべつの定理を自動で証明できるわけでもないし、ソフトウェアとして全く無意味だよね……
証明支援系を使うことで未知の証明ができたり、数学の問題がよくわかったりするわけじゃなくて、
証明支援系が役に立たないなら、そもそも数学で証明を与えることにどういう意味があるのか考えてしまう
厳密だが根拠がない等式を、厳密ではないが根拠のある不等式の集まりにすりかえる
数==数では背理法が使いにくいが
読まなくても分かることをほぼ知り尽くしてから読めば楽に読める
∫_0^1 dx/(1 + x^2) = Arctan(1) - Arctan(0) = π/4
あとArctanのテイラー展開
積分変数を別名に変えても積分の結果が変わらないこと
>>4 そしてあんたはプログラムができない
永久にすれ違いだなｗ
>>5 実際に計算しない限りプログラムの世界では完成したとは言えない
できたような気になってるだけだｗ
変数に別の変数 (を含む式) を代入するのは嫌なので、右辺を実際に計算してしまった値を代入する
コード書けない奴が必死に妄想でレスバするクソスレ
しかし、何も書かないより悪いコードを書く方がマシみたいな保証が
数学を記述するには一階述語論理があれば十分
○○を支援する言語と○○が可能な言語を分断するパラダイムはたしかにオワコンだ
>2 の紹介しているCoqとか、純粋関数型言語HaskellもPCで動く数学って感じではあるけども、そもそもメモリが有限なので連続を表現できない。
leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか？
ほんとうに教科書に載ってる定理の証明がぜんぶ正しく書かれてるなら、それは教科書読んでるのと同じわけだし
lean4はプログラミング言語としても、haskellやrustくらいパワフルな言語なので、cだのfortranだの勉強するよりプログラミングの勉強にもなる
>>29 推論規則にしたがって項を削除したり、条件をみたす要素を深さ優先探索したり
証明支援系っつっても、ふつうにプログラム書くのと同じで、特定の問題の解法をプログラムしてるだけ
証明支援系Lean4
>>36 「プログラミングの勉強」を「プログラム言語」の勉強だと思ってるバカ
「program」の意味を調べてみろ。言語はただの手法の一つ
>>36 CやFortranの評価が低いということはHaskellの中でモナドの評価が低いよね
それはもったいないから言語を競争させる原理はよくない
ミサイルでも撃たれたならともかく
スレタイが悪い
>>33 すでに解けてる問題を特定の処理系の言語に書き直すのが一大プロジェクトというのがくだらないと思う
>>50 すでに常識になっていることを「先入観にとらわれている」と思う人はいる
先入観をリセットしてやり直したい需要は多少はある
>>52 馬鹿すぎて話にならない
わざとやってるならむしろお笑い番組の脚本とか考えるセンスあると思うよ
わざと馬鹿になったのではないが
現代数学は集合と写像の言葉で書かれている
>>56 それは違う
数学ができるプログラミング言語のコンパイラをCで書くことができる
そもそもすべてのプログラム言語はチューリング完全だからCで書けてハスケルに書けないなどということは無い
>>56 それ逆だね
mapは関数型言語で登場した
そのRubyやPythonといったスクリプト言語は後からそれを導入した
マップは関数の集合直積に過ぎない
>>60 跡から登場したってことはRubyやPythonのほうが優れているってことやろが
まともなプログラマーがスクリプト言語でプログラミング開発することはない
CやPYTONはスクリプト言語だから単純なことしかできない
スレタイ
数学に副作用はないがモナドは副作用があるのでハスケルでは数学はできない
>>56 Cでは関数の引数として関数ポインタを渡せるから、map関数を簡単に自作できる。
空論、絵に描いた餅、機械語にだってできるだろｗｗｗ
>>69 機械語に識別子はないからできないだろ。Cでは長さnの配列aの各要素に関数fを適用した結果を
配列bに格納する関数 map(f, a, n, b) を簡単に自作できる。
>>70 普通mapは配列に対してではなく
もっと一般的にイテレータに対して適用
結果もイテレータとする
その結果を例えばfor文で使う場合
わざわざ結果を配列に入れても無意味だったことになるからだ
mapを多段にした使った場合も同様で中間結果配列は無意味になる
だからmapの入力も出力もイテレータが使われる
>>72 それは実装上の効率化のための操作で、本当の写像ではない。本当の写像は配列から配列を作る。
C#で言えばSelectしただけでは写像にならず、ToArrayしないと写像にならない。
>>73 配列から配列なんて嘘つきだな
例えば写像の入力を数学でもよくある自然数とする
これは配列では表現できない
イテレータならば表現できる
出力も同様で配列は不可能だがイテレータなら可能
>>74 自然数は要素数が無限大の配列だが、コンピュータではメモリが有限なので表現できないだけ。
イタレータによる遅延評価は問題を先送りしただけで、本当の写像である配列を作ろうとすると
メモリが途中で尽きて作れない。
>>76 配列なんていう間違った考えをするからそのように失敗する
正しくイテレータと捉えれば自然数もそこからの写像も扱える
>>77 イタレータは配列の各要素を走査しながら操作する道具、つまり写像を逐次的に作っていくための操作手順を表したものに過ぎない。
>>78 イテレータとは何かを学び直しなさい
それは配列に対するイテレータ
イテレータに配列なんていうものは必要ない
イテレータなんぞプログラミング側の都合でしかないやろｗ
配列こそプログラミングやコンピュータ都合の邪道なものだね
>>78 >>81 イタレータの意味を分かっているのか。反復子だぞ。反復子が写像のわけないだろ。
写像を実行するための操作手順でしかない。
反復子の遅延評価により無限の操作手順をコードとして書くことはできても、実際には
実行が途中で終わるので無限を扱えるわけではなく、有限を無限に見せている構文上の
まやかしに過ぎない。
>>82 あんさんボケとるな
ここまで読んで反復子(iterator)が写像(map)と書いているのは君しかいない
他の人たちは以下を正しく理解して書込みしている
>>72 >> だからmapの入力も出力もイテレータが使われる
>>83 >>74 はごっちゃにしているようだが。
反復子を使っても遅延評価をしなければ、mapを多段に使った場合の効率は良くならない。
例えば、C++ STLのtransformがそう。
>>70 のような配列のmap関数でも、引数fとして複数の関数の合成関数のポインタを渡せば、
効率は良くなる。あるいは、引数fとして関数ポインタの配列を受け入れるようなmap関数を
書いても良い。
>>83 >>74 はごっちゃにしているようだが。
反復子を使っても遅延評価をしなければ、mapを多段に使った場合の効率は良くならない。
例えば、C++ STLのtransformがそう。
>>70 のような配列のmap関数でも、引数fとして複数の関数の合成関数のポインタを渡せば、
効率は良くなる。あるいは、引数fとして関数ポインタの配列を受け入れるようなmap関数を
書いても良い。
そもそもCでmap関数を書けるかという話だから、書けるという回答で何の問題ないだろ。
>>84 根本的な勘違いをしているようなのでアドバイス
イテレータは抽象的な概念に過ぎないのでそこに遅延評価などという話は一切出てこない
イテレータの実装の一つに遅延評価の有無を持ち出すケースがあるようだがそんな特殊などうでもいい話をしても意味がない
>>86 そんなことは分かっている。
>>72 に言ってくれ。
iteratorは可算無限を扱える
mapは入力も出力もiterator
例えば
2倍にするというmapに対して
入力を自然数のiteratorとすると
出力は偶数の自然数のiteratorとなる
これだけの話だろ
>>82 の人だけ理解できてないようだが
それは間違い
集合論はラッセルのパラドックスで矛盾した
プログラム言語は機械語→アセンブラ→高級言語 と進化してきたが、高級言語にも高級度の段階があって
まったくトンチンカンな話してんな
>>95 それはarrayを入出力とするmapだね
それは遅延評価もできず可算無限列を扱えない古い劣化タイプ
一方でiteratorを入出力とするmapはarrayだけでなく可算無限列など任意のものを対象にできる
この完全なデタラメな話をここまで長々とする気力がどこから湧いてくるのかがわからない
>>97 昔は配列に対するmapしか無かったから、遅延評価できず、有限列しか扱えず、中間生成配列のムダなど、悲惨だったな
今はイテレータに対してmapその他を適用するプログラミング言語が増えたので、扱える対象が広がるとともに、効率も良くなったな
そもそも高階関数のmapは、数学の集合論における写像のことではない
ゴミみたいな話しかしてないな、定理証明系とかの話をしているのかと思ったら
>>97 >> 100 Visual Stduioで y = 2 * x + 1 の行の逆アセンブリを見てみると、
インタプリタのRubyや、配列っぽく見える[1, 2, 3]がリンクリストのHaskellが効率を
>>105 の訂正
(誤) for (i = 1; i <= 3; i++) y[i] = 2 * x[i] + 3;
(正) for (i = 1; i <= 3; i++) y[i] = 2 * x[i] + 1;
>>104 固定長の配列を入力に使っている時点で失格
このスレは
>>1 の例のように対象は可算無限列
静的な固定長で最適化できるのは当たり前だから
>>108 無限なんて実行不可能なものを構文として書けても、コメントとして書けるのと同じようなもので無意味。
>>109 何を頓珍漢なことを言ってるんだよ。
for (i = 1; i <= 3; i++) y[i] = 2 * x[i] + 1; が
for (i = 1; i <= n; i++) y[i] = 2 * x[i] + 1; に変わるだけだぞ。
入力対象は
>>1 の数列でいいんじゃね
1
1 - 1/3
1 - 1/3 + 1/5
1 - 1/3 + 1/5 - 1/7
1 - 1/3 + 1/5 - 1/7 + ...
もちろん何番目まで必要かは不明
この数列を他と切り離して記述できるかどうか
しょうもない算法や文法を力説されても
集合論はラッセルのパラドックスがあるからまちがい
集合は悪くないがそれを内包表記で定義するのが悪い
Pythonには内包表記はあっても外延表記はないから集合論はできないよ
>>104 はVisual Studioでは最適化オプションがなぜか無視されてしまうが、コマンドライン
コンパイラではまさに
>>109 が言う要素数が固定かつ全要素がコンパイル時に計算可能という
特殊な場合に応じた最適化が施され、コンパイル時の計算結果を配列yに書き込むだけで
y = 2 * x を全く計算しないコードが生成されることが、アセンブリ出力から分かる。
IFORT (旧式Intel Fortran) では
mov eax, 3
(中略)
mov DWORD PTR [TEST$X.0.1], 1
mov DWORD PTR [TEST$X.0.1 + 4], 2
mov DWORD PTR [TEST$X.0.1 + 8], eax
mov DWORD PTR [TEST$Y.0.1], eax
mov DWORD PTR [TEST$Y.0.1 + 4], 5
mov DWORD PTR [TEST$Y.0.1 + 8], 7
というコードが生成され、Cの
int t = 3;
*x = 1; *(int *)((char *)x + 4) = 2; *(int *)((char *)x + 8) = t;
*y = t; *(int *)((char *)y + 4) = 5; *(int *)((char *)x + 8) = 7;
に相当する処理になる (CではC流に添字0～2を使うとして)。xとyに共通する
要素3はレジスタに入れて使い回される。一度も使われない変数xを除去する
最適化はされない。
IFX (新式Intel Fortran) では
rustのほうがスゲーからfortranは黙っとれ
フォートランは行列、有限要素法のライブラリィ呼ぶだけ、独自のコードなんか書かないｗ
数学をプログラミングするには、プログラマが数学の必要があるのでは？
ギャンブルなら敗者が金を振り込めば秩序が戻るのだが
>>117 圏論型と言えるか分らんが、圏論が注目されたのは副作用の問題を圏論のモナドで表現できるということでHaskellに採用されたのがきっかけっぽい。
今は非可換確率論を圏論で表現すれば意識がどうやって生まれるのかの研究に使えるって話がある。
意識が生まれる謎が解ければAIに意識を持たせられる。
戻らないだろ、刑務所行き
コンプライアンス的には絶対に違反しないブレないスタイルの方が楽だな
>>126 ガイジか？
プログラマ→職業
数学→学問分野
日本語勉強し直すか死ねよ
きっちりした仕様決め無しで「プログラミング」できるわけないだろうに
ラッセルは作る人というより脆弱性を発見する人のように見える
意識は非可換だってどこかで聞いたな
借金取りは見かけ上は極めて非決定的にふるまうが
ポエマーさんはポエム板にでも行けよ
ゲーデルの不完全性定理で完全に否定されているだろ
不完全ではなく無定義語で挫折する人がいる
>>149 ガイジか？
ゲーデルの不完全性定理はそんなことについて言及してないぞ
数列の概念がない奴でも無限級数の意味は分かるんだよね
↑
言語に依存しない数学的オブジェクトの存在が保証されれば
「プログラム技術」板で「数学」がどうのこうの語ってるのがもう頭悪いというか頭おかしい
>>154 数学と物理はなんの関係もないぞ
数学ってZF(C)公理系を絶対ルールとするパズルゲームでしかないから
絶対にルール追加しないのは
馬鹿参上
ただし
>>160 は支持するぞ
公理系を何にするかは議論があるだろうが推論パズルゲームってところは正しい
プログラム組めない雑魚ほどなにか深遠そうな理論めいたものを言おうとするよな
学があったらポエム書かんやろｗ
バブルソートで長さnのリストがソート済みになることをnに関する数学的帰納法で示すコードを書いて下さい
構成論理でしかない帰納法は逃げ
数学一般をプログラムするのはきつそうだけど、
>>1 の内容くらいならMathematicaとかでできるのでは
iterableがソート済みならばfilter(function,iterable)もソート済みである
>>171 プログラム技術と全く関係ないの、わかる？
単語だけ知ってても意味ないのよ
べき集合の濃度がもとの集合よりも真に大きいことを対角線論法で示すプログラムを書いて下さい
ゲーデルの不完全性定理とかプログラミングに関係ないぞ
計算機科学的には背理法はプログラミングでの継続に相当するものだと判明している
計算機に記号処理での証明は荷が重いやん
訂正((A->B)->A)->A)だった
ポストモダンも用語の雰囲気だけで数学や物理の用語を援用して失敗したけど，同じことを繰り返したいのかな
うん。必ずしも泥棒が悪いとはお地蔵様も言わなかった。
>>182 そう、λμな
でも対応があるだけで実用性はないよな
ム板にバカが書き込むのは今に始まったことじゃないが、意味不明な戯言書き込みに来る奴がすごく多くなった
>>189 不満なら見なきゃいいだろ
インターネットしか居場所ないのか？w
スウ学をプログラミングするのは、簡単そうぢゃーーーん
嫌なら見るな，は反論になってないな
>>191 不完全性定理をわかってないなら無理にそんな意味不明なこと書かなくていいよ
>>192 正当化は2種類
行動に個性があればもし失敗しても同じ失敗が集団的に繰り返される心配がないのと
もう一つは、目には目を歯には歯をみたいな相手と同じことを繰り返せばOKと思ってるやつ
>>162 >>164 その場合はコンピュータじゃなくて理論計算機科学とかだな、比較対象がおかしい。
数学史とか数学基礎論とか少しでもなんか読んでみ、今の数学はそういう思想だから
その調子じゃヒルベルトプログラムもブルバキも何にも知らないだろ
>>180 いやあるだろ…停止性問題とか知らないの…？
こんなん数学科でもなくてもCS学科でもなくても
趣味でWikipedia読んでれば知れる雑学だぞ
>>173 背理法って推論規則の一つでしかないから他の推論規則を使って導けるものじゃないんじゃないの
証明をプログラミングでやるって、命題論理の変換で真か偽になる変換方法の組み合わせを見つけるってことでしょ
人間がなかなか納得しがたいロジックでもプログラミングしたらはっきりする、わけじゃなくて、
なかなか納得しがたいロジックでも間違いがなければ論理に間違いはないので証明されたとする、という根本は変わらなくて
論理の変換をプログラムで行なえても不思議ではないと思うけどな
記号論理学を大学1年のときにとったけどそれぐらいの基礎すらなかったら証明、公理系、推論規則、あたりの概念がめちゃくちゃになってるんじゃないか？
完全性、健全性の意味をしらんのだな
身体性という言葉の悪いところは
数式ゴリゴリのデジタルフィルターなんか、プログラムで書くと、あぁそういう事かと理解が速いよね。
罵り愛が一段落下っぽいね。
「数学をプログラミングする」というのを「量子化しない」という意味だと思ってるのが、学がなさすぎる
とりあえずHelloWorldから一歩でも先に進んでからこの板に書き込めよ
そうなん？
printf("数学をプログラミングする\n");
数学一般を広く浅くプログラミングできない
>>208 だから、>1への回答をお願いします。
その不完全性定理とか流し読みだからうろ覚えだけど、
ある数学モデルの無矛盾性をその数学モデルは証明できないとか？だっけ？
数学そのものの不完全さを証明したもので、「「数学」をプログラミングする」の
証明ではない気がするんだけど…。
物理的な不可能の証明として無限や連続性を上げるのは妥当だと思うのだが、
あなたは違うと言う。
なら、あなたは私の代わりに証明する義務があるのでは？
プログラムってバカでもできるけど、間違いを指摘されて認めることもできないキチガイは入り口にも入ってこれてないよ
数式を計算するプログラムって逆ハンガリアン記法でスタックに積んで取り出すの？
数学をプログラミングと聞いて電卓が頭に浮かぶのか
このスレはポスト オブジェクト指向はオワコンのスレって感じがする
オブジェクト指向はもっと柔軟性を高めて欲しいわ。
C++の具体的な問題を目で盗めばRustを作れるが
たしかに、お金でも賭ければその限界が具現化するけど
不完全性定理は公理的集合論から証明できないならPythonとかJavaには欠陥があるってことじゃん
厳密に求められないからπという記号を用いたわけで
>>230 「数学をプログラミングするには」って書いてあるじゃん
#define final constant π;
>>230 > 厳密に求められないから
πは厳密に求まるが
1/3 = 0.33... は割り切れないから求まらないとか思ってる文系くんかな？（笑）
> πという記号定数を使えばいいだけ
>>230 君、国語力が低すぎて文章を理解できないから、
数学の教科書もなんとなくで読んで来たんでしょ？
学問に向いてないよ、君（笑）
>>230 で、こいつ次は、
「厳密にもとまらないというのは、10進数で有限桁で表せないという意味で言った」
とか言い訳するんだろうなあｗｗｗｗ
>>230 > 1がしたいことが何なのかよくわからん
問題意識を理解できないなら、わざわざいっちょかみすんな
わざわざいらんことして、おまけに無知まで晒してる
究極に恥ずかしいよお前（笑）
スレタイが読めないなら小学校の国語からやり直しｗｗｗ
モピロン、地球人の開発したAIには、無理
26点
そういや誰かがすべての言語はチューリング完全とか適当なことかいてたけど
チューリング完全は算法に関する性質
計算 + 証明 = 数学
命題 + 証明 = 数学
命題 + 証明
カリー・ハワードだろ
構成的論理ならきいたことはあるが構成論理ってなんだよ
>>1 > たとえば、プログラミングで
>
> π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
>
> を近似ではなく厳密に確かめるにはどうしたらいいの
> 人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど
人間が証明出来るからって、有限なアルゴリズムに書き換えられるとは限らないんだよなぁ…。
そもそも人間の証明がlimとか使って（仮に無限回繰り返せれば）極限はnになる（だろう）って感じで有限のアルゴリズムじゃない訳で。
>>260 とっくに解決した話題にいちいち間違った指摘をするのは面白いのか？
命題を実験すれば近似、証明すれば厳密
>>261 テキトーに読み飛ばしてた＾＾；
どのあたりで解決してたかアンカー教えて。
πは、プログラミングは、近年の地球人は、
現在のAIは何故か胴元になれないギャンブラーと同じ
>>265 うんうん。
罵られるのは甘んじて受け入れるので、解決したところのアンカー(>数字)を教えてください。
このスレで解決されたって意味ではないのでは?
>>260 の指摘なんて常識的なことだし
>>268 ○ 常識的
× 数学ができない人によくある勘違い
>>260 多分これって数列がある値に収束することを示すには無限に計算する以外に方法がないって思い込んでるのでは
人間が有限回のステップで証明できてる時点で有限のアルゴリズムだよ
>>260 まず「極限はnになる」の基礎となる理論から調べたら？
εδ論法は理解してる？
極限とは位相空間のある点の近傍にある番号から先の有向族が入ることである
帰納法とは順序集合においてある命題がある番号まで成立としたとき次の番号の命題が成立することである
>>270 うん…。
まあ、そもそも有限ステップで証明可能な事と、近似値ではない真の値を求めることを混同してる>1が悪いって事やね。
ε-δ論法で証明出来るのはいくらでも精度の高い近似値を求められる（それをもって極限の存在を証明）ってだけやし。
>>286 1/3 = 0.33...は無限につづくから真の値は求められないとか言ってるようなもん
小学生レベル
>>289 無理数はまさしく真の値は求められないだろ？
それこそスパコンで何兆桁求めたとかニュースになるけど、それでも近似値でしかない。
証明はあくまで存在を保証するだけ。
>>290 「コーシー列の極限」が実数なんだから、コーシー列を与えれば真の値になるだろ。
証明は数列が極限を持つことを示せば良く、数を無限に並べる必要は無い。
他責というか他人からもらった情報を丸暗記しなければいい
>>291 いあ、だから。それが真の値の存在を示してるだけって事だろ。
証明の厳密さが違うだけで、意味としては同じだ。
値のサイズが大きかろうが無限だろうがそれを指すポインタのサイズは小さい
>>294 同値判定(ついでに大小判定)できるんだから「存在だけ証明」じゃないだろ。
確かに四則演算は有理体で閉じていないけど、拡大体を考えれば問題ない。
>>296 それについては言い過ぎたと謝罪するけど、それって結局真の値は分からなくても√２って記号に押し込めれば順序比べられるし四則演算出来るってのと変わらない。
>1の求める近似値ではない厳密って何？って話になるが。
>>298 当たり前だろ。無理数は有理数じゃないんだから、有理数とは対応しない。
現代の数学は「実数=コーシー列の極限」で構築されているから、コーシー列が分かれば実数そのものとして扱うことができる。
>>299 実数の構成に5つぐらいある、切断とか。それに同値なものを同じものとみなすこともよくやる。
例えば実数は体、順序構造、連続性をもつものとして定義する
>>301 その存在示すのに、切断やコーシー列使うんやろ
>>306 >>308 微積というよりも解析だな。
>>306 > だから存在をどうやって示すんだ
こんな解析学の教科書の最初に書いてあることが分からずに実数論の講釈を垂れてた恥ずかしいやつ→ID:scEUff9F
>>315 証明できないのならどの本の何ページに証明が書いてあるのか教えてくれ
デデキント切断や完備化などが出てきても
横からだけど
>>317 は
理系の大学数学(所謂現代数学)における論理展開の流れや
存在の証明とされるパターンが分かってないから、かなりの独学なのかな
始めの内は簡単な教科書を(定理部分だけ)拾い読みするんじゃなくて
書いてある文章や定義、証明を精読しないと論理展開が抜け落ちて話が通じないよ
>>318 が書いてくれたか、任せた
存在論を厳密にやり過ぎるとクソどうでもいい心理学の信者が増える
Q = 有理数の全体
Qの切断C = (A, B)に対して、論理的には次の4つの可能性がある
Rの加法、乗法を
ただし
(仮定、前提、公理として)存在しているものから(公理的)集合論操作で構成したものは存在する、
>>301 >例えば実数は体、順序構造、連続性をもつものとして定義する
これは数論とか超準解析とか特定の用途でご都合定義や対比で採用(完備(非)アルキメデス順序体)する位で
well definedかどうかの議論は本来は必要だし
>>302 のツッコミが入るのは当然
>>320 >存在論
そう言うのが寄り付かないのが現代数学の良い所の1つかも
>>325 ご苦労さん、実数の公理があるだけなんで証明するものではない
ポエム連投しか能が無いのに、かっこつけで数学の話してみたら秒でボロが出るザコ（笑）
ま、何だな。近年の計算機ってさ内部2進数か稀に十進数
いずれ量子コンピュータの時代になるから
>>337 ,339
そんなことより、これを大学数学初年度の回答レベルで解いてみてよ
>>340 明らかに成り立たないし、そもそもnが定義されていなかったり問題として成り立ってない
カリー・ハワード対応 (Curry-Howard correspondence) は、数学と計算理論の分野で重要な関係性を表す概念です。この対応は、論理学と型理論の間の深い関連を示しています。
n乗根のアルゴリズムは選択公理みたいに解の集合から一つ選択するんだよね
>>345 ,346
そんなことより
>>340 の題意は伝わってるようだね
成立してるよ
カリー・ハワードって別にそれで何かブレイクスルーが起こったわけでもない
Pachinkoですった借金
ブレイクスルーのたびに歴史の断絶があるのは面倒だから
>>340 P(x) = x^2
f_1(x) = 0
[∀x∈R, P(x) ≥ 0]∧[P(x) ≠ (f_1(x))^2]
？
>>381 そこまで話が通じないとはw
ネタだろうけど出来損ないAIを真似た皮肉かなw
マジネタだったらそう言ってくれ、多少は補足するから
前提
Pは任意の実係数多項式で∀x∈R, P(x) ≥ 0を満たすもの
示すべき事
この時、ある自然数nと実係数多項式f_k(x)、k=1..nが存在して
>>340 の等式を満たすことが出来る
>>383 と
>>340 が数学の主張として異なるということが理解できないということ？
それとも、問題に不備があったことを素直に謝罪できない性格だということ？
奇数次ならかならず符号が逆転するので偶数次
平方完成で
>>388 ,389
問題自体は高校数学
大学レベルの隙の無い回答を求められているけど
妥協して高校基準でも
0点
∀x, P(x) ≥ 0なので、最高次の係数はかならず正
∀x, (x^2 + a)^2 - x^2 ≥ 0 となるようaをとってみる
問題に不備があったら出題も採点も自分でやればいい
P(x)は実数係数多項式で、∀x∈R, P(x) ≥ 0が成り立つとする。
二次式の場合は成り立つ
プログラミングしろよ
酒をのんだら、無意識に呼吸できなくなった
>>395 100点(最小値mは≧0なのはお目こぼしとして)
演習で板書すると100点でも理解度を確かめるために既知として良い所も
訊かれた経験あるかも知れないけど、例えば、この部分を噛み砕いて見てよ
>F(x)はF(x_0) = 0で、x = x_0で極小値をとるから、あるQ(x)が存在して
>F(x) = (x - x_0)^2 Q(x)
>となる。
(他にも最小値の存在を暗黙裡にしたらツッコミどころだった)
>>396 そこまでは知らない、
>>340 はユーチューブの拾い物なだけだから
VIDEO (そこでは別解がなされてる)
>>398 Lean4で回答してくれても良いよ
ある朝、男が牧場の近くを通った時、腕時計が壊れていることに気づきました。
In 1888, Hilbert showed that every non-negative homogeneous polynomial in n variables and degree 2d can be represented as sum of squares of other polynomials if and only if either (a) n = 2 or (b) 2d = 2 or (c) n = 3 and 2d = 4.
>>403 へー、勉強になるわ
今回のはhomogeneousにしてn=2の場合だね
任意の整数nに対し
上流は70点位の擬似コードを
商人なら主語を修正する
国際社会では日本はすっかり女性差別および児童ポルノ大国と見られている
>>411 網羅できない理由の方が多いのに何故できる方に賭けてしまうのかね
カリー・ハワード対応もそうだが
>>415 お前の首の上につけているものはなんだｗ
モビルスーツに手と足と頭があるのも網羅がしたいだけ
カリーハワード対応の元でも
「Haskellには依存型がない」は「Cにはclassがない」と同じ形式だし
依存型がなければ、その上に型システムを構築したらいいのでは？
やりたいことをやってる人は問題ないが必然的にこの道しかないみたいな考えはたいてい間違っている
型に複雑さ移動するだけで何も楽にならない
「道具」には役に立つとか楽になるための道具という意味がなくもない
ああっ、ナメクジみたいな篦が目の裏に浮かんでくる～っ！！
縁側と玄関の間に黒電話
サッポー「楡の木陰に高島さん」～ダンディな占い師伝説
物理をプログラミングって
その辺が、πを計算するのに近似値がどうのこうの言ってる連中の誤解かも知れんな
本体と付属品が別なのは当たり前だが問題は
>>454 圏論や型理論を記述言語にする
結局、数学を記述できる言語が必要
プログラミングをプログラミングするといえばlispだろ
ジェダイは可
同じ入力に対して常に同じ出力をかえすのが数学の関数だからコルーチンは邪道
なんか圏論が万能かのように語る雑魚ってかならずいるよな
∃.elim(h, (w) => ((hw) => q))
append (v: Vec t n) (w: Vec t m) : (Vec t (n + m)) :=
>>466 元の概念(マイクロスレッドとかファイバ)は関数とは独立かもしれんがコルーチンの実装は関数のようだぞ
pythonはジェネレーティブ関数とよび、c#のコルーチンも関数って書いてあった
>>467 1ミリも関係ないもの同士がじつは同型だったみたいな感じ？
何もしてないのに同型
lambdaはghost componentを扱えるからな
割り当てられたメモリの値を変更できる時点で数学はできない
プログラミングは数学もできるしアルゴリズムも書ける
自由すぎても強力とはいえないけどな
基本はIOモナドとSTモナドで副作用を扱える
モナドはListとMaybeをベースに理解しろとあれほど言ったのに
∧＿∧ ／￣￣￣￣￣
モナドは副作用の繋げ方を定義しているだけで、副作用を起こしているわけではない
OEISとか数学の数列をプログラミングしてるサイトだな
モジュラ計算はマルチコアに依存するからプログラミングではできない
マルチコアの処理をするコードもプログラミングの範疇だが
大きいモナドはお父さん 小さい緋鯉はコモナドたち 面白そうに双対してる
モンスターの位数は10^52ぐらいだから256ビット(10^77ぐらい)あれば表現できる
>>501 知ってても役に立たない知識を自慢げに披露してどや顔する馬鹿
>半単純リー代数の分類も知らぬザコめが
はじめに空間と場としよう
pを取ると
ここで疑問じゃ
なぜ、針の先端
種がわれた未来では
さて
まず、トリビアル
どこかに、綻び・縺れがあった
答えがわかれば
結論からいうとqは最大公約数的で全部の駅を合わせればいいんだな
なんか小難しいスレに迷い込んでしまった
>>522 まず、トリビアル
結論から言うと擬似的なストーリーに惑わされてやしないか？
惑いは現象であり物ではない
トリビアルさんがsageを覚えたようだ
エバQはあくまで共通部分だから中身スッカスカ
標準型は常に全関数だ
>>531 数学では様々な構成において、ある関係をみたすA1, A2, A3, ... を集めてくると、新たな対象Aが一意的に定まる、という形式のものがある。
これは普遍性と呼ばれている。
たとえば、Rを環とし、R加群M, Nのテンソル積π: M x N → M⊗Nは、次の性質で特徴付けられる。
(☆) 任意のR加群Lと、双線形写像f: M x N → Lを与えるごとに、線形写像g: M⊗N → Lが存在して、g∘π = fをみたす。
アラビア語圏では、材料となるデータA1, A2, A3, ...のことを「マンコ」、新しい対象Aのことを「ハメル」という。
それぞれの意味は「欠けたもの」、「補われたもの」である。
量子コンピュータでのプログラミングが出来るようになったら世界は変わるだろうか
調べたら中国のgeminiとかいう量子コンピュータが市販(価格は100万,500万,700万の3種類)されてるようだが
google
https://ionq.com/ どうプログラミングするのかは分からなかったｗ
言語はQ# / QuTiP /Qiskitなどがあるようだ
>>542 分解したら、Windows PCだったりして
クラウドストライク略してクラスト
>>562 Haskellだと分数型があるから、整数型と分数型のタプルにするとして、分数を型の方で1/2に限定できないから、四則演算の演算子の方に分数が1/2かどうかとか、半整数型で閉じてないから、計算結果の型を条件ごとに…肩を同じにしないといけないから無理だ。
分数型で統一して、半整数の条件満たしてるか判定した方が早そう。
専用演算子の返す値の型は…分数と半整数かどうかの判定結果のタプルかな？
(Ratio, Bool)
奇数・単偶数も見分けた方が良いだろうし、Boolの方を4値位のHeafIntFlg型？的なの作るか？
data HIFlg = HInt | Odd | SEven | AEven deriving Show
type HInt = (Ratio, HIFlg)
試しに(Ratio,Bool)で作れそうか見てみた。(Haskellの分数型は%が/の代わり)
ghci> (1+1%2,True) -- 1+1%2 = 1 + 1/2
(3 % 2,True)
うん。
行けそうだね。
>562、ここまでお膳立てすれば後は出来るよね？じゃあねﾉｼ
NHK BS 熱血Bリーグ
こういうのはLLMでどうにかならんの？
無理かな。
>>571 それたんにNNのこと言ってだけで
language modelでやる説明になってない
ここまで表示的意味論の話題無し。
専門外（そもそも趣味なので専門以前）だが、確かに詳しい人が居たら聞いてみたい
俺も詳しくはないが、具体的に何を聞きたい？
表示的意味論でプログラミング不可能な部分とか、その逆にプログラミングで出来るけど表示的意味論では不可能な部分。
プログラミングでできるけど表示的意味論で不可能な部分なんて大量にあるのでは。
でも、問題はプログラミング言語のいろんな特徴を反映させたデータ領域というのが、機能をひとつ追加するごとにその
原理的に可能でも、現実的には不可能…なるほど…。
いや、知らんけど。俺も勉強中の身だからまともに受け取らないでほしい。
それより「表示的意味論」てう用語は全角漢字6文字で長いから
「プログラミング」これも長ったらしい
なんか夢見てる感じの文章な気がするぞ。
Rubyとかを表示的意味論（DS？）で数学的対象与えようとすると、データ領域の定義が滅茶苦茶複雑になるから、意味論なのに人間には理解できないとかそういうことになると思うけれど
DSの定義とは
💣💣💣detonational semantics💣💣💣
プログラミングの課題
直感的に、短く、そしていちいちボイラープレートを書かんでもいいようにしてくれ
マシンや処理系の仕様に合わせてキーを打つのは人間様のすることではない
x^2 = 2をみたす正の実数xは一意的に存在する
>>597 問題だと思わないならすべてのソフトウェアをマシン語直接書けばいいと思うんだけど、そうしないの？
ありがちなつまらない問答
このガイジ3月からずっと粘着してんの？
>>596 マジレスするとsympyとか使ってxのまま計算して
最後にsolveさせると良いよ
>>596 そういう道具をお前が開発すればいい話、有効ならみんな使ってくれる
>>601 それは√2を代数的に扱えるだけで、「数学」ができるようになるわけじゃないよね
>>602 CoqだのAgdaだのLeanだのすでにあるが、プログラミングのタスクに使うには現実的ではないから使われていない
>人間の思考をコンピュータの都合に合わせようとしているのが問題
どうせコンピュータの仕組み、どう動くか分からん素人のポエムだろ
>>606 コンピュータの仕組みとこの話がどう関係すんの？
>>608 コンピュータの仕組みとこの話がどう関係するの？（2回目）
>>612 自分で考えろ
わかんねーなら口挟むな雑魚
>>612 定理証明支援だろ
日本語読めんのか？ｗ
子どもたちがママや先生に「なんで？どうして？」と質問攻めする
やらないやつは
ここまでやって
>>1 や
>>596 の問題でさえ、まともな解答を与えられない雑魚ども
人間が証明する場合だって地道に微積分とか勉強しなきゃいけないんだから、プログラミングでやる場合でも、前提となる命題を地道にライブラリとして実装するしかないんじゃないの？
>>63 RubyやPythonは実行も遅くバカ大衆向けの言語
>>617 虐待するような親は
どんな素晴らしい育児本が出ても
どのみち読まない
どの数学を勉強するかにもよるな
コンピュータは電気で動いている
電子レベルでは不確定性原理が成り立つから、演繹法は成り立たない
数学は純粋関数型言語と同じで副作用がないが、プログラミングは副作用を扱えるので、プログラミングは数学の完全上位互換といえる
数学は数学で記述される
ポエム書き始めるぐらいならもう引退したほうがいい
>>631 >>639 数学にできてプログラミングにできないこととは？
lim[x→0](1/x) みたいなのってどうやるんだっけ
>>641 Σ(n = 0, 100) 2^(-n) ≠2 -- 100の部分が∞になった時(2^(-∞))、初めて 2 になる。
数学だと真(True)になるが、Haskellプログラムは-53乗から答えが2になって、この式は偽(False)になる。
sum [2^^(-n) | n <- [0..53]] /= 2 = False -- 間違った答えを表示。
グラフアプリ（Webアプリ）のDesmosでも確認したので、専用のアプリや言語でも間違ってる可能性が高い。
こういう精度の問題がプログラムはメモリが有限である限り、必ず存在する。
(√2)^2 = 2
が正しく真になるかどうかもプログラム次第。
（こちらはグラフアプリの様な専用のものは対応してることが多い）
>>642 ghci> [1/x | x <- [10,9..0]]
[0.1,0.1111111111111111,0.125,0.14285714285714285,0.16666666666666666,0.2,0.25,0.3333333333333333,0.5,1.0,Infinity]
ghci> last [1/x | x <- [10,9..0]]
Infinity
>>644 イプシロン-デルタ論法使えばいいじゃん
>>647 じゃあやってみて。
言語は問わないので。
>>648 イミフ
イプシロン-デルタ論法って特定のプログラミング言語の機能だと思ってるの？
lim_{k to ∞} sum_{k=1}^{n} 2^(-k) = 2
>>650 やり直し。
TeXの数式じゃなくて、プログラミング言語のコードで。
使えば良いじゃんって事は、普通のプログラミング言語なら使えるんでしょ？
>>652 >644を数学にしかできない方法として極限を出したらイプシロン-デルタ論法出してきたでしょ？
プログラミングでイプシロン-デルタ論法使えば、数学と同じことができるって主張じゃないの？
というか、私の主張は
lim_{k to ∞} sum_{k=1}^{n} 2^(-k) = 2 をチェックする関数verify()を作って、
>>654 なんで数学サイドは極限を扱っているのに、プログラミングサイドは近似値計算してんのが分からない
>プログラミングはイプシロン-デルタ論法が（一定の精度までしか）出来ない。
意味がわからない
イプシロンデルタ論法の「精度」とはなんぞや？
数式プロセッサで10秒で解ける話をいつまで引っ張る気？
>>657 概念や問題設定を確立することも含めて研究だ
問題意識に共感できないなら黙ってろ
先行研究を調べるという発想もそのやり方もわからないポンコツなの自覚した方がいいぞ
>>659 定義を否定するのはさすがに数学者の姿勢として間違っているかと。
数学なんて定義が違えば結果が変わるんだから、定義すらできないなら議論する以前の状態。
擬似問題だらけになって議論なんてできないわな。
>>661 微積分もフーリエ変換も超関数も厳密な定義の無いところから始まったんだが
そもそも何を定義してほしいんだ？
未知の概念を誰かに「定義してほしい」では会話にならない
「自分はこういう定義・定式化するのが適切だと思う」と自発的に提案できなければ、数学の研究はできない
>>661 は完全に間違っている
>646
>>654 の言ってるのは、「CPUは整数しか扱わないから、コンピュータで文字列は扱えない」と言ってるのと同じ
それに対してこちらはずっと「文字に文字コードを割り当てれば文字列を扱える」と正しい指摘をしているのだが、
「できるならプログラミングで書いてみろ」とか意味不明な言いがかりをつけてくる
Σ_{k=0 to N} 2^(-k)が2に収束することを証明するには、N = 100や1000を代入しようが駄目で、極限を扱わなければならない
>>654 のやってることは何の意味も無い
で、イプシロンデルタ論法を使えば厳密に証明できるとこちらは何度も言っているのに、聞く耳を持たない
数学と実装は独立
>>671 うちの主張したいことは、イプシロンデルタ論法はいくらでも数値の誤差をイプシロン以下に抑えられるのを保証することを証明しているのだが、プログラミングではそのイプシロン以下に抑えられない程誤差が大きくなるってのが、数学を厳密にプログラミング出来ない理由として挙げてる。
プログラミングのは、極限値だけ決め打ちで答えが出るようにしてるだけなので、100とかでイプシロン以下に抑えられない誤差が現れる例としてだした。
添え字集合が実数や複素数というのも、その実数の連続性・比可算無限が根本にある。
無限次元の空間は整数の話だが、多倍長整数使ってもメモリ以上の空間は扱えない。
どれも事実上問題になるわけではないが、>1のいう「近似ではなく厳密に」なら不可能と言わざるを得ない。
>>676 何度同じことを言えば理解できるのだろうこの馬鹿は
>>678 プログラミング可能なことをコードで示したら理解します。
「実数εを任意に選べる文脈で、項と極限値の差をε未満に抑えるNを選ぶことができる」ことを示すのがイプシロンデルタ論法
>>679 それはお前の理解力が低すぎるだけ
コンピュータで文字列を扱うのに文字コードの実装をすべて見せなくたって
「たとえば文字の'0'に整数48を割り当てる」のように説明すれば、ふつうの理解力があれば理解できる
自分の知性の問題を責任転嫁しないでくれ
>>681 verify()の中身。
あと、決め打ちって書いてるでしょ。
その100での具体的な近似値求められないと「厳密」にならない。
なので私からの宿題は100の時の具体的な近似値を求めるコードを示すこと。
>>683 二進法で一の位以下に1が101個並んだ数だよ
こんなんプログラミングしなきゃわからんの？
s = "1.";
>>680 ε自体はな。
でも、真の値aに対して a + ε, a - εって使うのがイプシロンデルタ論法。
数学ではそれで限りなく無限に近くεを小さくしてもその範囲内に真の値が存在することを証明しているが、
プログラミングでは一定の大きさのεまでしか保証されない。
こういえばいいか？
真の値は確かにあるが、プログラミングでは間違った値を返す場合がある。
極限が正しければ厳密じゃない。
途中もすべて正しくないなら、それは厳密ではない。
>>685 ,686
御大層なこと言っておいてそれで数学を厳密にプログラミング出来ましたってか？
そういうのを決め打ちっていうんだよ。
どんなコードが出るか期待してたら…。
>>687 こいついつまで同じ間違いを主張し続けるんだろう
わざとなのかな
>>687 それは組み込み関数、ライブリライのせいだよ、アホ
>>687 そんなことは70年代には解決されている
なんか擬似問題臭くて良くわからんが、非可算無限と可算無限を同列に扱っている？
発明したな
イプシロンデルタは
数学の定義や命題は有限の記号列で書ける
結局それをやる意味ってないよね
ZFCを書いて、それらで定理を書けばできそうな気もするけど、意味あるのｗｗｗ
自分の無知や誤解を認めずに「それ意味あるの」と話をそらすのはみっともない
>>701 プログラムの性質が型として記述されていれば実行前にチェック可能
物理、化学もプログラミングできるんじゃね、知らんけど
チューリングやノイマンにも「それ意味あるの？」とか言ってそう
>>708 仮想マシンやエミュレータって聞いたことない？
記号の変換はスマホの機種変更と同じぐらい無駄が多いので
手書き最高
とにかく実装をしたくない
>>719 理論的には可能だけど
結局複雑さが仕様記述に移るだけ
>>721 理論的に不可能と言わないと学のレベルが知れちゃうよ
>>722 は？自動証明機の原理と同じって習ってないの？
学がないね
O(n logn)のソートアルゴリズムいくつあると思ってんだ(笑)
>>724 やっぱり何もわかってないし
CSと数学基礎論を修めてないの自白してるぞ
それは算法でいくつもあるならどれでもいいって話だバカ
無理です
>>727 な？不思議だよなw
学べば別に魔法じゃないことがわかる
test
∧＿∧
>>728 TypeScriptの型システムは強くない
ザルのJavaScriptに比べればマシという程度
それでも実用的な型システムは強ければ強いほど開発効率が上がる
気付いた人たちはもっと強力なプログラミング言語へ移行する
一方で数学的な各種概念などを型システムに採り入れただけの言語は実用には遠い
効率って短時間という意味だよな
>>740 こんなのプログラミングに使わないけどw
中高生がプログラミングするのは今や当たり前だけどw
Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明
https://mathlog.info/articles/1405 グレゴリー・ライプニッツ級数の収束をCoqで証明する際には、Realsライブラリを用いて実数の扱いを行い、級数の定義を元に収束の証明を組み立てます。証明の詳細は、数列の部分和の収束を示すために必要な補題や定理を適宜導入し、論理的に証明を進めていく必要があります。
誰でもできることには価値がないと判断しなかった者だけが
証明の正確さを検証するためのツールなのに、わかり切った証明（項の交換など）を明示的に書かなければいけない
自明な部分とそうでない部分は平等に検証されるべきか？
>>761 じゃあ、正しく少数を表現できるコードをどうぞ。
前回の人は>685-686などというコードで信用無くした。
Ωをプログラムの表現しうる全データの集合
ゲーデルの不完全性を解けば人類は理論上次の次元に到達する
予言者
そういえばπの定義は微妙なので
>>742 の証明は形式的なものに過ぎない可能性がある
>>762 任意精度数値計算ライブラリ
メモリに依存するみたいだけど
言語論とか役に立たないからな
計算可能実数というのがあってπは扱えるけど実数全体は無理
球面上で風や海流などの分布を考えると、かならず流れが無い点Pが存在する
縮小写像はかならず不動点をもつ
テンソル積、射影加群、入射加群、逆極限、順極限、……などはすべて普遍性で特徴づけられる
不動点定理は不動点を持たない関数(特に否定演算)がある領域では成り立たないよね。
掛け算の可換性は非可換群では成り立たないよねとか当たり前のことを言ってるようなもん
数学とプログラミングを対立構造で見てる時点で何もわかってない
>>785 具体的にどのレスを指して「数学とプログラミングを対立構造で見てる」と言ってる？
ただの独り言？ならごめん。
単一継承ならせいぜい親と子の対立しかない
自分が理解できないからと言って難癖をつけるのはやめましょう
正しい言葉遣いをしたら綺麗事しか言わなくなると思うよ
商売なら買い手に責任がある
科学をプログラミングするのは難しいが
オブジェクト指向って、コンピュータサイエンスじゃないんだよな
構造化プログラミングや、関数プログラミングは、それ以前より高レベルの抽象化をもたらしたけど、オブジェクト指向は単に書き方の問題
そして、科学論文の体裁は重要だが、オブジェクト指向はいまや重要ではない
型
俺が大学生だった20年前はオブジェクト指向もCSの一部だったが
で、出ｗｗｗｗインターネットあまのじゃく君ｗｗｗｗｗｗｗ
>>809 たった三行でここまで頭悪そうな文章書けるのってある意味才能だな
カプセル化も全否定されてるけど
デザインパターン20数個のうち10数個ぐらいはただの高階関数でかけるという研究もある
>>816 そして残りの10個はただのアンチパターン
岩波講座 ソフトウェア科学 [基礎]1
なぜ高階関数を使わないのか
型なんて特別なものじゃない
>>824 咄嗟にアニメの話出せるとか
おまえすげえ最先端行ってるな
才能の塊かよ
>>824 それ知ってるわ
煉獄さんの映画のやつだろ
お前マジでおもしれーな
型が第一級オブジェクトなら、クロージャを使えば状態つきの型を作れるわけか
>>827 わざわざ型情報を実行時に変化させてどうすんだ
有理数型はHaskellやMathematicaにもうある
状態付きの計算を行う手順を持った型なら純粋だから許せるけど
`f1 = Foo 1`なら、f1の型は`Foo 1`
`f1 = Foo 1`なら、`f1`の型は`Foo 1`
型っつっても所詮は構造体に名前がついただけ
>>841 君が数学で研究職に就いているのでなければ、まず間違いなく君よりは理解してるよ
>>839 実行時のアサーションで書けることは、型にできる
二分探索やクイックソートのロジックが正しいことを型で証明できるか
数学的帰納法で証明できる
アキュームレータを再帰的に更新していくようなのはF代数に抽象化できる
抽象データ型、凝集度、関心の分離などの既存の概念だけで簡潔かつ正確に説明できることをわざわざバズワードに言い換えただけのクソ概念
実は当たり前にやっていること。関数適用はmodus ponensに相当する
型情報からあまり使ったことない関数でも使い方にあたりがつくのは便利だと思うけどお前はそうではないんだな
複素数型も四元数型も定義可能だし、GPUに組み込んで高速で並列演算できるようにしてやれば科学界に革命を起こせるな
処理系がcall/ccをサポートすることは、直観主義論理に背理法を加えることに相当する
研究者の名前がなかなか思い出せなかったがGriffinだな POPL 1990
イマドキ型のない言語なんて、即席のスクリプトくらいにしか使わんでしょ
代数的データ型やパラメータ多相を使えばプログラムのかなり多くの性質をコンパイラが保証できるのに、わざわざ型検査なしで注意してコード書くとか馬鹿のすること
人類未曾有のソフトウェアを書くならともかく、巷のプログラムの9割近くのコードはただデータを整形してマッピングしてるだけ
しかし、それができるなら動的型付けの言語でもエディタが構文から型推論すれば同じことができるのでは？
ところがどっこい
なんかグダグダ言ってるけどそれ形式論理なしでできるよね
単純に、お前の話に誰も興味ないから話題が変わっただけでは
ocamlなんかは型推論の健全性と完全性を備えているから
まぁ形式論理も時相論理もプログラミングには何の恩恵もないわな
CSは数学を一部利用するが
学問にコンプレックス持ってる人って、みっともないね。
>>857 パラメータ多相のジェネリックな型は特に制約を指定しなければ任意の型がOK何でもありだけど
何の型でもありということは使える範囲も極めて狭いというか
言語によってはprintすることすら任意の型が可能派と必ずしも可能とは限らない派もあり曖昧で
何らかの制約を指定しないと何の処理もできないためその型の値をそのまま返すことしかできなくなってしまう
つまりジェネリック型パラメータに対する制約記述がカギとなる
>>866 多分コンプレックスとかじゃなくて無駄なものを持ち込まずにシンプルにしておきたいってだけじゃない
>>865 数学が専門の人がどんどんCSに入ってきて内容が高度化してるって聞いたぞ俺は
なんでコンプレックスの話が出て来てるのかさっぱり判らん
>>869 それこそ
>>865 の説を補強してるだけじゃないの
>>868 数学やCSを持ち込んで対象が複雑になると思ってるのは、
自分が理解できないものにコンプレックス持ってるからだよ
理論を作って対象が複雑になることはあり得ない
>>873 一筆書きして最初の場所に戻ってこられるか、は複雑な問題
グラフのすべての頂点から出ている辺の数が偶数、というのは単純な問題
グラフ理論を持ち込んで問題が複雑になったというのは、
頂点・辺・偶数・奇数などの概念が理解できないから
それは数学に対するコンプレックスにほかならない
>>871 P=NP予想とかCSの問題も数学で扱われてるんだから知らんがな状態ではないと思う
プログラミングに必要な数学は数値計算で使う数学くらいか？
>>876 プログラミングと数学を分けてる時点で、Qiitaのブログのサンプルコピペしてる雑魚と同レベル
プログラミングに数学はいくらでも使うことができる
Felleisen 30年研究して「プログラミングには型が必要なことがわかった」←これ好き
型＝命題
>>881 お前のソースコード見せてくれよ
どんだけ立派なのか拝ませてくれ
int i=10;
C/C++の型付けは、メモリをなんぼ確保するかの目印でしかないからな
Rustの型はトレイト属性があって
その代わりにmany shared XOR one mutableのキツいルールがあるけどな。
自力で証明するよりも他者の言質を取るというか契約が成立することにより安全が保証される
正直、Rustに心酔してる奴って、程度が低すぎ・・・
言っちゃ悪いが、人間の知能は平等ではない
ある人は数論幾何学や場の量子論などがわかるが、ある人は中学校の連立方程式くらいしかわからない
振舞いを自動化しろと言われるのと判断は人間の責任っていうのは
>>887 single writer XOR multiple readers はデータ参照の競合バグを防ぐために役立つルール
これを守ると参照競合によるバグを防げるだけでなく
プログラムのスパゲッティ化を防ぐ効果も高い
さらにRustではそこに内部可変性が用意されているため
そのルールを守ったまま複数のデータ更新者(ex.マルチスレッド)が排他制御しながら同じデータを書き換えることも可能
>>891 その数論幾何の人にプログラミング言語を作ってもらえばいいんでね
新商品を作ることにより今後の支障がなくなるといつから錯覚していた
>>895 すでに表記の体系はある
CS畑のやつが処理系を作ればいい
>>897 それはMathematicaじゃダメなん？
表記の体系って、プログラミングするには演算子の優先順位を決めないといけないがそれも決まってるの？
CSやってて数学のわからないところは記号の優先順位がわからなくて読み解けないことがある点
>>900 Mathematicaは数式処理システムだ
数論幾何用のソフトウェアがないってことかね、表記の体系はどこでみれるの
必要なのはドリルではなく穴
ID:iLzbIZXE こういう現代文なら零点のレス返してくる人って、日々の生活相当苦労してそうだな
試験はギリギリ解けないレベルまで難化する
レベル、経験値、ポイント、HP、通貨、メッセージ数、フレンド数
経験的なデータはリセットできるからリセット不可能なものと分断されたり見下されたりする
そう言えばPASCALのスレ無くなってるな
スレタイ、レス件数、スレ作成日、投稿時刻に4や13、忌み数字を使って嫌がらせするネットストーカー、SNSストーカー業者がキモすぎ
業者の嫌がらせ数字組み合わせ
閲覧171人とか174人、179人、180人、184人
忌み数字を踏ませる業者、アプリ、コンピュータプログラムの嫌がらせ
閲覧171人とか174人、179人、180人、184人
お薬のもうね
口コミや地域マップの表示回数やいいね件数、コメント数、フォロワー数、投稿時刻、通知件数、レビュー評価等で、意図的に忌み数字や悪意のあるポケベル暗号数字をしつこく強調する町内会員の嫌がらせがキモすぎ
スケッチ→スキャッフォルド→スキーマ
とりあえずフロントエンドは度外視
Wolfram Languageの使い方を聞きに来たんだが
存在は普遍性
ゲーテルの不完全性定理と計算可能性の話で全部記述することは無理なんじゃなかった？
>>950 知らんから教えて
Wikipedia見ても分からん
「初等的な自然数論を含む」って何？
「有限の立場」って何？
説明してね
このスレへの固定リンク： http://5chb.net/r/tech/1710585705/ ヒント： 5chスレのurlに http ://xxxx.5chb .net/xxxx のようにb を入れるだけでここでスレ保存、閲覧できます。 TOPへ TOPへ
全掲示板一覧 この掲示板へ 人気スレ |
Youtube 動画
>50
>100
>200
>300
>500
>1000枚
新着画像 ↓「「数学」をプログラミングするには YouTube動画>1本 ->画像>1枚 」 を見た人も見ています：・【議論】お前らって「プログラミング」に「数学」って「必要」だと「思う」？ 「数学」をプログラミングするには2 (186) 【悲報】OpenAI代表「数学、プログラミング、物理学はAIがやるようになる。電卓に人間が絶対勝てないのと同じ」 A「古文漢文得意です。崩し文字、隷書書けます」B「数学物理得意です。プログラミング書けます」日本ではBの方が評価されるらしい… プログラミングにはMac プログラミングにはMac プログラミングにはMac 趣味プログラミングに使ってる言語何？ プログラミングに自信ニキ来て 競技プログラミングについて語るスレ 線形代数ってプログラミングに使う？ プログラミングに興味があるゲイ Windows VS Macプログラミングに適したOS 競技プログラミングにハマるプログラマのスレ 63 競技プログラミングにハマるプログラマのスレ 212 競技プログラミングにハマるプログラマのスレ 51 プログラミングに自信あるやつちょっときてくれ 競技プログラミングにハマるプログラマのスレ 191 競技プログラミングにハマるプログラマのスレ 73 競技プログラミングにハマるプログラマのスレ 50 競技プログラミングにハマるプログラマのスレ 117 競技プログラミングにハマるガイジのスレ 94 競技プログラミングにハマるガイジのスレ 93 競技プログラミングにハマるプログラマのスレ 33 競技プログラミングにハマるプログラマのスレ 93 競技プログラミングにハマるプログラマのスレ 44 競技プログラミングにハマるプログラマのスレ 43 競技プログラミングにハマるプログラマのスレ 97 データベースプログラミングに最適な言語は何か 競技プログラミングにハマるプログラマのスレ 12 競技プログラミングにハマるプログラマのスレ 166 競技プログラミングにハマるプログラマのスレ 193 競技プログラミングにハマるプログラマのスレ 153 競技プログラミングにハマるプログラマのスレ 201 競技プログラミングにハマるプログラマのスレ 156 競技プログラミングにハマるプログラマのスレ 5 競技プログラミングにハマるプログラマのスレ 64 競技プログラミングにハマるプログラマのスレ 67 競技プログラミングにハマるプログラマのスレ 82 競技プログラミングにハマるプログラマのスレ 11 競技プログラミングにハマるプログラマのスレ 78 競技プログラミングにハマるプログラマのスレ 36 競技プログラミングにハマるプログラマのスレ 99 競技プログラミングにハマるプログラマのスレ 69 競技プログラミングにハマるプログラマのスレ 81 競技プログラミングにハマるプログラマのスレ 80 競技プログラミングにハマるプログラマのスレ 28 競技プログラミングにハマるプログラマのスレ 102 競技プログラミングにハマるプログラマのスレ 160 競技プログラミングにハマるプログラマのスレ 143 競技プログラミングにハマるプログラマのスレ 177 競技プログラミングにハマるプログラマのスレ 175 競技プログラミングにハマるプログラマのスレ 116 競技プログラミングにハマるプログラマのスレ 167 競技プログラミングにハマるプログラマのスレ 205 競技プログラミングにハマるプログラマのスレ 144 なぜプログラミングに向いてない人がプログラミングを頑張ってしまうのか 音声処理ソフトを作りたいんだけどプログラミングに詳しい人助けて 「プログラミングするならMac」の真偽は プログラミング勉強したい その理由は 中卒がjavaとかいうプログラミング言語でゲーム作れるようになるには 【IT】2019年にフリーランスに求められるプログラミングスキルとは 宣言型 命令型プログラミングについて (7) 知ってるとプログラミングに役立つ数学知識 (272) プログラミングに詳しくて辛抱強い人来て (35) 競技プログラミングにハマるプログラマのスレ (222)
18:51:38 up 63 days, 19:50, 0 users, load average: 9.97, 11.11, 10.96
in 0.028146028518677 sec
@0.028146028518677@0b7 on 062007
ブックマークへ