GCD

冬休みのプログラミングです。Automaton の授業の例題に√2が無理数ってのをやろうとしていたらしいんだが...

　　gcd26 : (n m i : ℕ) → 1 < n → 1 < m　→ gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )

という簡単な部分で停まってます。割り算なんだけど、全部引き算で実装するわけなんだが、

　　gcd1 : ( i i0 j j0 : ℕ ) → ℕ
　　gcd1 zero i0 zero j0 with <-cmp i0 j0
　　... | tri< a ¬b ¬c = j0
　　... | tri≈ ¬a refl ¬c = i0
　　... | tri> ¬a ¬b c = i0
　　gcd1 zero i0 (suc zero) j0 = 1
　　gcd1 zero zero (suc (suc j)) j0 = j0
　　gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
　　gcd1 (suc zero) i0 zero j0 = 1
　　gcd1 (suc (suc i)) i0 zero zero = i0
　　gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))　j0 (suc j0)
　　gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0　

　　gcd : ( i j : ℕ ) → ℕ
　　gcd i j = gcd1 i i j j

と簡単なんだが、四つの引数の制約が足りないようだな。対称性とかは示せたんだが。

これができると、√2の他に素数が無限にあることとか、そんなのが証明できるはです。

そんなことをしながら大晦日か。

256番

ぴったり感のある番号のバスですが

　　意地でもゆいレールと北谷/沖縄市を結ぶ路線は出さない

という感じですかね。56番のてだこ浦添止まりなんだが、

　　既存路線を短くして自慢する

ってのは面白いな。

浦添前田の接続の56番の終バスは真栄原止まりとか、いろいろ面白い。

もっとも、最近は那覇にはあまりでないわけですけどね。

〆

特に区切り感ない人なのですが... 仕事納めは昨日だったらしい。でも、うちのゼミは火曜日。

ハリーズ開いてるのか説もあったんですが、ちょっと両方で様子見してしまったか。

　　ちゃんと予定を聞こうぜ

学生は人数頼まないととか言ってましたが、いや、10人分とか頼むのは前もって言っておかないと。

一応、お店は昨日までだったらしいです。また来年、よろしくお願いします。

ゼミもお休みではあるのだが、危なさそうなB4/M2には見ようかな。

久米のチャコ

今年のシス管はシステム更新で大変だったので、打ち上げは「チャコでステーキ食おうぜ」で。先月の話ですが。

なんか写真取る方式の検温計が。

　　やってる感が出てよろしい

レアで頼んだんですが、10oz じゃぁ、ミディアムにしかならんか。

まぁ、昔の味は思い出補正があるからな。BSE騒ぎで日本のステーキは割と残念になった気がする。

宜野湾も10時まで

さすがに、那覇浦添沖縄市には文句がついたか。いや、飲んでもバスがあるのは良いかも。意味あるのかとか言ってる人もいるけど、

　　確率だから、時間を短くすれば減る

ま、ゼロにはなりませんけどね。いや、本気度が足りないんだよな。中国や韓国みたいに「二週間封鎖」みたいにすれば解決なんですが。

武漢であれだけ猛威をふるっていたものが収まっていることは確かなので、まぁ、そうすれば良いだけのものらしい。

　　でも、できないもんだよね。いや、「やらない」ですか。

素粒子物理とか、ソフトウェアのバグとかと同じで

　　確率の低いところが問題になる

のは現代的な気がする。そういう時代なのだな。

個人に対してがんばれと言えばなんとかなると思ってるあたり、この国は戦時中と変わってないのだとも思う。

Agda apkg はだめ

結局、DivMod 通らないので apkg はあきらめ。とりあえず、Homebrew から入れなおし。

Solver とか面白いんだけど、

　open AlmostCommutativeRing ring
　-- The solver is flexible enough to work with ℕ (even though it asks
　-- for rings!)
　lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
　lemma₁ = solve-∀

こいつって、Data.Nat じゃないんだな。これを Data.Nat に引き戻す方法がわからない。

もっとも、もっと、ずっと簡単にできる方法がある気もする。

いや、~/.cabal が悪さをしていたらしい。削除で解決。

Google Cloud Directory Sync というそびえたつくそ

