X



How to do Math in programming
0001デフォルトの名無しさん
垢版 |
2024/03/21(木) 09:41:43.97ID:85WuJ+Bw
What is "mathematics in programming?"

Some well-known facts in mathematics are difficult to prove using a computer.
For example, the Leibniz series

1 - 1/3 + 1/5 - 1/7 + ...

is exactly equal to π/4, but calculating this series directly is impossible because it requires infinite computation.
However, from the theorems of analysis, this equality can be shown. Thus, if all these theorems are formulated in terms of logic symbols, the proof is reduced to a finite algorithm.

Some might say that a "proof assistant" or "theorem prover" would make this possible.
However, the language of proof assistants is too complicated to describe proofs of non-fundamental theorems, so proof assistants are used only to check proofs that have already been solved.
This is far from doing mathematics.

My question is where do mathematical ideas come from and whether programming can help yield them?
0005デフォルトの名無しさん
垢版 |
2024/03/21(木) 23:49:19.66ID:qInfXZgz
より直感的なシンタックスと、命題のインタフェースを簡単に変換できる機能がほしいな
0006デフォルトの名無しさん
垢版 |
2024/03/23(土) 09:58:52.52ID:vizf8omG
命題 → 型

偽 → ∅
not A → Hom(A, ∅)
真→ not ∅

AかつB → 直積A×B
AまたはB → 直和A⊕B

AならばB
= not A または B
= (not A)⊕B
= Hom(A, ∅)⊕B
~ Hom(A, B) ※ 真偽が一致する
0007デフォルトの名無しさん
垢版 |
2024/03/24(日) 22:31:53.90ID:XQMIeHSx
プログラムはバイト列にコンパイルされるから、すべてのプログラムは高々可算個になるのだが、なぜ非可算集合をふくむ論理を扱えるんだ?
0009デフォルトの名無しさん
垢版 |
2024/03/25(月) 00:03:34.00ID:q4vXpy6m
数学者だって、自分の専門分野の数学をすべて論理学と集合論の公理から演繹したわけじゃないだろう
すでに理解したことやよく知られた事実は認めて問題を解いているはずだ

そういう柔軟性がほしい
つまり、認めてもいい仮説はその場その場で手軽に導入できるような言語設計がいい
その上で、そこから機械的に導けることの証明や、定義から直接わかる具体例の計算などを半自動でしてほしい

もちろん、コンピュータにやらせる以上、曖昧さのない構文は必要だろうが

def continuous_at(f: Real -> Real, a: Dom(f)) = forall({e: Real | e > 0},
exists({d: Real | d > 0},
forall({x: Dom(f)},
implies(abs(x - a) < d, abs(f(x) - f(a)) < e)
)
)
)

これよりもさらに手短に、見た目ももっと見易く
0010デフォルトの名無しさん
垢版 |
2024/03/25(月) 01:17:03.24ID:YF7A8RJG
たとえば>>9のcomtinuous_atなんかも、一度書いたはいいけど実際に使うとなると、使うたびに、fの定義域が実数全体じゃない場合みたいな微妙な調整が必要になるんだよね

人間が考えたら時間がかかるような部分をコンピュータに助けてほしいのに、どうしても「知りたいのはそこじゃない」って部分に時間をかけなきゃいけない
0011デフォルトの名無しさん
垢版 |
2024/03/25(月) 08:46:28.85ID:e2d3VFLD
かと言って最初から一般的に対応しようとすると、典型的なケースで必要以上に多くの記述をしなきゃならんだろうね
0012デフォルトの名無しさん
垢版 |
2024/03/25(月) 08:59:06.31ID:e2d3VFLD
継承とかいう欠陥だらけのサブタイピングのしくみは、証明に置き換わってもいい

つまり、厳密にis aであることを証明しなければ継承できない
 &ポリモーフィックな関数は型の共通部分で動作が一致することを証明しなければ定義できない

