How to do Math in programming (34ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
9(3): デフォルトの名無しさん [sage] 2024/03/25(月) 00:03:34.00 ID:q4vXpy6m(1) AAS
数学者だって、自分の専門分野の数学をすべて論理学と集合論の公理から演繹したわけじゃないだろう
すでに理解したことやよく知られた事実は認めて問題を解いているはずだ
そういう柔軟性がほしい
つまり、認めてもいい仮説はその場その場で手軽に導入できるような言語設計がいい
その上で、そこから機械的に導けることの証明や、定義から直接わかる具体例の計算などを半自動でしてほしい
もちろん、コンピュータにやらせる以上、曖昧さのない構文は必要だろうが
def continuous_at(f: Real -> Real, a: Dom(f)) = forall({e: Real | e > 0},
exists({d: Real | d > 0},
forall({x: Dom(f)},
implies(abs(x - a) < d, abs(f(x) - f(a)) < e)
)
)
)
これよりもさらに手短に、見た目ももっと見易く
10(2): デフォルトの名無しさん [sage] 2024/03/25(月) 01:17:03.24 ID:YF7A8RJG(1) AAS
たとえば>>9のcomtinuous_atなんかも、一度書いたはいいけど実際に使うとなると、使うたびに、fの定義域が実数全体じゃない場合みたいな微妙な調整が必要になるんだよね
人間が考えたら時間がかかるような部分をコンピュータに助けてほしいのに、どうしても「知りたいのはそこじゃない」って部分に時間をかけなきゃいけない
13: デフォルトの名無しさん [sage] 2024/03/25(月) 11:24:25.60 ID:tzV2+lCA(1) AAS
>>9
量化した変数や条件式の評価は遅延させなきゃいかんから、コールバック地獄みたいになるのね
33: デフォルトの名無しさん [sage] 2024/06/10(月) 22:10:57.74 ID:TCmEQru+(1) AAS
>>9
同意
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.335s*