How to do Math in programming

How to do Math in pr ..

2:デフォルトの名無しさん
24/03/21 10:47:44.36 8aAFTiSh.net
fuck your asshole

3:デフォルトの名無しさん
24/03/21 11:56:07.97 etpddAIY.net
Theorem Proving in Lean 4　日本語訳
URLﾘﾝｸ(aconite-ac.github.io)
定理証明なら、今はCoqよりこっちなんかな

4:デフォルトの名無しさん
24/03/21 12:07:26.54 etpddAIY.net
依存型を使った定理証明入門
URLﾘﾝｸ(zenn.dev)
定理証明の流れは
命題を型に変換する
型がnon-emptyであることを示す
なので、実行時に型チェックすれば動的型付け言語でも証明はできるわけか
ただ、全称型とか存在型とかをどうやって表すのかがわからない

5:デフォルトの名無しさん
24/03/21 23:49:19.66 qInfXZgz.net
より直感的なシンタックスと、命題のインタフェースを簡単に変換できる機能がほしいな

6:デフォルトの名無しさん
24/03/23 09:58:52.52 vizf8omG.net
命題 → 型
偽 → ∅
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)　※ 真偽が一致する

7:デフォルトの名無しさん
24/03/24 22:31:53.90 XQMIeHSx.net
プログラムはバイト列にコンパイルされるから、すべてのプログラムは高々可算個になるのだが、なぜ非可算集合をふくむ論理を扱えるんだ？

8:デフォルトの名無しさん
24/03/24 23:10:41.69 p5jI7jhC.net
量化してるからだよ

9:デフォルトの名無しさん
24/03/25 00:03:34.00 q4vXpy6m.net
数学者だって、自分の専門分野の数学をすべて論理学と集合論の公理から演繹したわけじゃないだろう
すでに理解したことやよく知られた事実は認めて問題を解いているはずだ

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

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

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)
)
)
)

これよりもさらに手短に、見た目ももっと見易く

10:デフォルトの名無しさん
24/03/25 01:17:03.24 YF7A8RJG.net
たとえば>>9のcomtinuous_atなんかも、一度書いたはいいけど実際に使うとなると、使うたびに、fの定義域が実数全体じゃない場合みたいな微妙な調整が必要になるんだよね

人間が考えたら時間がかかるような部分をコンピュータに助けてほしいのに、どうしても「知りたいのはそこじゃない」って部分に時間をかけなきゃいけない

11:デフォルトの名無しさん
24/03/25 08:46:28.85 e2d3VFLD.net
かと言って最初から一般的に対応しようとすると、典型的なケースで必要以上に多くの記述をしなきゃならんだろうね

12:デフォルトの名無しさん
24/03/25 08:59:06.31 e2d3VFLD.net
継承とかいう欠陥だらけのサブタイピングのしくみは、証明に置き換わってもいい
つまり、厳密にis aであることを証明しなければ継承できない
　＆ポリモーフィックな関数は型の共通部分で動作が一致することを証明しなければ定義できない
そうすれば誰も使わなくなるか、使える能力のある奴だけが使うようになる

13:デフォルトの名無しさん
24/03/25 11:24:25.60 tzV2+lCA.net
>>9
量化した変数や条件式の評価は遅延させなきゃいかんから、コールバック地獄みたいになるのね

14:デフォルトの名無しさん
24/03/25 18:53:28.86 gEcAWv1u.net
証明を書き下すのが手間なのもあるが、数学のオブジェクトをプログラムで扱えるよう定義するのも相当手間だろうね

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

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

商空間で辺に沿って同一視した曲面とかもめんどくさそう。

15:デフォルトの名無しさん
24/03/26 01:22:14.15 D7UVXJYK.net
LEAN
URLﾘﾝｸ(lean-lang.org)
SageMath
URLﾘﾝｸ(www.sagemath.org)

今ならこの2つだな

16:デフォルトの名無しさん
24/04/01 00:51:33.03 1WSos/bD.net
>>14
数学を表現するための概念のサブセットも選ばないといけない
現代数学が公理的集合論で記述されることは誰でも知ってるけど、具体的な対象（たとえば実数など）を扱う時に、それが∅から始めてZFCで構成可能かどうかなんてことを意識している人はいない
おそらく多倍長整数と浮動小数点数くらいはあったほうがいい