LDAP と Google のアカウントを同期するって奴なんですが...

なんか学生が苦労しているので... なんと、

　　Java 8 なアプリで、Browser 立ち上げて認証

で、Ubuntu で動かないとおっしゃる。今までは Windows なPCで動かしていたらしい。

どうせ xdg-open で開けてるのだろうと思ったんですが、そんなんでは動かないらしい。

　　Java 8 だからな

なので、

　　捨てるのが良いらしい

です。代わりは CSV でやれと? 本気?

対角線論法とHalting Problem

対角線論法は割と簡単に(やっと)書けたのだが、Halting 問題の方は良くわからない。

　　 Bijection TM (List Bool)

自体が矛盾するので、 TM = List Bool → Bool にしないで、そのうちの encode を持つものみたいに限定するのだろうな。
で、halt が encode を持つとすると矛盾くらいか。いや、そう書こうとしているんですが...

record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)　where
　 field
　　　 fun←　:　S → R
　　　 fun→　:　R → S
　　　 fiso← : (x : R)　→ fun← ( fun→ x )　≡ x
　　　 fiso→ : (x : S ) → fun→ ( fun← x )　≡ x

open Bijection

diagonal : ¬ Bijection　( ℕ → Bool ) ℕ
diagonal b = diagn1 (fun→ b diag) refl where
　　¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
　　¬t=f true ()
　　¬t=f false ()
　　diag :　ℕ → Bool
　　diag n = not (fun← b n n)
　　diagn1 : (n : ℕ ) → ¬ (fun→ b diag ≡ n )
　　diagn1 n dn = ¬t=f (diag n ) ( begin
　　　　　 not diag n
　　　　≡⟨⟩
　　　　　 not (not fun← b n n)
　　　　≡⟨ cong (λ k → not (k　n) ) (sym (fiso← b _)) ⟩
　　　　　 not (fun← b (fun→ b diag)　n)
　　　　≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
　　　　　 not (fun← b n n)
　　　　≡⟨⟩
　　　　　 diag n
　　　　∎ ) where open ≡-Reasoning

年内の授業は終わり

でも、あんまりめどのついてない修士のためにゼミはやるかとか考えてます。オンラインだしな。

OSの教科書は、今年は手に入りやすいものと考えて、

AN INTRODUCTION TO OPERATING SYSTEMS: CONCEPTS AND PRACTICE
https://www.amazon.co.jp/dp/B085B1W656

を使ってるんですが、微妙な感じ。問題が Review Question とかやさしいものが分離されてる。まぁ、それもいいか。

タネンバウム先生のも良いんだが、なにせ問題が「メインフレーム」だったりするからな。

いまどき、ハードウェアとかOSとか流行らないよ的な意見もあるかも知れない。でも、プログラミング技術的な興味もあるし。

キャンパスバス実証実験

まぁ、いろいろひどい。琉大からてだこ浦西を結ぶわけですが...

　1. そもそも遠隔授業で学生があんまりいない
　2. 終バスが18時前。修士で18時前に帰るなんてありえない。朝は来ないし。
　3. 北口からてだこ浦西までは高速バスで3分なので琉大には意味がない
　4. 真栄原までは98/広栄からは125とかぶり
　5. 北口までなので東口の文系や病院の人は使えない

そもそも需要がずれてる。足りないのは

　A. ゆいれーるからの遅い時間の接続

てだこ浦西のバスは21時にはもうない。ゆいれーるは0時着がある。浦添前田は22:39があるが真栄原止まり。

　B. ゆいれーるから330/58の接続

このバスは確実に宜野湾営業所から来る。なのに、58号線からは人は乗せない。

　C. 琉大から沖縄市への接続

長田の乗り換えは200m歩く。誰も乗り換えてない。

まぁ、沖国からは便利かも。本数の少ない125の代わりにはなる。真栄原から大学へのバスの本数が増えることにはなるな。

スタバから琉大に直接行ける。

琉大生はバスがあんまりに不便なので、だいたい車で通うから。

http://www.watta-bus.com/news/detail.php?news_id=156

西原

たまに ingress で廻るわけですが、西原サンエーまでバスで行って、お昼ご飯と思ったが、

　　予想通り、ベトナム料理屋さんは開いてない

