How to do Math in programming

**デフォルトの名無しさん** · 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

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