How to do Math in programming

**デフォルトの名無しさん** · 2024/04/01(月) 00:58:01.06

あと、近年のスクリプト言語における型チェッカやJITコンパイラなどと同様に、
言語は同じでも、プログラミングをする処理系と、証明をする処理系をわけたほうがいいと思う

同じだと、たとえば自然数の2を、数値として評価するか、「0の後者の後者」のように展開するか、プログラマが書き分けないといけない

**デフォルトの名無しさん** · 2024/04/08(月) 20:17:45.51

パターンマッチングの構文もかなり柔軟じゃないと書きづらいだろうね

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

**デフォルトの名無しさん** · 2024/04/08(月) 21:50:38.81

>>10
必要なら小さく取り直す、とか
a ≠ 0としても一般性を失わない、とか
そういうの簡潔に書けるといいよね

**デフォルトの名無しさん** · 2024/04/11(木) 19:11:04.51

埋め込みによって元の空間とその像を同一視するとか、
解析接続によって部分領域上定義された正則関数を複素平面全体の関数とみなすとか、
そういうのはどうやるんだろうな

**デフォルトの名無しさん** · 2024/04/11(木) 22:05:12.71

穴を掘って埋める、平安京エイリアン

**デフォルトの名無しさん** · 2024/04/12(金) 07:06:54.14

LeanとIdrisはどちらが良い？

**デフォルトの名無しさん** · 2024/04/12(金) 08:41:58.82

∅への写像は定義域が∅のときのみ存在するから
p→∅がpの否定を表すのね

**デフォルトの名無しさん** · 2024/04/12(金) 09:44:04.06

背理法って、Falseをreturnしたら全部示されるんじゃないの

**デフォルトの名無しさん** · 2024/04/12(金) 11:38:22.83

>>24
False型の値を返すと、Falseが証明される
False型の値はない（FalseはType型の値）ので、真の命題からは返すことはできない
唯一返すことができるのは、仮定もFalseである場合のみ

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

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

が、X = ∅のときのみ元を1個持ち、その他の時は空集合であることに対応

**デフォルトの名無しさん** · 2024/04/12(金) 12:30:58.16

boolean main()
{returnFALSE);};

**デフォルトの名無しさん** · 2024/04/12(金) 12:47:01.19

「∅を返す」と「a∈∅となるaを返す」の違いがわからないのか？

**デフォルトの名無しさん** · 2024/04/12(金) 15:02:42.13

>>26
ここのFalseはブーリアン型ではない

**デフォルトの名無しさん** · 2024/04/19(金) 11:16:47.49

何がしたいのかよくわからんけど、計算に時間がかかっていいなら色々と自動化できるんじゃね
プログラミング言語で細かく指示するのは欲しい結果以外の計算をはぶくためでもあるからな
そしてユーザーが欲しがる結果を言語を設計する時点で特定することはできない

**デフォルトの名無しさん** · 2024/04/19(金) 12:06:54.47

まず代数計算は自動化したいよね

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

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

**デフォルトの名無しさん** · 2024/04/19(金) 12:59:19.99

その平凡なアイデア思いついたのお前が初めてだと思うか？

**デフォルトの名無しさん** · 2024/04/19(金) 13:58:03.23

「自分が初めて思いついた」という話題はどこから出てきたの？

**デフォルトの名無しさん** · 2024/06/10(月) 22:10:57.74

>>9
同意

**デフォルトの名無しさん** · 2025/04/27(日) 16:18:53.10

日本語と英語と同じスレがあるのか
重複だからどっちか削除汁