17:デフォルトの名無しさん
24/04/01 00:58:01.06 1WSos/bD.net
あと、近年のスクリプト言語における型チェッカやJITコンパイラなどと同様に、
言語は同じでも、プログラミングをする処理系と、証明をする処理系をわけたほうがいいと思う
同じだと、たとえば自然数の2を、数値として評価するか、「0の後者の後者」のように展開するか、プログラマが書き分けないといけない

18:デフォルトの名無しさん
24/04/08 20:17:45.51 lvukj15+.net
パターンマッチングの構文もかなり柔軟じゃないと書きづらいだろうね

複素関数をf = u + ivと分解するとか、V^nの既定v_1, ..., v_nを取るとか、そういうのが頻繁にある

19:デフォルトの名無しさん
24/04/08 21:50:38.81 azze6O2m.net
>>10
必要なら小さく取り直す、とか
a ≠ 0としても一般性を失わない、とか
そういうの簡潔に書けるといいよね

20:デフォルトの名無しさん
24/04/11 19:11:04.51 0/pdO5wD.net
埋め込みによって元の空間とその像を同一視するとか、
解析接続によって部分領域上定義された正則関数を複素平面全体の関数とみなすとか、
そういうのはどうやるんだろうな

21:デフォルトの名無しさん
24/04/11 22:05:12.71 M3s07OXs.net
穴を掘って埋める、平安京エイリアン

22:デフォルトの名無しさん
24/04/12 07:06:54.14 mV7jaryD.net
LeanとIdrisはどちらが良い？

23:デフォルトの名無しさん
24/04/12 08:41:58.82 dWqcXhet.net
∅への写像は定義域が∅のときのみ存在するから
p→∅がpの否定を表すのね

24:デフォルトの名無しさん
24/04/12 09:44:04.06 sBlCiCbm.net
背理法って、Falseをreturnしたら全部示されるんじゃないの

25:デフォルトの名無しさん
24/04/12 11:38:22.83 VfOiBAdh.net
>>24
False型の値を返すと、Falseが証明される
False型の値はない（FalseはType型の値）ので、真の命題からは返すことはできない
唯一返すことができるのは、仮定もFalseである場合のみ
これはXから∅への写像の集合
∅^X := {f: X -> ∅}
が、X = ∅のときのみ元を1個持ち、その他の時は空集合であることに対応

26:デフォルトの名無しさん
24/04/12 12:30:58.16 Kw0ACNUt.net
boolean main()
{returnFALSE);};

27:デフォルトの名無しさん
24/04/12 12:47:01.19 trEYbdGK.net
「∅を返す」と「a∈∅となるaを返す」の違いがわからないのか？

28:デフォルトの名無しさん
24/04/12 15:02:42.13 /hR1sMGb.net
>>26
ここのFalseはブーリアン型ではない

29:デフォルトの名無しさん
24/04/19 11:16:47.49 fuxAiCc1.net
何がしたいのかよくわからんけど、計算に時間がかかっていいなら色々と自動化できるんじゃね
プログラミング言語で細かく指示するのは欲しい結果以外の計算をはぶくためでもあるからな
そしてユーザーが欲しがる結果を言語を設計する時点で特定することはできない

30:デフォルトの名無しさん
24/04/19 12:06:54.47 0YEF9E1Q.net
まず代数計算は自動化したいよね
ほぼ定義を再掲するだけみたいな証明は自動で演繹できるようにしたい
全部が全部そうできなくてもいいけど、書き方に若干のルールを設ければ自動で証明できる範囲は広がるはず
型駆動でも、OOPでいうとこのデザインパターンを発見して、
>>10や >>19みたいな微妙に命題を変形するようなのは楽に書けるようにしたい

31:デフォルトの名無しさん
24/04/19 12:59:19.99 wsMDWrIu.net
その平凡なアイデア思いついたのお前が初めてだと思うか？

32:デフォルトの名無しさん
24/04/19 13:58:03.23 3z6RQVPy.net
「自分が初めて思いついた」という話題はどこから出てきたの？