26-07-18
ニコニコのAI予測でコメントを複製する機能が意味不明で良い。存在する意味が無い。
- 総再生数推移がこのまま線形的に勧めば、10年以内にマイナスに踏み込むから動向が気になる。
コンピュータは凪ある永遠の趣味なので、私は今後も続けられる。OB
素朴なコンピュータの使用ほど面白いことはない。何か特定の活動ではなく、コンピュータから派生する全だ。
少し前に型検査を自作してみて、理論的な部分も少し入門できた。型理論の研究者が素人から入門するまでをまとめてくれていて役に立ったので、気になるなら参考にすべきだろう。彼のサーベイ論文など全体的に著者本人の足跡を辿れるように線が引かれいてる物が多くて本当に有用だった。彼の指南無しで双方向検査を理解できるまではやれなかった。
訳して無機質に列挙してみた↓
1. 静的型付き関数型言語（Haskell推奨、OCaml/SML可）を習得する。代数的データ型を型の加法・乗法として、集合の和・直積に対応させて理解する。
2. ラムダ計算（STLC、Hindley-Milner）の型システムの構造を理解する。型推論アルゴリズムの習得は不要。
3. 依存型を持つ言語（Agda / Lean / Idris2 / Arend）を表層的に学習する。rewriteの概念と等式型に対する直観を形成する。厳密な理解は不要。
4. 型理論の記法を習得する。対象：シーケント計算・自然演繹の判断形式、横線記法、Γ、⊢、コロン、代入 u[v/x]。STLCの型検査規則（少なくともラムダバインダ関連）を暗記で再現できる状態にする。任意の新規構文に対して代入操作の定義を導出できるようにする。証明論（⊨等）の学習は不要。
5. 形成規則・導入規則・除去規則・計算規則・η-等価性・宇宙階層を理解する。
6. 入門的な論文を読む。対象例：oktt（宇宙部分を除く）、arXiv:2103.15408、quantitative type theory。双方向型検査の構造と、それが双方向である理由を理解する。この段階でelaborationや圏論に着手しない。
7a. **設計方面**：
- 圏論の基礎：前層、引き戻しを理解する。
- 証明論における「モデル」＝型理論における「意味論」の概念を理解する。
- デカルト閉圏（CCC）がSTLCのモデルとなる理由を理解する。
- 文脈圏を学習する（Andrew Pitts, *Categorical Logic* 第1–2章）。代入と文脈の圏論的モデル化を理解する。
- CwF（categories with families）を学習する。CwFが型の値への依存を記述でき、CCCでは不可能である理由を理解する。LCCC（局所デカルト閉圏）は非推奨：型が値に依存する本質を捉えておらず、対応する型理論が外延的。
- CwFの応用を学習する。例：QCwF（quantitative type theory論文）。QCwFがquantitative type theoryのモデルとなる理由と、消去に用いられる関手を特定する。
- Grothendieckファイブレーションを理解する。概括圏（comprehension category）を理解する。CwFおよびCwA（categories with attributes）の一般化として位置づける。
- CwFにおける各型（Π型・和型・積型）の表現を理解する。
- CwFにおける宇宙多相の表現を理解する。2種の定式化：CwU、およびN→CwFの関手にlift操作を定義する方式。
7b. **実装方面**：
- elaborationの概念を学習する。参照：Mini-TT、LambdaPi.pdf、arXiv:2105.14840。conversion check、spine、telescopeを理解する。
- de Bruijn index、de Bruijn levelを理解する。
- 簡易な依存型理論を実装する。要件：Π型、sum type、単変数・非ネストのパターンマッチング。検証：Leibniz equality関連の定理の証明、自然数の加法交換律の定義と証明。複雑なパターンマッチングには着手しない。
- 暗黙引数の脱糖と求解を実装する。参照：elaboration-zoo。pattern unificationの解決対象と実装を理解する。
- 多変数・ネスト許容のパターンマッチングのelaborationを実装する。検証：indexed赤黒木（色・黒高さを型にエンコード）の記述。forced patternの必要性を確認する。
- 型クラス、宇宙多相を実装する。
- 既存の定理証明器のコード・論文を読む。大規模：Agda、Arend、Idris2、Lean4。小規模：[ditto](https://github.com/ditto/ditto)、[sixty](https://github.com/ollef/sixty)。
私は7a,bの最初辺りまで理解できた。型理論は何を勉強するか迷走する時間が多いとネット上の雰囲気を感じた。
なので研究者がロードマップを作ってくれるのは本当にありがたいよね。そのおかげで型の使用については納得できた。型の実装は少し寝かせる時間を作ろうと思う。これを参照するまでは型エラーと実行エラーの違いについてもピンときてなかったんだよね。まさかschemeから関数型言語などと繋がって、それが数学の証明になったと思った瞬間に圏論と直観主義数学とλの大三角形が怪しげな天体を広げて,宇宙になっていくとは思わなかった。プログラミングの世界観とはλのファンタジーなのは言うまでもない。
直積や直和など、実際に触れないと認識がズレることなど、プログラミングで言われるタームの原典に強制的に触れないといけないので、定義のビタ当てが起きて、十分にやる価値はある。これをする前は悪い意味で哲学的な用語の使い方をしていた。反省
あとplfaもいいぞ！
agdaは証明支援系の中でかなり気に入ったモノだ。使ってみたら分かるけど、あまりにシンプルで構築的すぎる。だが理解するにはこれ以上ない。
やはり再構築はいい。明日死ぬと分かっても、再構築するだろう。知識とは受容ではなく、構築だから。暗記や言語化も、知識を構築する導線を強める訓練だ。
プログラミングにおけるIntやBoolが集合だと説明されるものが多かったが、圏論の入門書を一周した時点で納得できた。 agdaの記法と組み合わせるとかなり簡単だと思う。ただ素の脳容量を越える内容だった。前にブログに書いた気がする。 集合に条件を付与していって、プログラミングで使う型として見做す。実装で理想的な状態ではなくなるけど、何を見て作られた概念なのかは原典を当たることで納得できたのでよかった。
今世で情緒的な問題に決着が付くとは思わなかったから突然に克服できてしまって人生の絶頂に到達した。 躁鬱の周期的なものじゃなくて、もうかれこれ半年は平静が続いている。
私の脱出条件は
- 植物油、小麦粉を断つ
- 肉中心の食生活
- サプリで調整する(論文を参照し、勝ち残り方式で新規開拓し続ける)
私の気分は外部の変数を考慮しなくて良くなった。 前は嬉しいことが起きても、関係なく循環系が沈んでいるから気分が落ち込んでいた。今はその逆になっている。
うーん、控えめに言って素晴らしい成果だ。悲しいのはサプリや特定の食物を断つ思想は一般的じゃないのでフラットに話せないこと。 疲れ果てたおじさんなんかを見てると、taurineに会わないせいで今後の30年程を疲労し続けるのかともったいない。しかし一般倫理において、サプリメントを勧めたりできない。倫理観があるせいで人が自殺してる。私には誰も救えない！(絶望の素振り)。
他にも明確に効くものもあるけど、循環系から間接的に精神を安定させる方が私に向いてる。 一時的に効く薬って大抵は寿命を減らし、効果が局所的で気分が良くなるけど気持ち悪く、高価だ。
インデックス投資でも同じことを思っている。私も大学を地元脱出の詐欺的な交渉に使って、住まいが与えられた後にしめしめと中退したけど、別に無資格の高卒がやる仕事や無気力なバイトに惰性で興じようと、入金力さえ維持できればいつか金銭的に上がれる(マジで)。生活水準は低くしないといけないけどね。これ楽観だけど非現実的じゃない(現状は)。正直、恵まれていることよりも他人の金で生きる方が気持ち悪いんだよな。初めて給料を受け取った時、目が覚めるような感覚がしたのを覚えている。一瞬で脳が冴え渡り、オープンワールドが始まった。
世間一般は個人の資産形成の統計を見れば氷河期レベルの認識で止まってるけど、NISAが始まった2014年が分水嶺で、そこから始めてた人の結果を見るとインデックス投資は正しい資産形成の１つになっている(つまり現状は善)。難点は結果が十年単位で出るので、せっかちな人は理解できない。借金と逆のことが起きると説明すれば、身を持って理解できる人もいるかもしれない。
インデックス投資の情報が出回らない2014年以前に就職難やバブル崩壊に直撃した世代の絶望感なんて、今を生きる我々が理解できるわけない。 なぜ山上徹也が暗殺しようと凶行に走ったか？というか,40代overがなぜキチガイ事件を起こしがちなのか?の答えはそこにある。若い時期に資産形成する機会を20代の時期に剥奪されているからだ。インデックス投資をしていたことの結果が今出ているように、若い内に複利を作れなかったリザルトが反映されている。彼らは今は耐えるだけのために生きている。時代として仕方ないことだ。
資産形成として「若い頃から複利を作ること」が最良とされている。狂っている40代が狂っているのは、金融知識も広まってないし、就職難で金銭もない。成功者は家や子や高級車を持つ"べき"なので成功しても資産にならない。(そういう時代を生きていた人はリスペクトしないといけない。年寄りには優しくすべき)
リアルだと嫉妬対策とモラルのために金銭や投資の話はできないけど、ネットだと、、、まあしていいんじゃないの？全ての人の不幸の回避を願っているので、タウリンと複利についてはプッシュしたい気持ちがある。しかししつこいからこれで終わりにしよう。導線を考えて、こんなサイトを見てる人はいないけど笑
今、若い人は「金融資産を何十年も寝かせる猶予」という圧倒的な優位性を持つ。 これを無視するなんて、インデックス投資の金融リスクが霞むレベルのメリットなんだよな。あと5年もしたら寿命で死ぬ人がインデックス投資してもそんな意味ない。私もセベラル年くらい入金維持すればセミFIRE(週3の深夜バイトで資産が増えていく)くらいの射程だ。
俺と年齢が近い人は今後の米帝の覇権を祈りつつ、お互いに金策頑張ろうぜ(年齢非開示)(グータッチ)。