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
「自分が初めて思いついた」という話題はどこから出てきたの？
33:デフォルトの名無しさん
24/06/10 22:10:57.74 TCmEQru+.net
>>9
同意
34:デフォルトの名無しさん
25/04/27 16:18:53.10 rRExk4WB.net
日本語と英語と同じスレがあるのか
重複だからどっちか削除汁