「数学」をプログラミングするには
たとえば、プログラミングで π/4 = 1 - 1/3 + 1/5 - 1/7 + ... を近似ではなく厳密に確かめるにはどうしたらいいの 人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど >>1 証明を記述するための言語がある。CoqとかAgdaとか あと単発質問はスレを立てるまでもない質問スレでどうぞ >>1 アルゴリズムではなくメモリ容量の問題 無限小数を求めるには無限のメモリが必要で世界中のメモリを集めても無限にはならないので不可能なだけ >>3 この問題解くのに無限小数計算してる奴なんかおらんわ(笑) 数学をプログラミングする方法は、使用するプログラミング言語によって異なりますが、一般的なアプローチは次の通りです。 適切なプログラミング言語の選択: 数学をプログラミングするためには、数値計算やデータ解析に適した言語を選択することが重要です。Python、Julia、MATLAB、Rなどが一般的に使用されます。 必要なライブラリのインポート: 数学的な計算を効率的に行うためには、各言語には数学関連のライブラリが用意されています。例えば、Pythonの場合、NumPyやSciPyが、Juliaの場合、Baseや特定のパッケージが数学関数を提供します。 数学的なアルゴリズムの実装: 数学的なアルゴリズムをプログラミングする際には、基本的な数学的概念やアルゴリズムの理解が必要です。数式をプログラムに変換することが重要です。 データの操作と可視化: 数学をプログラミングする場合、しばしばデータの操作や可視化が必要になります。そのためには、適切なデータ構造や可視化ツールを使用します。 ランベルト関数(近似精度がヤヴァくてもヨシ) をサポートしてる言語のがほしいデス 基礎論以外の命題の証明を証明支援系で一から書くのは現実的ではないから、既存の有名命題がライブラリとして使えるような処理系を使うことになるんだろう 証明支援系で証明を書いても、それを再利用してべつの定理を自動で証明できるわけでもないし、ソフトウェアとして全く無意味だよね…… 証明支援系を使うことで未知の証明ができたり、数学の問題がよくわかったりするわけじゃなくて、 すでに証明できてるものを、PかつQを表す型はこうで~ みたいな書き換えをやるだけだからな 証明支援系が役に立たないなら、そもそも数学で証明を与えることにどういう意味があるのか考えてしまう 厳密だが根拠がない等式を、厳密ではないが根拠のある不等式の集まりにすりかえる 数==数では背理法が使いにくいが 集合==集合は背理法や不等号の価値がまるで渡米したIT創業者みたいになる 読まなくても分かることをほぼ知り尽くしてから読めば楽に読める 例えば書いた者に悪意があるのかないのかを事前に知らないより知っている方が楽 正義とか悪とかが苦手な人にはこれができない ∫_0^1 dx/(1 + x^2) = Arctan(1) - Arctan(0) = π/4 x = arctan(y) x' = 1/y' = cos(x)^2 = cos(x)^2/(cos(x)^2 + sin(x)^2) = 1/(1 + tan(x)^2) = 1/(1 + y^2) 微分とtanの特殊値がライブラリによって既知なら、書き下せそう ただ、書いたところでだからなんだって話だが あとArctanのテイラー展開 もしくは項別積分 項別積分する場合は、べき級数の収束半径とか、境界での連続性とかも 積分変数を別名に変えても積分の結果が変わらないこと などを証明することに興味無さすぎて 変数を使わない技術だけが発達しているんじゃないか >>4 そしてあんたはプログラムができない 永久にすれ違いだなw >>5 実際に計算しない限りプログラムの世界では完成したとは言えない できたような気になってるだけだw 変数に別の変数 (を含む式) を代入するのは嫌なので、右辺を実際に計算してしまった値を代入する 計算してない式を代入するのが何故そんなに嫌なのかを理解しない限り話が進まない コード書けない奴が必死に妄想でレスバするクソスレ NG決定 しかし、何も書かないより悪いコードを書く方がマシみたいな保証が あると思うならそれこそ妄想なのでは 数学を記述するには一階述語論理があれば十分 しかし処理系側は特殊なケースに特化するよりも自然に実装できる範囲で一般化したほうがいいだろう 命題の記述は依存型による ○○を支援する言語と○○が可能な言語を分断するパラダイムはたしかにオワコンだ 逆に支援を語りえない所謂unsafeを書けるやつが比較的新しい >2 の紹介しているCoqとか、純粋関数型言語HaskellもPCで動く数学って感じではあるけども、そもそもメモリが有限なので連続を表現できない。 どんなに小さい数を表現できても有限である以上は離散的なのよねん。 離散数学の範囲ならHaskell良いよ。 子供向けだけど、Viscuit(ビスケット)は写像というか変換のみで言語作ってる。 (ビスケットの中の人曰く「書き換え型言語」) leanとかいうソフトで学部レベルの定理の証明をすべて書くとかいうプロジェクトがあるそうですが、そういう証明を見ると勉強する側として勉強になりますか? ほんとうに教科書に載ってる定理の証明がぜんぶ正しく書かれてるなら、それは教科書読んでるのと同じわけだし lean4はプログラミング言語としても、haskellやrustくらいパワフルな言語なので、cだのfortranだの勉強するよりプログラミングの勉強にもなる >>29 推論規則にしたがって項を削除したり、条件をみたす要素を深さ優先探索したり 証明支援系っつっても、ふつうにプログラム書くのと同じで、特定の問題の解法をプログラムしてるだけ ようは論理のピタゴラスイッチ作ってるだけ べつに未知の証明を自動で発見してくれるわけではない(もちろん、問題によっては自動的に解決できる場合もあるが) 証明支援系Lean4 数式処理システムSage 組版システムLaTeX を組み合わせたオープンソースの統合数学環境と、黒板の文字や図を認識する入力インタフェースがあればいいと思う >>36 「プログラミングの勉強」を「プログラム言語」の勉強だと思ってるバカ 「program」の意味を調べてみろ。言語はただの手法の一つ >>36 CやFortranの評価が低いということはHaskellの中でモナドの評価が低いよね それはもったいないから言語を競争させる原理はよくない ミサイルでも撃たれたならともかく ポエムなるものを書き込まれたことへの反応が過剰なのが気になる 現実世界にポエムが存在しなくなれば消去法で「数学」になるってことなのかな スレタイが悪い 専門用語や英語を入れておかないと、自分も話題に参加できると勘違いした馬鹿が書き込む >>33 すでに解けてる問題を特定の処理系の言語に書き直すのが一大プロジェクトというのがくだらないと思う >>50 すでに常識になっていることを「先入観にとらわれている」と思う人はいる 先入観をリセットしてやり直したい需要は多少はある >>52 馬鹿すぎて話にならない わざとやってるならむしろお笑い番組の脚本とか考えるセンスあると思うよ わざと馬鹿になったのではないが 数学の範囲内の定理を厳密に証明しても、内か外かの判断は厳密にならないので 「プログラミングならなんでも数学」のような馬鹿な意見も厳密に全否定できないんだよな 現代数学は集合と写像の言葉で書かれている 写像は関数の一般化だからC言語やHaskellなどの関数型言語では数学をプログラミングできない RubyやPythonなどにはsetやmapといった機能があるから これで数学をプログラミングできると思われる >>56 それは違う 数学ができるプログラミング言語のコンパイラをCで書くことができる そもそもすべてのプログラム言語はチューリング完全だからCで書けてハスケルに書けないなどということは無い >>56 それ逆だね mapは関数型言語で登場した そのRubyやPythonといったスクリプト言語は後からそれを導入した マップは関数の集合直積に過ぎない c言語でも有限アルゴリズムで数学プログラミングが出来る パイソンは構文をパースできるがスクリプト言語ゆえ数学プログラミングは無理 >>60 跡から登場したってことはRubyやPythonのほうが優れているってことやろが まともなプログラマーがスクリプト言語でプログラミング開発することはない スクリプト言語はスクリプトを書く程度のことをするだけのおもちゃ CやPYTONはスクリプト言語だから単純なことしかできない スレタイ 集合と写像が数学の基本らしい 写像というのは関数の一般化だからCは関数言語だから数学できないということになる Javaのmainは写像だからJavaは数学できる。Rubyにも写像ある 数学に副作用はないがモナドは副作用があるのでハスケルでは数学はできない >>56 Cでは関数の引数として関数ポインタを渡せるから、map関数を簡単に自作できる。 空論、絵に描いた餅、機械語にだってできるだろwww >>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 イテレータとは何かを学び直しなさい それは配列に対するイテレータ イテレータに配列なんていうものは必要ない イテレータなんぞプログラミング側の都合でしかないやろw 数学のどこにイテレーションって概念があるの? もとは集合の話だっけ? 集合のどこにイテレータ出てくる? 配列こそプログラミングやコンピュータ都合の邪道なものだね 配列は有限しか扱えないから不要 イテレータは自然数イテレータだけでなく例えばフィボナッチイテレータなど無限を扱える イテレータは数学とも相性がいい >>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 の人だけ理解できてないようだが それは間違い FORTRANが今もなお科学技術計算に使われてる 集合論はラッセルのパラドックスで矛盾した だから集合と写像に基づくC言語やRubyは数学を扱うのに不適切 よってハスケルなどは圏論に基づくから関数型言語が正解 プログラム言語は機械語→アセンブラ→高級言語 と進化してきたが、高級言語にも高級度の段階があって gotoジャンプ→構造化ループ→map→ベクトル演算 という序列になっている。 y = x.map(i => 2 * i) のように冗長な記述をしなければならない言語よりは、ベクトル演算で y = 2 * x と すっきり書けるFortranの方が進化している。 まったくトンチンカンな話してんな プログラミング言語にmapがあったところでそれで数学ができるわけじゃないだろ 何を解きたいんだよ? 定理証明か?仕様記述か? ド文系のふわっとした思考やめな >>95 それはarrayを入出力とするmapだね それは遅延評価もできず可算無限列を扱えない古い劣化タイプ 一方でiteratorを入出力とするmapはarrayだけでなく可算無限列など任意のものを対象にできる この完全なデタラメな話をここまで長々とする気力がどこから湧いてくるのかがわからない >>97 昔は配列に対するmapしか無かったから、遅延評価できず、有限列しか扱えず、中間生成配列のムダなど、悲惨だったな 今はイテレータに対してmapその他を適用するプログラミング言語が増えたので、扱える対象が広がるとともに、効率も良くなったな そもそも高階関数のmapは、数学の集合論における写像のことではない ゴミみたいな話しかしてないな、定理証明系とかの話をしているのかと思ったら >>97 >> 100 Ruby厨、Haskell厨が他の言語を貶めるのに必死だなw Fortranのプログラム program test integer :: x(3), y(3) x = (/1, 2, 3/) y = 2 * x + 1 print "(i0)", y end program の y = 2 * x + 1 の行で中間配列が作成されて、 integer :: temp(3) temp = 2 * x y = temp + 1 のような非効率な動作になるとでも思ってるのか? STLで提供しているC++のvalarrayと違って、 Fortranはベクトル演算に言語仕様レベルで対応しているから、そんなことするはずないだろ。 Visual Stduioで y = 2 * x + 1 の行の逆アセンブリを見てみると、 mov qword ptr [rbp + 68h], 1 mov rax, qword ptr [rbp + 68h] cmp rax, 3 jg TEST + 105h mov rax, qword ptr [rbp + 68h] imul rax, rax, 4 lea rdx, [X] add rdx, rax add rdx, 0FFFFFFFFFFFFFFFCh mov eax, dword ptr [rdx] imul eax, eax, 2 inc eax mov rdx, qword ptr [rbp + 68h] imul rdx, rdx, 4 lea rcx, [Y] add rcx, rdx add rcx, 0FFFFFFFFFFFFFFFCh mov dword ptr [rcx], eax mov eax, 1 add rax, qword ptr [rbp + 68h] mov qword ptr [rbp + 68h], rax jmp TEST + 0B7h というコードが生成されていて、中間配列なんて作成せず合成関数を1回だけ適用し、Cの for (i = 1; i <= 3; i++) y[i] = 2 * x[i] + 3; に相当する効率的な処理になっている。(add rdx, 0FFFFFFFFFFFFFFFCh を見ると、 配列の添字が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) では movabsq $21474836483, %rax movq %rax, TEST$Y(%rip) leaq TEST$Y(%rip), %rax movl $7, TEST$Y+8(%rip) というコードが生成され (IntelのコンパイラなのAT&T記法で読みにくいが)、Cの *(long long *)y = 0x500000003; *(int *)((char *)y + 8) = 7; に相当する処理 (リトルエンディアン環境で) になり、3と5がyに一度に書き込まれる。 いずれにしても、Ruby厨、Haskell厨の浅知恵でFortranに嚙み付いても滑稽なだけwww rustのほうがスゲーからfortranは黙っとれ フォートランは行列、有限要素法のライブラリィ呼ぶだけ、独自のコードなんか書かないw 数学をプログラミングするには、プログラマが数学の必要があるのでは? ギャンブルなら敗者が金を振り込めば秩序が戻るのだが 金を振り込んでしまう人がここにはいないので >>117 圏論型と言えるか分らんが、圏論が注目されたのは副作用の問題を圏論のモナドで表現できるということでHaskellに採用されたのがきっかけっぽい。 今は非可換確率論を圏論で表現すれば意識がどうやって生まれるのかの研究に使えるって話がある。 意識が生まれる謎が解ければAIに意識を持たせられる。 戻らないだろ、刑務所行き >ギャンブルなら敗者が金を振り込めば秩序が戻るのだが コンプライアンス的には絶対に違反しないブレないスタイルの方が楽だな 中庸とかいうのは数学的にも意味のない言葉 の筈だけど >>126 ガイジか? プログラマ→職業 数学→学問分野 日本語勉強し直すか死ねよ きっちりした仕様決め無しで「プログラミング」できるわけないだろうに なんで過疎ってる5chのさらに過疎板でこんな板違いスレ何度も書き込むやつがいるんだよ 「プログラムを作る人」じゃないよな ラッセルは作る人というより脆弱性を発見する人のように見える 意識は非可換だってどこかで聞いたな 現代数学は可換理論しか扱えないが、量子力学は非可換だから、意識=量子力学ってことになる 意識が非決定論なのは量子力学では状態が重ね合わせであることに起因する したがって意識の問題を解決するには量子コンピュータが必須となる 借金取りは見かけ上は極めて非決定的にふるまうが それでも純粋に合理的な行動しかしない存在とされているので意識の問題がない ポエマーさんはポエム板にでも行けよ 統失なら病院のほうがいいかな ゲーデルの不完全性定理で完全に否定されているだろ プログラムは不完全性では動かせない 不完全ではなく無定義語で挫折する人がいる 無定義語の定義を特定できないと命題を肯定も否定もできない説 日常生活で出てくる >>149 ガイジか? ゲーデルの不完全性定理はそんなことについて言及してないぞ 数列の概念がない奴でも無限級数の意味は分かるんだよね ハードルが低いせいで基礎知識の共有が難しい ↑ 数学が何がわかってないやつの典型 虚数もあるとかないとか騒いでるタイプ 言語に依存しない数学的オブジェクトの存在が保証されれば 表現を(統一するために)訂正させる仕組みを正当化しやすくなる 「プログラム技術」板で「数学」がどうのこうの語ってるのがもう頭悪いというか頭おかしい プログラムも数学もできない、掲示板の使い分けもできない知的障害 >>154 数学と物理はなんの関係もないぞ 数学ってZF(C)公理系を絶対ルールとするパズルゲームでしかないから 絶対にルール追加しないのは ルール追加のふりをしてバックドア設置されるリスクを回避してるんだろう 馬鹿参上 >数学ってZF(C)公理系を絶対ルールとするパズルゲームでしかないから ただし>>160 は支持するぞ 公理系を何にするかは議論があるだろうが推論パズルゲームってところは正しい プログラム組めない雑魚ほどなにか深遠そうな理論めいたものを言おうとするよな 大したこと言えないんだから黙ってればいいのに 学があったらポエム書かんやろw アホ文系の血が騒ぐからポエムに活路見出すんよね? バブルソートで長さnのリストがソート済みになることをnに関する数学的帰納法で示すコードを書いて下さい 構成論理でしかない帰納法は逃げ 背理法をプログラミングできてこそ真の数学プログラマ 数学一般をプログラムするのはきつそうだけど、>>1 の内容くらいならMathematicaとかでできるのでは iterableがソート済みならばfilter(function,iterable)もソート済みである これが活路か? >>171 プログラム技術と全く関係ないの、わかる? 単語だけ知ってても意味ないのよ べき集合の濃度がもとの集合よりも真に大きいことを対角線論法で示すプログラムを書いて下さい ゲーデルの不完全性定理とかプログラミングに関係ないぞ 計算機科学的には背理法はプログラミングでの継続に相当するものだと判明している プログラム=証明 型=命題という対応がある 命題としてはあるが証明ができない型としてa -> b -> a -> aがある 計算機に記号処理での証明は荷が重いやん これに出来る事は無限に数値計算をする機能だけなんだ 訂正((A->B)->A)->A)だった 記号処理はmaxima/mathematicaみたいなのでできるね ポストモダンも用語の雰囲気だけで数学や物理の用語を援用して失敗したけど,同じことを繰り返したいのかな うん。必ずしも泥棒が悪いとはお地蔵様も言わなかった。 パプリカのビキニより、DCミニの回収に漕ぎ出すことが幸せの秩序です。 五人官女だってです! カエルたちの笛や太鼓に合わせて回収中の不燃ゴミが吹き出してくる様は圧巻で、 まるでコンピューター・グラフィックスなんだ、これが! 総天然色の青春グラフィティや一億総プチブルを私が許さないことくらいオセアニアじゃあ常識なんだよ! >>182 そう、λμな でも対応があるだけで実用性はないよな ム板にバカが書き込むのは今に始まったことじゃないが、意味不明な戯言書き込みに来る奴がすごく多くなった 自分の中ではなんかすごいこと書いてるつもりなのか?すごいバカかキチガイなのはだれが見てもわかるが そんなことばかりやってるからネットですら過疎って文句言われにくいここに逃げ込むしかないんだろうな >>189 不満なら見なきゃいいだろ インターネットしか居場所ないのか?w スウ学をプログラミングするのは、簡単そうぢゃーーーん だって、乱数発生させて、厨二病が喜びそうな単語を 羅列すれば、完成だもんね。多分。ていうかさ、 全ての証明問題は、 【ゲーデルの不完全性定理により証明不可能 Q.E.D】 ってプログラミングするだけしさ、これだな。 嫌なら見るな,は反論になってないな 戯言を書き込む行動を少しは正当化してみろよ >>191 不完全性定理をわかってないなら無理にそんな意味不明なこと書かなくていいよ >>192 正当化は2種類 行動に個性があればもし失敗しても同じ失敗が集団的に繰り返される心配がないのと もう一つは、目には目を歯には歯をみたいな相手と同じことを繰り返せばOKと思ってるやつ >>162 >>164 その場合はコンピュータじゃなくて理論計算機科学とかだな、比較対象がおかしい。 数学史とか数学基礎論とか少しでもなんか読んでみ、今の数学はそういう思想だから その調子じゃヒルベルトプログラムもブルバキも何にも知らないだろ >>180 いやあるだろ…停止性問題とか知らないの…? こんなん数学科でもなくてもCS学科でもなくても 趣味でWikipedia読んでれば知れる雑学だぞ >>173 背理法って推論規則の一つでしかないから他の推論規則を使って導けるものじゃないんじゃないの 証明をプログラミングでやるって、命題論理の変換で真か偽になる変換方法の組み合わせを見つけるってことでしょ 人間がなかなか納得しがたいロジックでもプログラミングしたらはっきりする、わけじゃなくて、 なかなか納得しがたいロジックでも間違いがなければ論理に間違いはないので証明されたとする、という根本は変わらなくて 論理の変換をプログラムで行なえても不思議ではないと思うけどな 記号論理学を大学1年のときにとったけどそれぐらいの基礎すらなかったら証明、公理系、推論規則、あたりの概念がめちゃくちゃになってるんじゃないか? 完全性、健全性の意味をしらんのだな 完全って言葉から中二妄想膨らましてしったかかましてる 身体性という言葉の悪いところは 自分だけでなく他者の心身まで知ったかぶるところだ 数式ゴリゴリのデジタルフィルターなんか、プログラムで書くと、あぁそういう事かと理解が速いよね。 乱反射を解析し反射元の形状を投影するとか、マクスウェルFDTDで、MEMSデバイスのパターンを作るプログラムなどは、プログラムで理解する有用性を証明している。 始めに数学工学が必要なのは言うまでもない。 罵り愛が一段落下っぽいね。 まあ、何にせよ「数学」をそのままプログラミング出来てたら離散数学は今ほど重宝されてないと思う。 プログラミング言語の浮動小数点数も結局は離散数学だから、実数を浮動小数点数に、そして、CGとかだとさらに浮動小数点数を画面上のドット…つまり自然数(に0を加えたもの)の組(x,y)に変換しなきゃいけない。 「数学をプログラミングする」というのを「量子化しない」という意味だと思ってるのが、学がなさすぎる とりあえずHelloWorldから一歩でも先に進んでからこの板に書き込めよ 無能かつ的外れの「知ってるもん!」アピールなんか痛いだけって自覚もできないんだろうか そうなん? 「数学をプログラミングする」ってのがそういう意味じゃないなら、代数学的なのはHaskellの代数的データ型使えば割とできるし、証明とかは定理証明器って専用のプログラミング言語(Coqとか)があるよね? 統計学はRとか。 >1の文章読む限りは極限を求められる的な事と思ったけど? まあ、私に学がないのは事実なんで、↑2名は説明お願い致しますm(_ _)m printf("数学をプログラミングする\n"); 数学一般を広く浅くプログラミングできない 離散数学のバイアスがかかっている 不完全性と同様に、バイアスと言われても痛いと自覚しないやつほど順調に先に進める >>208 だから、>1への回答をお願いします。 その不完全性定理とか流し読みだからうろ覚えだけど、 ある数学モデルの無矛盾性をその数学モデルは証明できないとか?だっけ? 数学そのものの不完全さを証明したもので、「「数学」をプログラミングする」の 証明ではない気がするんだけど…。 物理的な不可能の証明として無限や連続性を上げるのは妥当だと思うのだが、 あなたは違うと言う。 なら、あなたは私の代わりに証明する義務があるのでは? プログラムってバカでもできるけど、間違いを指摘されて認めることもできないキチガイは入り口にも入ってこれてないよ 5chに書き込む前に早めに病院行ってお薬もらってきた方がいい 数式を計算するプログラムって逆ハンガリアン記法でスタックに積んで取り出すの? 数学をプログラミングと聞いて電卓が頭に浮かぶのか このあたりがCSを勉強したかどうかの違いだよな このスレはポスト オブジェクト指向はオワコンのスレって感じがする オブジェクト指向はもっと柔軟性を高めて欲しいわ。 クラスとかメソッドの集合として外延性を持つようにしてほしい。 C++の具体的な問題を目で盗めばRustを作れるが オブジェクト指向のアイデアを広く浅くコピーしても負け癖が複製されるだけだ たしかに、お金でも賭ければその限界が具現化するけど 考えるだけの場合はむしろ限界がないことが忌々しいんじゃないか 不完全性定理は公理的集合論から証明できないならPythonとかJavaには欠陥があるってことじゃん てことは今後はnginxとPostgreSQLが無きゃ食っていけなくなる?SQLは三値だから完全だろ? 厳密に求められないからπという記号を用いたわけで コンピュータで扱う場合はπという記号定数を使えばいいだけ 無限に続くので3.14...を厳密に求めることはできないのは数学もコンピュータも一緒 1がしたいことが何なのかよくわからん >>230 「数学をプログラミングするには」って書いてあるじゃん #define final constant π; >>230 > 厳密に求められないから πは厳密に求まるが 1/3 = 0.33... は割り切れないから求まらないとか思ってる文系くんかな?(笑) > πという記号定数を使えばいいだけ 馬鹿かな πって置いただけで、どうやってこれが無理数であることや、4arctan(1)と等しいことが確定するんだ?(笑) >>230 君、国語力が低すぎて文章を理解できないから、 数学の教科書もなんとなくで読んで来たんでしょ? 学問に向いてないよ、君(笑) >>230 で、こいつ次は、 「厳密にもとまらないというのは、10進数で有限桁で表せないという意味で言った」 とか言い訳するんだろうなあwwww >>230 > 1がしたいことが何なのかよくわからん 問題意識を理解できないなら、わざわざいっちょかみすんな わざわざいらんことして、おまけに無知まで晒してる 究極に恥ずかしいよお前(笑) スレタイが読めないなら小学校の国語からやり直しwww モピロン、地球人の開発したAIには、無理 霊的な霊感がないからだ。 Arctan(x) のマクローリン展開式の xに1を 代入して証明するような閃きは、 AIには無理なのである。 その訳は、閃き💡といった宇宙からの霊的な電波を 受信するのは、論理的考えて、 地球のAIには、ソレは、実装されてない。 モピロン、イカの視覚野に電極を、差し込んで 宇宙から霊的波動を受信できるようにすれば 話しは、別だが、シリコンウェーハに その様な回路はナイだろうから、 それは、証明は、無理だろう。 ていうか、ゲーデルの不完全性定理により 証明問題の全ては証明不可能ぢゃーーー BY 今日もテキトーな事を呟いてみたー 26点 長い上に一本調子 デタラメに書いたらいいわけじゃない そういや誰かがすべての言語はチューリング完全とか適当なことかいてたけど 一昔前のcobolはチューリング完全じゃないぞ チューリング完全は数学をプログラムするための必要条件ではないかな アセンブラはその意味で資格はあると思われる チューリング完全は算法に関する性質 数学そのものではない 計算 + 証明 = 数学 これは データ構造 + アルゴリズム = プログラミング に対応する 命題 + 証明 = 数学 ↑↓ 型 + アルゴリズム = プログラミング 命題 + 証明 ↑↓ 型 + プログラム これはカリーハワード同型対応として知られている このセットで数学といえるかは俺にはわからない 計算だけが数学ではなくとも計算以外の部分も大体は計算に埋め込めるのではないか? カリー・ハワードだろ 構成論理が前提なのわかってるか? 構成的論理ならきいたことはあるが構成論理ってなんだよ >>1 > たとえば、プログラミングで > > π/4 = 1 - 1/3 + 1/5 - 1/7 + ... > > を近似ではなく厳密に確かめるにはどうしたらいいの > 人間が証明できるってことは、有限なアルゴリズムに書き換えられると思うんだけど 人間が証明出来るからって、有限なアルゴリズムに書き換えられるとは限らないんだよなぁ…。 そもそも人間の証明がlimとか使って(仮に無限回繰り返せれば)極限はnになる(だろう)って感じで有限のアルゴリズムじゃない訳で。 >>260 とっくに解決した話題にいちいち間違った指摘をするのは面白いのか? 命題を実験すれば近似、証明すれば厳密 これを間違えて 命題(と証明)を明文化しなければ近似、明文化すれば厳密と思ってる人は結構いる >>261 テキトーに読み飛ばしてた^^; どのあたりで解決してたかアンカー教えて。 πは、プログラミングは、近年の地球人は、 arctanのヤツを4倍してるよ。ポクはホントは地球人だけど 然るに、 閃き💡でarctanのマクローリン展開をネットサーフィンで 調べてさ、xに1を代入すりゃ、 π/4 = 1 - 1/3 + 1/5 - 1/7 + ... になるってわかるし、収束するかなんて 霊的直感で、わかるぜ なんてたって、1/2 + 1/3 + 1/4 + 1/5 + ・・・ ですら、絶対有限値log(∞)に収束しちゃうもん🤡 ま、この発想、AIには無理だと思うよん。 てか、最近の地球人って🐴🦌ばっかだな πをarctanを4倍するなんて、 πは定数3.14159265でダイレクトにコーディングしなさーーい これ、不味いのかな❓ 知ってるヒト教えて下さい神様 現在のAIは何故か胴元になれないギャンブラーと同じ >>265 うんうん。 罵られるのは甘んじて受け入れるので、解決したところのアンカー(>数字)を教えてください。 このスレで解決されたって意味ではないのでは? >>260 の指摘なんて常識的なことだし >>268 ○ 常識的 × 数学ができない人によくある勘違い >>260 多分これって数列がある値に収束することを示すには無限に計算する以外に方法がないって思い込んでるのでは 人間が有限回のステップで証明できてる時点で有限のアルゴリズムだよ >>260 まず「極限はnになる」の基礎となる理論から調べたら? εδ論法は理解してる? 極限とは位相空間のある点の近傍にある番号から先の有向族が入ることである 帰納法とは順序集合においてある命題がある番号まで成立としたとき次の番号の命題が成立することである >>270 うん…。 まあ、そもそも有限ステップで証明可能な事と、近似値ではない真の値を求めることを混同してる>1が悪いって事やね。 ε-δ論法で証明出来るのはいくらでも精度の高い近似値を求められる(それをもって極限の存在を証明)ってだけやし。 >>286 1/3 = 0.33...は無限につづくから真の値は求められないとか言ってるようなもん 小学生レベル >>289 無理数はまさしく真の値は求められないだろ? それこそスパコンで何兆桁求めたとかニュースになるけど、それでも近似値でしかない。 証明はあくまで存在を保証するだけ。 >>290 「コーシー列の極限」が実数なんだから、コーシー列を与えれば真の値になるだろ。 証明は数列が極限を持つことを示せば良く、数を無限に並べる必要は無い。 他責というか他人からもらった情報を丸暗記しなければいい たとえば嫌いな問題は飛ばして好きな問題で点数を稼ぐのも 与えられた情報を好き嫌いで切り取ってしまう技術 >>291 いあ、だから。それが真の値の存在を示してるだけって事だろ。 証明の厳密さが違うだけで、意味としては同じだ。 値のサイズが大きかろうが無限だろうがそれを指すポインタのサイズは小さい >>294 同値判定(ついでに大小判定)できるんだから「存在だけ証明」じゃないだろ。 確かに四則演算は有理体で閉じていないけど、拡大体を考えれば問題ない。 >>296 それについては言い過ぎたと謝罪するけど、それって結局真の値は分からなくても√2って記号に押し込めれば順序比べられるし四則演算出来るってのと変わらない。 >1の求める近似値ではない厳密って何?って話になるが。 >>298 当たり前だろ。無理数は有理数じゃないんだから、有理数とは対応しない。 現代の数学は「実数=コーシー列の極限」で構築されているから、コーシー列が分かれば実数そのものとして扱うことができる。 >>299 実数の構成に5つぐらいある、切断とか。それに同値なものを同じものとみなすこともよくやる。 例えば実数は体、順序構造、連続性をもつものとして定義する >>301 その存在示すのに、切断やコーシー列使うんやろ >>306 >>308 微積というよりも解析だな。 >>306 > だから存在をどうやって示すんだ こんな解析学の教科書の最初に書いてあることが分からずに実数論の講釈を垂れてた恥ずかしいやつ→ID:scEUff9F >>315 証明できないのならどの本の何ページに証明が書いてあるのか教えてくれ デデキント切断や完備化などが出てきても 有理数を既知として実数体を構成しているということが理解できない これでは数学書をいくら読んでもザルで水をすくうようなもの 横からだけど>>317 は 理系の大学数学(所謂現代数学)における論理展開の流れや 存在の証明とされるパターンが分かってないから、かなりの独学なのかな 始めの内は簡単な教科書を(定理部分だけ)拾い読みするんじゃなくて 書いてある文章や定義、証明を精読しないと論理展開が抜け落ちて話が通じないよ >>318 が書いてくれたか、任せた 存在論を厳密にやり過ぎるとクソどうでもいい心理学の信者が増える Q = 有理数の全体 Qの部分集合A, Bの組(A, B)で以下をみたすものをQの切断という A ≠ ∅, B ≠ ∅ A∪B = Q a∈A, b∈B ⇒ a < b Qの切断C = (A, B)に対して、論理的には次の4つの可能性がある (1) Aは最大元をもち、Bも最小元をもつ (2) Aは最大元をもつが、Bは最小元をもたない (3) Aは最大元をもたないが、Bは最小元をもつ (4) Aは最大元をもたず、Bも最小元をもたない この内、(1)はありえない なぜならば、Aの最大元をm、Bの最小元をMとすると、(m + M)/2は有理数でA, Bのどちらにも属さないから (2), (3)の場合は、有理数と対応する (2)と(3)で境界の数が同じものは同一視すれば、 (2)(3)型の切断全体と有理数全体が1対1対応する これと(4)型の切断の合併をRとする Rの加法、乗法を (A, B) + (A', B') := (A + A', B + B') (A, B) (A', B') := (A+ A'+, B B') (if 0∈A, 0∈A') := (B B'-, A+ A') (if 0∈A, 0∉A') := (B- B', A, A'+) (if 0∉A, 0∈A') := (A, A', B- B'-) (if 0∉A, 0∉A') で定める(境界を含む/含まないなどで不具合があれば適当に修正してくれ) Rは体になる((0)が極大イデアルであることを示せばいい) Rの半順序を (A, B) ≤ (A', B') :⇔ a∈A, b'∈B' ⇒ a < b で定める ≤は全順序になり、Rは順序体になる ただし A + A' := {a + a' : a∈A, a'∈A'} A+ := {a∈A : a > 0} B- := {b∈B : b ≤ 0} (仮定、前提、公理として)存在しているものから(公理的)集合論操作で構成したものは存在する、 これは自明の理として存在証明のOKパターンな事だけ補足しておくよ >>301 >例えば実数は体、順序構造、連続性をもつものとして定義する これは数論とか超準解析とか特定の用途でご都合定義や対比で採用(完備(非)アルキメデス順序体)する位で well definedかどうかの議論は本来は必要だし>>302 のツッコミが入るのは当然 >>320 >存在論 そう言うのが寄り付かないのが現代数学の良い所の1つかも >>325 ご苦労さん、実数の公理があるだけなんで証明するものではない ポエム連投しか能が無いのに、かっこつけで数学の話してみたら秒でボロが出るザコ(笑) ま、何だな。近年の計算機ってさ内部2進数か稀に十進数 であり、絶対に絶対にゼッタイに内部3進数はないよな で、本題。何で、地球の計算機ってさ -27の1/3乗はエラーにならず-3って答え出せるの❓ ちなみに、-27の0.33333333乗はダメだった。 1/3と0.33333333333…5 の差は如何なるεより小さいのか❓ 地球人って数学もコンピュータもどっちも、ズルしてるな🥳 いずれ量子コンピュータの時代になるから コンピュータ=2進数のイメージはすたれていくだろうな >>340 明らかに成り立たないし、そもそもnが定義されていなかったり問題として成り立ってない カリー・ハワード対応 (Curry-Howard correspondence) は、数学と計算理論の分野で重要な関係性を表す概念です。この対応は、論理学と型理論の間の深い関連を示しています。 カリー・ハワード対応は、次のような三つの分野間の関係を表しています。 1. 論理学: 論理的な命題や証明体系 2. 型理論: プログラミング言語や計算の型システム 3. 圏論: 数学的構造を研究する分野 これらの分野の対応関係は次のようになります。 1. 論理学の命題や証明は、型理論の型とプログラムに対応する。 2. 論理学の証明の形式は、型理論のプログラムの構造に対応する。 3. 圏論における対象や射は、型理論における型や関数と対応する。 この対応関係は、論理学の証明とプログラミング言語のプログラムの間に類似性があり、その間の数学的な形式的関係を示しています。これは、プログラムの正しさや証明の正当性を検証するための形式手法に関連しており、特に依存型や型理論に基づく証明支援系で重要な役割を果たしています。 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 が数学の主張として異なるということが理解できないということ? それとも、問題に不備があったことを素直に謝罪できない性格だということ? 奇数次ならかならず符号が逆転するので偶数次 x → x + aと変換して、奇数次の項消してけばいいよ 平方完成で a(f(x))^2n + b(g(x))^2(n-1) + ... + c(h(x))^2 + d の形にはできる a, b, ..., c, dが正の数になることがわかればいい >>388 ,389 問題自体は高校数学 大学レベルの隙の無い回答を求められているけど 妥協して高校基準でも 0点 ∀x, P(x) ≥ 0なので、最高次の係数はかならず正 a(x + A)^2n + bx^2(n-1) + ... の形にできる b ≥ 0ならOK b < 0ならどうする? ∀x, (x^2 + a)^2 - x^2 ≥ 0 となるようaをとってみる x^4 + (2a - 1)x^2 + a^2 = (x^2 + a - 1/2)^2 + a^2 - (4a^2 - 4a + 1)/4 a ≥ 1/4ならOKなのでa = 1/4とする x^4 - 1/2 x^2 + 1/16 = (x^2 - 1/4)^2 4次の場合は (x^2 + A)^2 + (X + B)^2 + C^2 の形にできそう 6次は? 問題に不備があったら出題も採点も自分でやればいい それを自分でやってはいけないという思考それこそが他責思考である P(x)は実数係数多項式で、∀x∈R, P(x) ≥ 0が成り立つとする。 P(x)の次数は偶数。 ∵ 奇数なら、x → ±∞ どちらかの極限が-∞になるから。 deg(P(x)) = 2dとする d = 0のとき、P(x)は非負の定数Cなので、P(x) = √C^2と書ける。 2(d-1)以下の偶数次のR係数多項式では、 ∀x∈R, Q(x) ≥ 0 ⇒ Q = f_1^2 + ... + f_n^2と書ける が成立すると仮定する {P(x)|x∈R}は下に有界 十分大きなr > 0を取れば、|x| > rでのP(x)の値は、[-r, r]でのP(x)の値よりも大きくできる。 よって、P(x)は最小値m > 0を持つ。 P(x) = mとなるxをx_0 F(x) = P(x) - mとおく F(x)はF(x_0) = 0で、x = x_0で極小値をとるから、あるQ(x)が存在して F(x) = (x - x_0)^2 Q(x) となる。 Q(x) = F(x)/(x - x_0)^2は、次数2(d-1)以下でつねに非負だから、仮定より Q(x) = f_1(x)^2 + ... + f_n(x)^2 と書ける。 よって、 P(x) = (f_1(x)(x - x_0))^2 + ... + (f_n(x)(x - x_0)^2 + √m^2 と書ける。 二次式の場合は成り立つ x∈R^n Q(x) = txSx tは転置 とすれば、Sは実対称行列になるから、適当な基底変換Tで Q(Tx) = a_1(x_1)^2 + ... + a_n(x_n)^2 となるつねに非負なのは、∀i, a_i ≥ 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 はユーチューブの拾い物なだけだから https://youtu.be/gt5VVmztpak (そこでは別解がなされてる) >>398 Lean4で回答してくれても良いよ ある朝、男が牧場の近くを通った時、腕時計が壊れていることに気づきました。 牧場には、牧草の束にもたれて寝ている牛飼いがいたので、男は「今、何時ですか」と尋ねました。 すると、牛飼いは近くの牛の金玉を持ち上げて、「8時10分だよ」と言いました。 男は怪訝に思いながらも、お礼を言って牧場を後にしました。 その日の夕、時計を直した男は再び牧場のそばを通りました。 牧場には、朝の牛飼いが牧草の束にもたれて寝ていました。 男は牛飼いに「今、何時ですか」と尋ねました。 牛飼いは、やはり牛の金玉を持ち上げて、「5時30分だよ」と言いました。 男は自分の時計を見ました。時計は牛飼いの言うとおり、5時30分を指していました。 男は驚き、「どうして牛の金玉で時間がわかるのですか」と牛飼いに尋ねました。 牛飼いは笑って、「向こうの時計台を見ていただけだよ」と言い、牧場の向こうを指差しました。 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に対し abc+abd+acd+bcd=1 を満たす0でない整数の組(a,b,c,d)が無限に存在することを示せ 上流は70点位の擬似コードを 下流は隙のない100点のコードを求められる 商人なら主語を修正する 学者なら述語を修正する 中立ならどっちも修正するか、何も変えない 国際社会では日本はすっかり女性差別および児童ポルノ大国と見られている シリアやアフガニスタンと同列の人権後進国だと見なされている >>411 網羅できない理由の方が多いのに何故できる方に賭けてしまうのかね カリー・ハワード対応もそうだが >>415 お前の首の上につけているものはなんだw モビルスーツに手と足と頭があるのも網羅がしたいだけ カリーハワード対応の元でも 型の表現力の問題で大した命題は表現できなさそう 依存型をもつ言語が待たれる ただ、haskellにはカン拡張のライブラリがあるので圏論とは相性がよいのかもしれない 「Haskellには依存型がない」は「Cにはclassがない」と同じ形式だし 「数学だから違う」は数学の定理ではない 依存型がなければ、その上に型システムを構築したらいいのでは? やりたいことをやってる人は問題ないが必然的にこの道しかないみたいな考えはたいてい間違っている 型に複雑さ移動するだけで何も楽にならない むしろ難しくなる 「道具」には役に立つとか楽になるための道具という意味がなくもない 数学は道具ではないと言うべきだった ああっ、ナメクジみたいな篦が目の裏に浮かんでくる~っ!! 縁側と玄関の間に黒電話 渡辺さんワインを持って皆勤賞 ジャラランガ・ライスシャワー サッポー「楡の木陰に高島さん」~ダンディな占い師伝説 物理をプログラミングって シミュレーションじゃないだろ たとえば世界がライフゲームだとして、 ライフゲームのプログラムを実行するのと、 N手後や前の状態を求めたり、パターンを分類するのは 別のこと その辺が、πを計算するのに近似値がどうのこうの言ってる連中の誤解かも知れんな 本体と付属品が別なのは当たり前だが問題は 名詞に相当するものが本体で動詞やら形容詞やらは付属品というのは本当か? >>454 圏論や型理論を記述言語にする 結局、数学を記述できる言語が必要 プログラミングをプログラミングするといえばlispだろ ジェダイは可 一階述語論理(prolog)がやられたようだな やつは命題論理の次に最弱、プログラミング言語の面汚しよ 同じ入力に対して常に同じ出力をかえすのが数学の関数だからコルーチンは邪道 なんか圏論が万能かのように語る雑魚ってかならずいるよな そもそも関数型言語をやるうえで言論の知識なんて1ミリも必要ないわけだけど ∃.elim(h, (w) => ((hw) => q)) append (v: Vec t n) (w: Vec t m) : (Vec t (n + m)) := [] w => w x:xs w => x:(append xs w) >>466 元の概念(マイクロスレッドとかファイバ)は関数とは独立かもしれんがコルーチンの実装は関数のようだぞ pythonはジェネレーティブ関数とよび、c#のコルーチンも関数って書いてあった >>467 1ミリも関係ないもの同士がじつは同型だったみたいな感じ? 何もしてないのに同型 lambdaはghost componentを扱えるからな Idrisなどの関数型言語は、型推論とメタプログラミングによって増々レバレッジを得る 割り当てられたメモリの値を変更できる時点で数学はできない プログラミングは数学もできるしアルゴリズムも書ける 自由すぎても強力とはいえないけどな go to considered harmful 適度にバグりにくい制限があるほうが強力 基本はIOモナドとSTモナドで副作用を扱える let x = print 1 in x>>x>>x ↑これはIOモナド(1を改行して3回表示)。副作用を値のようにも扱える モナドはListとMaybeをベースに理解しろとあれほど言ったのに ∧_∧ / ̄ ̄ ̄ ̄ ̄ ( ´∀`)< オマエモナー ( ) \_____ | | | (__)_) モナドは副作用の繋げ方を定義しているだけで、副作用を起こしているわけではない OEISとか数学の数列をプログラミングしてるサイトだな project eulerを解くとき参考になった モジュラ計算はマルチコアに依存するからプログラミングではできない マルチコアの処理をするコードもプログラミングの範疇だが 大きいモナドはお父さん 小さい緋鯉はコモナドたち 面白そうに双対してる モンスターの位数は10^52ぐらいだから256ビット(10^77ぐらい)あれば表現できる >>501 知ってても役に立たない知識を自慢げに披露してどや顔する馬鹿 >半単純リー代数の分類も知らぬザコめが はじめに空間と場としよう エレメンタリーには場ありきだ 結論から言ってqは最大公約数的 pを取ると 盲目的崖っぷちに近い 1, 2, 3, と数えても とわに埋まらないものがある だから存在するとしよう ここで疑問じゃ それが本当に正しい解釈か? わたしたち 擬似的なストーリーに 惑わされてやしないか? なぜ、針の先端 のようなものから セメント流しこむのか? 本当にそれで合ってる? 種がわれた未来では 構成は簡単だ しかし本質は 未知に近い さて そもそもこれは何じゃ? 元はモジュロじゃ しかし全体はわからんから 一部だけ見る まず、トリビアル これが逆説的に難しい 何も出てこないから そこで変形する 近視眼的になる どこかに、綻び・縺れがあった それを回避した形じゃ これが柔軟な考え方を 可能にする儂らに 答えがわかれば カヴァーは簡単だ あとはまとめればいい 結論からいうとqは最大公約数的で全部の駅を合わせればいいんだな わかった。 なんか小難しいスレに迷い込んでしまった ここまでをまとめると、モナドはオワコンということでOK? >>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種類)されてるようだが OSがどうなってるのかとかよくわからんかった プログラミング言語も専用のがあるんかな 夢がひろがりんぐ google https://ionq.com/ どうプログラミングするのかは分からなかったw 言語はQ# / QuTiP /Qiskitなどがあるようだ QuTiPはpythonの延長で使えるらしい read.cgi ver 07.5.1 2024/04/28 Walang Kapalit ★ | Donguri System Team 5ちゃんねる