How to do Math in programming

How to do Math in programming at TECH

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
「自分が初めて思いついた」という話題はどこから出てきたの？