Show newer

朝まで時間あるし以前購入した少し前から進めていた「集合論・入門 無限への誘い」(遊星社) をやろうと思う。この本、公理的集合論の成果に裏打ちされた素朴な集合論の入門本で面白い。特徴としては一般的な集合論の本とは異なり、背理法を用いる証明がなく全部直接証明するらしい。なんかコンピュータで証明するときって背理法は使いずらい印象(気のせいかも)があるので背理法を使わない証明に慣れると良さそうであり、定理証明に関心のある私に丁度相性が良さそうと思いこの本を選択した。

そして後から気づいたことに最終章に「順序数」の章がある。これは ACL2 を使うのに必要な概念で ACL2 の中でも特に理解が進んでない部分であり、正しく読破できた場合にこれが学べるのは大変有り難いことだ。また、集合論の入門の最後の章に設置されるような概念でありやっぱそんな簡単な概念じゃないんだなと納得もした(軽く概念を学んでフィーリングで使って順序数を使ってメジャー関数を定義してアッカーマン関数的なやつの停止性の証明をしてみたことはあるけどあんま釈然としてなかった)。

初等の数学のたいていの問題は一段階低いレイヤーに落としてから見上げれば簡単そうに見える。問題は実際にはさらに難しいということなんだよな。

数学Aで集合について習ったときに人生で始めて数学に面白みを感じたんだよな。主に極度に単純計算と図形問題が苦手だったというのがあるんだが。
もしかすると証明中心の数学なら実は多少はできるんじゃないかという気がしている。

Show thread

まあ、私は公理的集合論を学ぶ前であり集合論に入門している段階なんでほど遠いところにあるけどな。
集合論、数学者の証明の書き方について知れて勉強になる。

私は 1 + 1 が 2 だと足し算の意味を明確に定義すれば導くことができると知ったときは感動したんだ。きっと似たような感動を覚える人はたくさんいるはずだ。数学者が数学基礎論を求めなくても大衆は数学基礎論を求めるに違いない!

Show thread

数学基礎論を使えば 1 + 1 = 2 が何なのか 0 の 0 乗がは何故 1 なのか、その答えを導ける。しかし、数学者はそんなことは気にしないらしい。それでもコンピュータの上で定理証明をするには必要なはずだ。きっと数学基礎論は生き残れる!

Show thread

計算機科学の世界に数学基礎論はまだ生きている。数学基礎論の生き残りとして生きよう!

Show thread

これは数学基礎論の時代が到来したのでは(到来してない)

割り算→逆数の掛け算の変換と分配法則は覚えろとしか言えない気がしてきた、頭が悪い

自由な意志なるものがあるというのはまるで永久機関が実現できると主張しているようにしか見えないよ。

にしても、物体同士が相互作用することなんて科学的には自明なのにどうして己、そして人間もしくは動物に対してだけは例外だと思ってしまうんだろうね。これは自分を含めて本当に不思議な話だよ。

社会的な改善まで考えるのは僧の仕事であって私の仕事ではない。私がやるべきことはまず私と近くにいるあらゆる相互作用するものに対してだ。

Show thread

まあ、私に作用する SNS を使うのはなるべく控えた方がいいのは明かだろうな。なんでかっていえば相互作用が薄いからな。悪くいってしまえば制御でないからってことになる。SNS を通じて平和をーなんて考えている間があったら身近な対人関係について意識した方が遥かに良いのである。

Show thread

> といっても、現在私は私自身のことで手一杯なんでそんな真似事をできる状態ではとてもない。

しかし、これ自体が仏教的な意味で誤りであるというのもそうか。私に作用する存在に対してうまく接すること自体が私を変えることになるわけだから。

Show thread

そもそも、SNS で何かを発信しているという時点で悟りとはほど遠い状態であることは自明である。ただし、大乗仏教とは菩薩として悟りに達することなく人々の救済にまわることを優先したということだから SNS を使うお坊さんがいたとしてもなんらおかしなことではないのだ。

といっても、現在私は私自身のことで手一杯なんでそんな真似事をできる状態ではとてもない。

Show thread

もし希望があるとしたら上記について SNS を使うもの全てが正しく知るということだろうけどまあ無理だろうな。少なくとも 2500 年もの間成し遂げられなかったことだ。そしてそこが始点だと思うのも不自然でありそれより過去にも何人もが気づいてきただろうし、その後にも気づく人は大勢いただろう。しかし、人間(当然私を含む)は根源的に愚かであり少なくとも SNS を使用する人々全員がそのような域に達せられそうな希望がどうもない。

Show thread

私と違って数学方面から対の面白さをきっかけにして Lisp にはまる人もたぶんいるんだろうな。

Show thread

かつて私は Lisp は簡単だし覚えること少ないし超簡単じゃんって思ってた。でも現実としてはそんなことはない。たぶん私が Lisp を簡単だと感じたのはそれ以前に C 言語とか Perl とか学んでたのが大きい。そういう経験のあとに Lisp に触れた場合に限り Lisp が単純でかつ簡単だと思えるんだ。

Lisp の最重要概念(Clojure 使いはおそらく異を唱えるだろう)は cons であり、cons を理解するには事前に C 言語におけるポインタを理解していることが望ましい。しかし、それは私の辿った道であり他の人もそうしなければならないという理由はない。

本当の意味で適切な Lisp の教科書があるとしたらそれはいったいどういうものになるのか、まったく検討もつかない。

Show older
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!