どうせ、そうだろうと思ってたよ。どうしようかってところなんですが、サンエーまでも戻ってもたいしたものがあるわけでもなく。

そういえば、大典寺から登る手がある。ぐぐったら、48分。48分であの坂登るのか。あぁ、まぁ、上原からバスに乗る手があるか。

で、ローソンで適当にすませて、坂を登りました。

トポロジー

なんとなく来年はチコノフの定理やろうと思っていたのだが少し書いてみました。

record Toplogy　( L : HOD ) : Set (suc n) where
　 field
　　　 OS　　: HOD
　　　 OS⊆PL :　OS ⊆ Power L
　　　 o∪ : { P : HOD }　→　P　⊆ OS　　　　　 → OS ∋ Union P
　　　 o∩ : { p q : HOD } → OS ∋ p →　OS ∋ q　→ OS ∋ (p ∩ q)

これは filter に似てるな。

record Filter　( L : HOD　) : Set (suc n) where
　 field
　　　 filter : HOD　
　　　 f⊆PL :　filter ⊆ Power L
　　　 filter1 : { p q : HOD } →　q ⊆ L　→ filter ∋ p →　p ⊆ q　→ filter ∋ q
　　　 filter2 : { p q : HOD } → filter ∋ p →　filter ∋ q　→ filter ∋ (p ∩ q)

実際、コンパクトが超フィルターが集積点を持つことに対応するらしい。量は多いけどできそうな感じ。

別に集合でやらなくても良くて束上でやるとか自然数上でやるとかでも。ただ集合論も基数できてないし、トポスもやってないし。

群論も正規部分群とかやってないんだよな。いろいろ老後の楽しみがたまっていく感じ。

パイプライン伊祖近辺

パイプライン道路は、昔、米軍基地へのパイプラインがあった通りらしく、自分が来た頃は、まだ残骸が残ってました。

人が通るわけじゃないから、上下動お構いなしで、ジェットコースターみたいな感じ。それが好きで通る先生も。

なんですが、だいぶ整備されて割と普通な道に。ここも、だいぶできたきた。車線増やすのだろうな。まぁ、バイパスのさらにバイパス的な。

その先の低くなっている辺りは、雨が降ると水没するあたりですが、それはなんとかなったのか?

介そばとスタンプラリー

パイプラインの嘉数のところにあります。バスが遠いから、なかなかいけないが、

　　Ingress のついでなら

割と普通に美味しい。で、なんか、

　　沖縄そばスタンプラリー

なるものが。しかし、名護とかですか? バス派には、ちょっと厳しい感じだな。

でも、我如古のは行ったことがない。今度いってみよう。

これって公式サイトみたいなのはないのか。

GCC cross compiler on Homebrew

単に自分で拡張した GCC10 な arm cross compiler を作りたいだけなんですが...

問題は ARM tool chain と GCC 10 の pthread.h がずれているかららしく。いや、prefix と読むべき header の位置がずれてるとかも。

そんなわけで、libgcc のコンパイルを通すことはできないらしいので、

　　　File.open("make.sh", "w") { |f| f.write "\#!/bin/sh\nmake \"$@\"\nexit 0\n" }

と必ず成功する make の shell wrapper を通すことに。こんなんで良いらしい。tool chain 自体は brew install -s すれば良いだけだらしい。

そもそもの問題は作った gcc が system 側の as を参照してしまうことだったんですが、どうも hard coded されてるらしく、

　　　"--with-as=#{arm}/bin/arm-none-eabi-as","--with-ld=#{arm}/bin/arm-none-eabi-ld",

と、こちらも hard coded で対抗すればよろしいらしい。LLVM はこういうクソな問題ないので、LLVM だけにしてしまいたいです。

GCC側

単に cross compiler 作れば良いだけなんだけど。clang 側は割と簡単に片付いたんですが、

　　GCC側が libgcc.a 作るところでこける(pthread関係)

いや、そんなもの要らないので、他は make -k でできるので良いんですが、

　　brew install

が許してくれない。くそ〜 macOS 上で作ってる好き者はあんまりいないしな。そもそも install 先をこそこそ見たりするし。

ま、ふっとできるかも知れないです。