そうすれば誰も使わなくなるか、使える能力のある奴だけが使うようになる
0013デフォルトの名無しさん
垢版 |
2024/03/25(月) 11:24:25.60ID:tzV2+lCA
>>9
量化した変数や条件式の評価は遅延させなきゃいかんから、コールバック地獄みたいになるのね
0014デフォルトの名無しさん
垢版 |
2024/03/25(月) 18:53:28.86ID:gEcAWv1u
証明を書き下すのが手間なのもあるが、数学のオブジェクトをプログラムで扱えるよう定義するのも相当手間だろうね

行列式→行列式を計算するのは簡単だが、置換を使って定義するのはめんどくさそう。置換群を先に定義しなければならない

リーマン積分→区間幅の最大値が0に収束するようなリーマン和の列すべてを考えなければいけない。

商空間で辺に沿って同一視した曲面とかもめんどくさそう。
0016デフォルトの名無しさん
垢版 |
2024/04/01(月) 00:51:33.03ID:1WSos/bD
>>14
数学を表現するための概念のサブセットも選ばないといけない
現代数学が公理的集合論で記述されることは誰でも知ってるけど、具体的な対象(たとえば実数など)を扱う時に、それが∅から始めてZFCで構成可能かどうかなんてことを意識している人はいない
おそらく多倍長整数と浮動小数点数くらいはあったほうがいい
0017デフォルトの名無しさん
垢版 |
2024/04/01(月) 00:58:01.06ID:1WSos/bD
あと、近年のスクリプト言語における型チェッカやJITコンパイラなどと同様に、
言語は同じでも、プログラミングをする処理系と、証明をする処理系をわけたほうがいいと思う

同じだと、たとえば自然数の2を、数値として評価するか、「0の後者の後者」のように展開するか、プログラマが書き分けないといけない
0018デフォルトの名無しさん
垢版 |
2024/04/08(月) 20:17:45.51ID:lvukj15+
パターンマッチングの構文もかなり柔軟じゃないと書きづらいだろうね

複素関数をf = u + ivと分解するとか、V^nの既定v_1, ..., v_nを取るとか、そういうのが頻繁にある
0019デフォルトの名無しさん
垢版 |
2024/04/08(月) 21:50:38.81ID:azze6O2m
>>10
必要なら小さく取り直す、とか
a ≠ 0としても一般性を失わない、とか
そういうの簡潔に書けるといいよね
0020デフォルトの名無しさん
垢版 |
2024/04/11(木) 19:11:04.51ID:0/pdO5wD
埋め込みによって元の空間とその像を同一視するとか、
解析接続によって部分領域上定義された正則関数を複素平面全体の関数とみなすとか、
そういうのはどうやるんだろうな
0025デフォルトの名無しさん
垢版 |
2024/04/12(金) 11:38:22.83ID:VfOiBAdh
>>24
False型の値を返すと、Falseが証明される
False型の値はない(FalseはType型の値)ので、真の命題からは返すことはできない
唯一返すことができるのは、仮定もFalseである場合のみ

これはXから∅への写像の集合

∅^X := {f: X -> ∅}

が、X = ∅のときのみ元を1個持ち、その他の時は空集合であることに対応
0029デフォルトの名無しさん
垢版 |
2024/04/19(金) 11:16:47.49ID:fuxAiCc1
何がしたいのかよくわからんけど、計算に時間がかかっていいなら色々と自動化できるんじゃね
プログラミング言語で細かく指示するのは欲しい結果以外の計算をはぶくためでもあるからな
そしてユーザーが欲しがる結果を言語を設計する時点で特定することはできない
0030デフォルトの名無しさん
垢版 |
2024/04/19(金) 12:06:54.47ID:0YEF9E1Q
まず代数計算は自動化したいよね

ほぼ定義を再掲するだけみたいな証明は自動で演繹できるようにしたい
全部が全部そうできなくてもいいけど、書き方に若干のルールを設ければ自動で証明できる範囲は広がるはず

型駆動でも、OOPでいうとこのデザインパターンを発見して、
>>10>>19みたいな微妙に命題を変形するようなのは楽に書けるようにしたい
レスを投稿する