How to do Math in programming

How to do Math in pr ..

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