hgweb date of Mercurial

久しぶりに LLVM いじったら、brew update から始まって環境設定に2時間... 恒例の Mercurial の hgweb の date の表示の修正です。

なんで、2 weeks ago とか 2 month ago とかだすのか理解できないです。2年前以上は日付がでる。ぜんぶそうしろよ。計算できないのはアメリカ人だけだから。

hgweb.config で指定できるべきなんだろうけど。ちなみに、hg もやっと Python3 に対応したらしい。全部のファイルが10%ずつ変更なので、つらいのはわかる。
pycompat なんてのがあるのか。

　　+firefly+one diff -c templatefilters.py　templatefilters.py.orig　
　　*** templatefilters.py　Mon Dec 14 19:40:36 2020
　　--- templatefilters.py.orig　　 Mon Dec 14 20:47:18 2020
　　***************
　　*** 86,93 ****
　　　　　　　　　return b'in the distant future'
　　　　　else:
　　　　　　　delta = max(1, int(now - then))
　　!　　　　 # if delta > agescales[0][1] * 2:
　　!　　　　 if delta > agescales[3][1] :
　　　　　　　　　return dateutil.shortdate(date)
　　　
　　　　　for t, s, a in agescales:
　　--- 86,92 ----
　　　　　　　　　return b'in the distant future'
　　　　　else:
　　　　　　　delta = max(1, int(now - then))
　　!　　　　 if delta > agescales[0][1] * 2:
　　　　　　　　　return dateutil.shortdate(date)
　　　
　　　　　for t, s, a in agescales:
　　+firefly+one diff -c templates/static/mercurial.js templates/static/mercurial.js.orig
　　*** templates/static/mercurial.js　　　 Mon Dec 14 18:31:49 2020
　　--- templates/static/mercurial.js.orig　Mon Dec 14 17:23:04 2020
　　***************
　　*** 293,301 ****
　　　　　　　　　　　　　　　　　　return "in the distant future";
　　　　　　　　　　　　　　}
　　　　　　　　　　}
　　-　　　　　　　　 if (delta > (scales.day)){
　　-　　　　　　　　　　 return shortdate(once);
　　-　　　　　　 　　}
　　　
　　　　　　　　　　if (delta > (2 * scales.year)){
　　　　　　　　　　　　　　return shortdate(once);
　　--- 293,298 ----

getArgs 解決

やっぱり「落ち着いてやればできるだろ」と思い直して。

Data.Text.Text とか言ってるので、getArgs が Text (おそらくutf8)を返しているんだろと思ったんだが、実は、

　　grep Text MAlonzo/**/*.hs | more

したら、

　　MAlonzo/Code/Agda/Builtin/String.hs:type T6 = Data.Text.Text

とかやってて、Compiler が Agda の String を Haskell の Data.Text.Text に変換してるわけね。そうといわかれば、

　　open import Codata.Musical.Notation
　　open import Data.Maybe hiding (_>>=_)
　　open import Data.List　
　　open import Data.Char　
　　open import IO.Primitive
　　open import Codata.Musical.Costring

　　postulate
　　　　getArgs : IO (List (List Char))
　　{-# FOREIGN GHC import qualified System.Environment #-}
　　{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

　　main : IO ⊤
　　main = getArgs >>= (λ x →　putStrLn $ toCostring $ sym5solvable $ getNumArg1 x )

という感じで、 IO (List (List Char)) で受ければよいと。

Monomorphic な Agda では Monad の修飾構文はよろしくないらしく、直接、getArgs >>= (λ x → と書くのが残念な感じ。

Agda の getArgs

五次の交換子を計算すると終わらないってのに気がついたんですが、

　　なんと、Agda から Haskell にコンパイルすると瞬時に終わる

それだと計算結果を証明に使えないのだが... まぁ、いろいろあるな。

で、そうすると、引数渡したくなるわけですが、

　　postulate
　　　 getArgs : IO (List String)
　　{-# FOREIGN GHC import qualified System.Environment　　#-}
　　{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

とかしろとあるわけですが、まったく動かないです。IO coString だったりとか、getArgs が Data.Text.Text になったりで
おいていかれているっぽい。github 上の getArgsの例題が軒並み動かない。

まぁ、コンパイルするような言語じゃないからなぁ。

Portal Scan

なんか、ポータルが点灯してるのでinsgessのNEWSみると Scout がどうたらと。ぜんぜんわかんないのでさらにぐぐったら、

　　Portal Scan しろ

と。え〜　あれ、周りの動画を撮るとかなんだよな。時間かかって面倒くさいだけ。気持ちはわかる。

　　Portal 周りの動画を集めて AR みたいなのをしたい

ってことでしょ? でも、携帯回線で動画の upload なんてしないです。しないよ。

まぁ、動画撮って、あとで Wifi のある所で送信とかなら。ただで仕事させるなら、もっと餌が良くないと。メダルだけではね。

ガロア理論一段落

一段落詐欺はいろいろあるわけですけどね。プロシンのネタので、締切前に終わっていたはずなんだが、まぁ、良くある。

残ってたのは順列の数え上げと交換子の数え上げがちゃんとできてるどうか調べるだけなので簡単だったはずなんだが....

順列の数え上げ自体は簡単で高校生でも書けるプログラムなわけなんですが、結構、難航。Fresh List の慣れもあるかな。

普通プログラムって何通りも書き方があって、まぁ、だいたいどれでも動くわけ。ところが、Agda だと

　　停止性とか、順序の正しさ、そして、全部入っていることを確認する方法

とかが全部つながってないとダメ。つまり、かなり特定の方法、再帰に特化した方法で書くことが必要らしい。

結局、三四回書き直す羽目に。でも、図書いて、ちゃんと再帰になるように書いたら、ぐっと短くなった。で、できあがり。長かった。

交換子の数え上げの方は任意のFresh List二つの組み合せに抽象化できるらしいんですが、ちょっと書き方がわからなくてやってません。

ガロア理論と言っても正規拡大体とかやってないけど、Agdaはむしろそっちの方が得意かもな。圏論に近いから。

来年は、チコノフの定理やろうかな。集合論あるし。Filter で圏論的にやるなんて言う手もあるらしい。

そんなわけで、詳細は、オンラインで開催されるプロシンで話します。

https://github.com/shinji-kono/Galois

空中戦

なんか、緑の新人さんに刺激されたのか、連日、緑になったり青になったり...

まぁ、一応、緑の時は壊しにいきますがね。

それにしても元気だな。

Agda の演算子の構文によるエラー

中置演算子を定義できる言語はいろいろあって面白いんですが、Agda の自由度はかなり高い。

　　C [ f ≈ g ] = Category._≈_ C f g
　　infix　4 _[_≈_]

で圏Cでの等号定義できる。これを使うと複数の圏の演算を混ざるとか平気でできます。三項演算子だ。しかも二項演算子を三項に拡張してる。

この _ のところに変数が来るわけだな。 この記法は圏論でも使われてたりします。
さらに syntax というのがあるらしいが、まだ使ってません。

equality 自体も _≡_ という二項演算子で

　　data : Set } :　(x y : A) → Set　where
　　　refl　: {x : A} → x ≡ x

なんですが、これを x ≡_ みたいに使える。

　　x ≡_ = λ y → x ≡ y

(x ≡_) y が x ≡ y になるわけなので正しく curry 化されてるわけ。 なのだが、

　　_≡_ x　と _≡ x と x ≡_

と三種類書ける。どれも構文エラーにならない。 　　_≡_ x　と x ≡_ は同じ。

x ≡ y と　y ≡ x は同じなので、どれでも良いと思ったし、動いてたんですが、昨日、突然、

　　annot instantiate the metavariable _491 to solution section
　　since it contains the variable section
　　which is not in scope of the metavariable
　　when checking that the inferred type of an application

というわけわかエラーが。いやなにいってるんだかわらないんですが。でも、いろいろ削ってだめなところを抜き出したら

　　_≡ x と x ≡_ との違いだった

どっちかに統一すれば解決。なくなく 60 箇所くらい修正する羽目に。いや、Emacs の Keyboard macro でできるわけなんだが...

　　x ≡_ = λ y → x ≡ y
　　_≡ x = λ y → y ≡ x

なので、確かに違う。しかも通る場合がある。しかし、結局は通るはず。しかし、エラーは出る。なるほどわけわかりません。

いや、混ぜた自分が謎でもあるのだが...

健診

なんか延期になってたらしく。封筒が入ってたんですが、外注にだしただけらしく、

　　日付も場所も書いてない

で、ググってみたが保健センターのWebには何も書いてない。

メールを検索してみると日付は書いてあって来週らしい。しかし、

　　場所がわからない

中にあるリンクのpdfをクリックすると、巨大ファイルのダウンロードが...

そこに大学会館三階と書いてありました。

PDFのテキストだけ抜き出して表示するのを mh には組み込んであるのだが、URLのリンクを自動展開するようにしてないからな。

この

　　テキストに書くことができない障害者

たちをなんとかいて欲しいです... 罫線とか色の付いた四角とか幼稚園のお絵描きじゃないんだから、簡潔に文章で伝えて欲しいよ。

ほら、そこの学生、レポートをスクショでだすのはやめるんだ。

最近のコード検索

普通に検索すると、もうゴミばかりで... 間違ってるコードのページをコピーして大量に広告をはったページばかり。

忘れてた自分が馬鹿なんだが、サーバ側が IN_ADDRANY で待つのをすっかり忘れてて... サーバを gethostbyname で待つクソコードに引っかかってました。

https://www.example-code.com/csharp/ssl_server.asp

ここの方が少しましか。検索以前のInternetに戻ってしまったようだな...

github で動いているコードの中を検索した方がましかも。もっとも、C# で github ってのはそんなにないか。

通知

iPhone の通知はほとんど切ってるので平和なんですが、

　　シス管ミーティングをすっぽかす

という問題が。でも、入れるとかなりの量が... MatterMost の Channel 毎になんとかできるようんだが...

いちいち設定が面倒くさい。vi で設定させろって感じです。

まぁ、なんとかなるかな。

Facebook/TwitterのDMが確実か?

Calendar

iCloud のカレンダーが、まったく連携してくれなくて。まぁ、

　　あんまりスケジュール関係ない

人なんだが、割と不義理が... あと、遠隔授業な時代に推薦で休講日とか知らんし。いや学年歴のGoogle Calendar はあるんだが。

いろいろ見てみるんだが、やっぱり、Apple のが全然駄目だな。Goolge Calendar は諦めて、この前、入れたので、それから見えるらしい。

と思ったら、

　　Google Calendar から iCloud にloginできる

ぐ。それかあ。いやだから

　　最近、Goolge 嫌いなんだけど。

でも、まあ、仕方ないか。それで一応見れるみたい。でも、iPhone のCalendar はアイコン上の日付だけ便利なのでおいておこう。

ギガ

11/29まで 10GB 余ってるだったんですが、大学の帰りにポータルとろうとしたら、なんか落ちる。

　　iijmio の容量がゼロ

なんだよ。統計見るんですがresetさぼってたので良くわからない。しかし、

　　app store が 3.5 GB

とか。いや、そいつの Wifi は切ってるんだが。と思ったらばっちり on 。お前か。

この前の iOS update か、自分で何かの理由で入れたか。なんか Wifi から勝手に携帯に切り替える余計な機能とかあるらしいが。

11/30の夜だったので、12/1 になれば6GBにはなったので問題ないんだが「俺のギガを返せ〜」とは思いました。

使い切ると特に遅くなるらしく。まぁ、Twitter/MatterMost には影響ないので ingress 以外はどうってことありませんでした。

相対論関係

こんな感じ。この前にダメな本に結構引っかかってます。ブルーバックスとか、岩波新書のとか。

特殊の方は行列で不変直線ならったら「それ光速度不変じゃん」で計算するとローレンツ変換がでたのでうれしくて、なんか文章書いてたな。

そこまでわかってから他の本を読むと楽勝。

一般相対論はディラックの読み会があって、そこでだいたい。その後、復習もやった。

ただ、結局、どう計算するってところになると「作用でやれ」で、え〜な感じ。シュバルツシュルト解までだな。

結局、アインシュタインの本が良いんじゃないですかって思う。

マックスウェルの方程式を共変性が明らかな形に書き下すところからですね。

4次元運動量がエネルギーと運動量に射影されるとか感動だったな。