「エウレカ〜!」のあれなわけですけどね。
最初はなんだろうな〜 おはじきを長方形に並べて掛け算の対称性を調べるみたいなのか?
こういうわかった感覚は中毒性があるので、わかるまで考えるとかがくせになるわけですが、世の中には難しいものも沢山あるからなぁ。
わかってないものも結構多い。チコノフの定理とかは、まだ、「わかった!」って感じではないです。一つは選択公理に依存しているからだな。自然にある集合が、そうそう都合良く順番に並んでくれるものか的な。
ピタゴラスの定理とか三角関数の加法定理とかを図で*証明*するのも、五次元世界の冒険とか読んで育った世代なので、
空間がまっすぐとか限らないから間違ってる
とか思う人だったりします。「それでわかってしまうのはダメだろ」的な。
Agda は直観主義論理だから、証明できるなら決まった推論規則から成立するのでわかりやすいと言えばわかりやすい。でも、
その推論規則本当にわかってる?
特に単一化と正規化が入り混じったのは結構複雑でな〜 まぁ、信頼してるけどさ。
疑り深い人の方がわかった感覚を身につけやすいのかも。人のいうことを簡単に信じては自分でわかったことにはならないからさ。
No comments:
Post a Comment