Agda 2.6.1 update

なんか再帰的定義の途中の置き換えを見てくれないので、少し困ってるんですが、もしかすると

　　update するとなおるかも?

前に報告したバグも「最新版で試せ、たこ」ってなことだったので、

　　pu ~/src/public/agda
　　make
　　cabal install --disable-documentation --builddir=./dist-2.6.1 --enable-tests --disable-library-profiling -fenable-cluster-counting　--force-reinstalls
　　pu ../agda-prelude
　　git pull
　　pu ../ataca
　　git pull
　　pu ~/src/public/agda-stdlib
　　cabal new-exec -- GenerateEverything
　　make
　　cabal new-install

問題は「どれがうまくいった原因か良くわからん」こと。

さらに、 ~/.emacs.d/init.el の
　　(load-file (let ((coding-system-for-read 'utf-8))
　　　　　　　　　　　　(shell-command-to-string "~/src/public/agda/dist-2.6.1/build/agda-mode/agda-mode locate")))
　　(add-hook 'agda2-mode-hook
　　　　　　　'(lambda ()
　　　　　　　　　(setq viper-mode t) (require 'viper) (viper-mode)
　　　　　　　)
　　)
　　(custom-set-variables
　　 '(agda2-program-name
　　　 "/Users/kono/src/public/agda/dist-2.6.1/build/Agda/agda"))

をなおす必要があるらしい。ここを変えないと古いのを見てしまう。

さらに vim では、 ~/.vim/filetypes.vim の

　　au BufNewFile,BufRead *.agda setf agda
　　let g:agda_extraincpaths = ["/Users/kono/src/public/agda-stdlib/src","/Users/kono/src/public/category-agda"]

ここらしい。

あと、もちろん、/usr/local/bin/agda を ~/src/public/agda/dist-2.6.1/build/Agda/agda にしないとだめ。

これを update のたびにやるかと思うと気が重いです。まぁ、そんなものなんだけど。

ハッカーズチャンプルー

会場が文系のビルだったので、かなり探しました。留学生のビルに人がいるので聞いてみましたが、その

　　ドアにはってある地図がそれっぽい

ので助かりました。

内職する気で来たんですが、思ったより話が面白い〜

腐女子から外資系へのジョブチェンジな話とか、小学生の時に30日OSやってたお嬢さんとか。売上50万円だった Doorkeeper の話とか。

零細なWeb Service って面白い。

http://hackers-champloo.org/2019/

ソウエイシャ

嘉数の50's cafeの後にできたカフェです。広くて良いが Wifi はない。

　　テザリング使えないauのSIMを選択した＊馬鹿＊ by void (そういうことを言って楽しい奴)

なので、ちょっと困る感じ。ちなみに au から docomo に乗り換える方法はないらしい。まぁ、電話番号にこだわりがあるわけでもないですが。

カレー頼んだけど、レトルトっぽかったな。他のメニューはどうだろう?

ここはプチエトワールが閉まっているとはまるので、何か開いているだけでうれしいので頑張って欲しいところです。

twitter archive

ZFまだ混迷中なんですが、twitter にはその格闘の痕が... 「こうすればできる」とか書いたはずなんだが、

　　twitter書きすぎててさかのぼれない

なので、twitterの設定からarchiveを取ってくるってのをやります。何年か一度やってます。

でも、今回は CSV が付いてきた。ふーん。Excel で見たりするのか? というわけで、それようの script を書いてみました。

　　#!/usr/bin/perl
　　open my $less,"|-","less";
　　select $less;
　　$/ = "\"\n\"";
　　while (<>) {
　　　　my @d = split(/","/);
　　　　print $d[3],"\n";
　　　　print $d[5],"\n\n";
　　}

2019-06-24 11:17:01 +0000
楕円軌道をおそらくは累積法で計算することができたらなら、逆自乗まであとほんの少しだったはず。そしたら、ケプラー力学と呼ばれていたかも。

2019-06-24 11:12:41 +0000
ケプラーのすごさは楕円だけじゃなくて、ケプラーの法則、つまり惑星が変速するってのも含んでいるところ。まぁ、周転円は変速を説明するものなんだから当然なんだけど。超計算し
まくっていたからできた。そろばんとか暗算とかあっても驚かない。

2019-06-24 10:02:04 +0000
院試はそこそこ勉強しましたよ。量子力学の摂動法とか出たし。フランス語とかも。どこにそんな時間があったのか不思議なんだが。マイコン少年で半分ソフト会社にいたのに。

slow ssh connection on IPv6

学内でサーバにアクセスする時に「IPv6だと遅い」とかの話が。ずーっと前からそういう話は出てたんですが解決しないでいたんですが、

　　何故か新規にチケットが...

シス管の学生に聞いてみると、気にしてないのが半分、IPv6切ってるのが半分。ちょっと、やってみてで、

　　ssh -v の認証のところで待つ(一分はないけど、20秒は待つ)

じゃぁ、DNS引いてみて。dig AAAA でも特に遅くはなく。でも、reverse ptr が怪しい感じ。しょうがないな、

　　ssh ipv6 slow connection

ぐらいでググってくれる? で、Gassip がどうのとかいろいろ出るんだが、

　　sshd で UseDNS no しろ

ってのが。まぁ、試してみるか。systemctl restart sshd で、最初は待ったんですが、

　　IPv4 と同じ接続速度に!

なんと解決ですか。おそらくIPv6の逆引きの問題だろうなぁ。

パパド

インドの豆の煎餅で油で揚げて食べます。簡単なんだが...

　　油断したら、鍋から煙が出てる...

火を止めて、パパドを一つ放り込んだら

　　こげこげに

危なかった。昔、火柱上げた奴もいるんだよな。

火がついてもコンロを止めれば停まることも。野菜でも放り込めば停まることが多いです。

箸を突っ込んであわが出るとかもあるんだけど状況によっては出ない。まぁ、一枚、入れてみれば良いんだが。

そんなことを学んでもらう機会ですね。今回はインド人たちが活躍してましたが。そこでノウハウを聞くべきなんだがあんまりできなかったかも。

Oculus Quest

VR系なB4がいるので買ってみました。カレーパーティに持ってきていたので、ちょっとお試し。

卓球なんですが、そもそもリアル卓球苦手なのにVRでできるわけない。サーブできれば成功的な感じ。

三次元酔いはあんまりない感じ。広さがあるのは良いんですが少し危ない。転んでいる人がいました。

決まった領域からでるとカメラがonになって、外が見える仕組み。これは、前のOculus Goより良い。

Standalone で動くので、対応するPCを問わないのも良い。Unity にも対応しているらしい。

なんか研究ネタあるのかな。VRでプログラミングとかもあるらしいですが...

カレーパーティ

インド人達と楽しく料理してます。(どっちかというと自分は疲れて横になってる

　　カシューナッツと豆腐のカレー
　　ほうれん草とナスのカレー
　　チャナ豆のカレー
　　ダル豆のスープ
　　サブジ
　　ビリヤニ
　　チャツネ
　　ムリカス
　　コフタ (野菜団子?)
　　ムリカス (大根サラダ)
　　パパド
　　チャパティ

チャパティは15時からかな。全部野菜にしました。ビリヤニは人参と玉ねぎだけ?

カレーパーティの準備

というよりは、インターンのプレゼンを見るので、ちょっと疲れ果てたかも。うちの研究室のやり方を学ぶのが良いかどうかは謎ですが、

　Web slide

を使ってもらいました。その方が自分が修正するのには楽。MindMap 書いてもらって、

　Presentation は story telling だから Happy end で

みたいな感じでやってもらうんですが、自分でちゃんと Slides 書けるようになるのは珍しいかも。英語の適切なお手本なかったしな。

自分で手を入れるのは躊躇しない方なのでそうしましたが、実際に話してもらうと、

　割とそれっぽい

インド人らしい早口だけど。伝えたいのだったら、ゆっくり話して。日本人に速い英語は無理だから。

Presentation 書くのはだめだけど、Presentation 自体は上手という人がいるんだよな。そんなわけで、割とお疲れだったかも。

あぁ、でも英語な学生が研究室にいるのは良いなぁ。楽しいです。

カレーはとりあえず三つは作りました。ビリヤニってどう作るんだっけ? メイドインアビスなみの怪しいものを作ってしまうかも。

qemu-arm cpu cycle count

明日はカレーの準備をしているはずです。もしかすると、vegetarian menu にしてしまうかも。

最近のCPUだとclock countを返してくれる命令があったりするんですが、ARMだと実メモリアドレスの特定のところにあるらしく。

わざわざ、xv6 でPTE書いてマップしたにも関わらずカウンタが動かない。ググってみると、

　　実装されてないかも

あぁ、qemu-system-arm だからな〜　単に、適当に時間計りたかっただけなので、tick count でいいかな。

Docker〜

インド人には、arm xv6 in docker をいじってもらってるんですが、

E: Failed to fetch http://archive.ubuntu.com/ubuntu/pool/main/q/qemu/qemu-system-common_2.0.0+dfsg-2ubuntu1.44_amd64.deb 404 Not Found [IP: 91.189.88.162 80]

おいおいおいおい。

ちょっと前までは動いていたんだけどな。(港のヨーコ風に)

そんなこともあろうかと、OS server上には Docker でない qemu-system-arm と cross compiler 一式が用意されてます。

クラウド信用するとかするわけでないでしょ。でも、この docker image 結構複雑なんだよな。もっとも古いからなぁ。また Docker hub quest?

課題は、xv6 に priority を入れるだけど、まぁ、

　　予想通りに難航

かなり単純なものだけど、Cの初心者は、ここでつまづくでしょ的なものを一通りみれました。qemu上のarmに接続した gdb で。

健診

早起きして朝食抜きで受けてきました。

人間ドックも行ったことあるんだけど、あんまりコスパ良くない感じ。はずれな時ははずれるわけだし。

職場健診は無料だけど、検便(=大腸がん検査)は入ってない。昔は入っていたんだけどな。

　身長体重ウエスト血圧血液レントゲン心電図検尿視力聴力

あとはアンケートと触診だけ。超音波もなし。安い。

この手のものは検査しまくっても意味ないものもあるので、適当にさぼっているくらいがちょうどいいかな。

Web Certificate

例の https にしろと言ってくるうるさい奴ですが、update の季節らしく、シス管がいろいろやってくれてます。

なになに、Fortigate のVPNがCertificate違うとか言ってくる? あぁ、そういう文句を言うためのものだからなぁ。

国立大学だと Sinet のなんかがあるらしく、取りまとめて配布とかになっているらしいんですが、

　　手続きが面倒くさいので、Let's Encrypt を使っているところがある

ことが判明。うーん、別に良いんじゃないの? それでいいなら、

　　全部、それにしちゃえば?

いや、うちは、https にしてなかったりするんだけど。VPN とか言われても ssh tunnel だし。

学生に、どうなの? と聞くんですが、はっきりとした答えは返って来ず。まぁ、そうだよな。

html 自体に署名しないで、web server に証明書をもたせる辺りがなぁ。

英語のお話

技術分野やアカデミックだと英語と中国語が文化的に必須なんだけど、どうも、学生はそう思ってないらしく。

でも、最近増えてきたミャンマーとかネパールの人と何語で話すかって問題もあるんだよな。

学生は楽観的にずーっと日本にいるから良いと思っているのかも知れないけど、今後の日本に「日本語の通じる国」ってのは期待しにくい。

でも中学高校大学と10年も費して、まだ英語が使い物にならないってのは、学生のモティベーションの問題だけでもなくて、

　　先生側も話せなくて良いと思っている

ことが大きい。大学で英語の教科書を選択してない先生に「なんで英語の教科書にしないんですか」と聞いてみると良い。

まぁ、でも語学が堪能な学生でも沖縄に戻ってきていたりしてな〜 無駄な抵抗かもな。もっとも、

　　韓国は日本と同じ状況だったが、通貨危機後に劇的に英語能力が上がった

と言う先例が。もちろん、それまでに話せなかった人が急に話せるようになるはずなく、

　　通貨危機後の世代は英語ができる

という状況になってる。日本も結局はそうなるんじゃないかな。

在学中に英語5000ページ読めって言ってるんですけどね。OSの教科書は1000ページくらい。

Ingress First Satudary 7/6

7/6 八重瀬町役場 14:00から17:30 参加無料、申し込み不要

だそうです。東風平ですね。昔のResistanceの南部の傘作戦を思い出すな。

2月に那覇でやったばっかりな気がするが年二回ぐらいがいいのかな?

Ingress は歩くのが好きだった僕には相性が良く、しつこくやってます。単なるお散歩よりは目標があって良い感じ。

つるむ感じじゃないのが合ってるかも。ポケモンは人を集める感じだからな。でも、2,3人で廻ると鍵集めの効率が良い。

沖縄だと大汗かきますが、まぁ、それが良いと言うことかな。

初心者歓迎イベントでもあるので、これからやってみるのも良いかも。RecursionしたベテランのAP稼ぎにも良い。

現在 Lv11 ですが、これでLv12に上がるんじゃないかな〜

https://fevgames.net/ifs/event/?e=12950

カフェユニゾン

普天間基地の向こう側は Ingress 的に重要なので。工事の関係らしく58号線が大渋滞。

　　なので、ゆっくり Ingress できました

ユニゾンでは「いつものように行き詰まってる」ZFをいじってました。どうも今まで作っていたのはODの中の順序数らしい。

帰りに森川公園に寄って、そこから歩き。ちょうど良い感じかな。

Made in Abyss

なんか学生が Netfelix で見つけたらしく、面白いとか言ってるので。そういえば、録画したはずだよな〜

先週言ってもらえればNetflixで見れたのに。

手元のindexで探すんだが見つからない。最後の日付は 2017/9? あ、そこから何もしてないですか。

BD-R/RE のplaylistを html に変換するツールを持っているので、それで index を作ればよい。 48枚入り3冊分。

まぁ、一冊一時間もかからないので。で、どこにあるかはすぐに見つかったんですが... この頃、かなりやる気なかったらしく、

　　アニメとしか書いてない

のはまだ良い方で

　　真っ白

なんてのも。せめて番号書けよ的なところもあるんだが、番号通りに格納されるとは限らず...

まぁ、そういうのが楽しいからやってるわけだけど、やる気ないなら Netflix で良いんじゃないの?

というわけで。まだ、Made in Abyss は見てません。そんなに好きな絵柄ではないけどな。

ZFの方は「∀x∋Φ」としていたのに気がついてしまって、まぁ、それでもZFのモデルにはなるんだが、それだと選択公理の時に困るので、やり直し中です。

http://www.ie.u-ryukyu.ac.jp/%7Ekono/pub/software/rpls.pl

那覇の消防隊〜

久茂地の交差点で見かけました。サンダーバード的だが、

　　なんかクレーンみたいなのが付いてるだけ?

放水塔かな?

6/23 カレーパーティ〜

やろうかなと。きっと、インドの留学生が手伝ってくれると思うので。

参加人数の見積りは相変わらずどんぶんり勘定ですが、まぁ、なんとかなるでしょう。

今回は、ベジタリアン向けのものになるはずですが、完全に肉抜きにはしない予定です。

mixi の外部ブログ

もはやどうでも良いんですけどね。まだ、何人か mixi に書いている人がいるので。

たまに見てる https://mixi.jp/new_friend_diary.pl とかは、おそらくは本来はアクセスできない場所なのかも。

http://http://teeda...

みたいなURLになってる。

タイムラインから見る方が正しいんだろうな。リンクボタンだけだけど。

人数の少なさが良いという人もいるんだろうな。blog は自分のために書くものだし。

ZF 一段落

順序数のの sup (上界 ∀x∈X ψ(x)<sup ψ) だけでは足りなくて、

　　x<sup ψ → ∃y x≦ψ(y)

を入れたら Power Set までできました(これはなんだろう?)。5/8から始めたらしいのでだいたい1ヶ月だな。

最初は inductive record で書こうとしていたようですが、ZFは一階述語論理だから平坦なrecordで十分。

これで Agda で定義された順序数Ordinalと順序数定義可能集合OD、そして、若干の仮定(ODとOrdinalの順序同型と上界と上のやつ)
で、ZFのモデルを作るところまでできた。

集合論の本だと構成可能集合を使ってZFのモデルを作るあたりまでに相当します。その後、選択公理と連続体仮説やって、
さらに強制法で選択公理と連続体仮説の成立しないモデルを作るわけだな。まぁ、そのうちにやるかも。

一階述語論理だと有限個のAxiomでは記述できないとか、ψ(x,a1,a2,a3,...,an) とかの不便があるんですが、高階直観論理なAgdaだと、

　　その辺の問題は全部普通に有限な関数で記述できる

すごい。高階論理偉大すぎる。数学の本と違って構文がはっきり決まってるし。「明らかに」とか省略されているところないし。

ZFを仮定して、その仮定を絶対性とか言いながら、対象となるZFの方を <v,∈> |= ψ x みたいに書くとか、やっぱりつらい。

というわけで全体的に簡単になってます。それでいて、元の集合論のモデル構築の基本的な筋には沿っている。
なので集合論の復習にもなりました。

選択公理は順序数との順序同型があるのでいけるはずですが、 結局、L は使わなかったので、連続体仮説はどうかな。

Twitter を振り返ってみると「わからん」とか「できない」とか言ってる翌日に「わかった」とか「できた」とか書いてる。そんなものらしいです。

Power Set

ZF の続き。ある集合Aの部分集合全体の集合、冪集合ですが、普通に論理式で定義してしまうとだめ。

しばらく、まったくわからなかったんですが、冪集合の公理が置換公理抜きでできると書いてるのはコーエン先生の本だけで、他の本は全部置換公理を使ってる。さらに、構成可能集合が部分集合の集合に等しいらしい。

部分集合自体は

　 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
　 ZFSubset A x =　record { def = λ y → def A y ∧　def x y }　

と言う形で集合の and で定義してやればよい。部分集合全体は、この x を「可能な集合全部」でUnionを取る必要がある。超限帰納法かと思ったんですが、

置換公理は sup と同じなので sup (上界)で良いんじゃないか? と思いついたら、

　　Def :　{n : Level} → (A :　OD {suc n}) → OD {suc n}
　　Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )　

　　-- Constructible Set on α
　　L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
　　L {n}　record { lv = Zero ; ord = (Φ .0) } = od∅
　　L {n}　record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
　　L {n}　record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
　　　　record { def = λ y → osuc y o< (od→ord (L {n}　(record { lv = lx ; ord = Φ lx }) )) }

と言う感じで構成可能集合まで一気にできました。

冪集合の公理は「ある集合に属するとAにも属するなら、その集合はAの部分集合」

　　 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t

なんですが　t ∋ x → A ∋ x があるので、t がA 部分集合であることが言えて、 Power A が上界なことから言えるようです。

反対側の「Aの部分集合に属するならAにも属する」 の方

　　 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x

こっちは ZFSubset A ? ∋ t が見つけられれば ZFSubset A ? ∋ x → A ∋ x で言えるんですが...　

Power A に含まれるなら、部分集合のどれかに含まれるってわけなんですけどね。最小性入れてないのでできない。どれかは構成的には探せない。

最小性入れても良いのだが、入れないで置換公理と同等なようなので入れないでできる方が望ましいかな。L を使うのかも。

というわけで、まだできてません。

Netflix 休止

うっかり更新してしまったんですが、

　　まったく観なかった

あぁ、まぁ、そういうものだよな。

Startrek ぐらい観ないのか。いきなりのクリンゴン語モノローグで挫折的な感じです。

学生たちの方が観てるかも。

交換留学生

一ヶ月ぐらいインド人の学生が滞在してくれるそうです。OSに興味があると。

　　OS、そんなに人気ないし、劇的な進歩もないよ

と言ったら別な分野があればみたいな。いや、そうじゃなくて、そういう賃貸した分野が意外に次の発展があったりするもの。

で、彼女の Mac Book Air にいろいろ入れていくんですが...

　　TreeVNC
　　Mercurial
　　zsh
　　slideshow (markdown から html)
　　Docker
　　
Docker 上には、xv6arm をdebugするための gcc cross compiler / qemu-system-arm / gdb for arm

Docker は一発なんだけど、それまでがな。

Pro3 な学生とか、うちの学生とかにいろいろやってもらうんですが...

　　お前ら、英語ぐらいちゃんと話せるようにしておけ!

ってところです。何人かは頑張ってました。

ZFの方は置換公理は(仮定)一発だったんですが、冪集合側は難航してます。いや、いままで難航しなかったところなんてないんだけど。

集合論(無限の公理)

無限公理、少し苦労したんですが終わりました。AgdaのInternal Errorに泣いたがバグレポしたら最新版でテストしろと。まぁ、そうだよな。でも、最新版についていくのはつらい。

置換公理は仮定で入れてしまったので、残りはPower Setだけです。他も苦労したので、これも苦労するはずです。

順序数の方程式としての順数定義可能集合OD(本来はその推移的な部分集合)でZFのモデルを作るわけですが細かいところが面白かった。

順序数には直後順序数というのがある。つまり、Suc ですね。Suc を積み重ねても次のレベルにはいけないがどの順序数にもある。

Suc には割り込めない。つまり、x と Suc x の間にある元はない。ということは、

　　Suc x ∋ y なら x ≡ y ∨ x ∋ y

なるほど。つまり、これを順序数のSucについて証明して間にある元がないということを証明できました。そうしないで、順序数から割り込みがないことを示すのは難しい。

でも、そこで順序数の定義を複雑にし過ぎてきたことに気がついた。レベルのある自然数で十分らしい。

　　data OrdinalD {n : Level} :　(lv : Nat) → Set n where
　　　 Φ : (lv : Nat) → OrdinalD　lv
　　　 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv

　　record Ordinal {n : Level} : Set n where
　　　 field
　　　　 lv : Nat
　　　　 ord : OrdinalD {n} lv

　　data _d<_ {n : Level} :　 {lx ly : Nat} → OrdinalD {n} lx　→　OrdinalD {n} ly　→ Set n where
　　　 Φ<　: {lx : Nat} → {x : OrdinalD {n} lx}　→　Φ lx d< OSuc lx x
　　　 s<　: {lx : Nat} → {x y : OrdinalD {n} lx}　→　x d< y　→ OSuc　lx x d< OSuc　lx y

　　_o<_ : {n : Level} ( x y : Ordinal ) → Set n
　　_o<_ x y =　(lv x < lv y )　∨ ( ord x d< ord y )

これだけで十分らしい。レベル間の相互作用がまったくないけど、それでいいのか。

なんとなく、ZFの公理に引きずられてUnionとかを論理式で定義ししそうになるんですが、それではだめらしい。あくまでも、

　　集合の構成は順序数の大小関係で定義する

方式。 x ∈ Union X は、Suc x < X みたいな感じ。Pair も実は、

　　Max ( Suc x , Suc y )

だった。無限公理には、x ∈ infinite →　 x ∪ { x } ∈ infinite というのが出てくるけど、

　　{ x } (xだけを含む集合) は、pair で ( x , x )

要素二つの A ∪ B は Union (A , B) なので、結局、

　　Union (x , ( x , x )) ∈ infinite

と言う形に。z ∈ Union (x , ( x , x ))

　　 Suc z < Suc ( Max ( Suc x , Suc x ) )

になるので、結局、

　　 z < Suc x

に。そして、z < y という条件のODは、y という順序数に対応する集合そのものなので、Union (x , ( x , x ))　は、

　　 Suc x という順序数に対応する集合

ということになり、無限集合の公理は、x が含まれていれば Suc x が含まれている集合が存在するということになるということでした。

ただ、これを Agda で丁寧に変換していくので、結構、大変でした。残りは冪集合(Power Set)だけだが....

-

MatterMost

Slack 割と使ってますが、容量にぶつかる先生も。有料のどうかなと思って見てみましたが...

　　在学生だけならなんとか
　　卒業生いれると無理

ですよね。なので、Open source なMatterMostとかいうのが。これがくりそつだ。これでいいなら、これえいいんですが。

もっとも、マストドンっぽい感じもあるな。

https://mattermost.com

ZF集合論の続き

集合論の本だと、

　　ZF集合論の公理 → 順序数 → 構成可能集合 → ZF集合論のモデル

ってな手順です。今回は、

　　ZFの公理の Agda の record を作る
　　順序数(Ordinal)を data で構築する
　　集合を順序数定義可能集合(順序数上の方程式)として定義する
　　集合と順序数の対応を仮定する (ゲーデル数/ゲーデル集合)
　　上界(Sup)を仮定する
　　集合論のモデルを順序数を使って構築する

ってな手順です。公理は

　　 pair : ( A B : ZFSet　) →　( (A , B)　∋ A ) ∧ ( (A , B)　∋ B　)
　　 union-u : ( X z : ZFSet　) → Union X ∋ z → ZFSet
　　 union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
　　 union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z)　∧ (union-u X z X∋z ∋ z )
　　 _⊆_ A B {x} = A ∋ x →　B ∋ x
　　 A ∩ B = Select A (　λ x → ( A ∋ x ) ∧ ( B ∋ x )　)
　　 empty :　∀( x : ZFSet　) → ¬ ( ∅ ∋ x )
　　 power→ : ∀( A t : ZFSet　) → Power A ∋ t → ∀ {x}　→　_⊆_ t A {x}
　　 power← : ∀( A t : ZFSet　) → ( ∀ {x}　→　_⊆_ t A {x})　→ Power A ∋ t
　　 extensionality :　{ A B : ZFSet　} → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)　) → A ≈ B
　　 minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
　　 regularity : ∀( x : ZFSet　) → (not : ¬ (x ≈ ∅)) → (　minimul x not　∈ x ∧　(　minimul x not　∩ x　≈ ∅ ) )
　　 infinity∅ :　∅ ∈ infinite
　　 infinity :　∀( X x : ZFSet　) → x ∈ infinite →　( x ∪ Select X (　λ y → x ≈ y )) ∈ infinite
　　 selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet　} →　( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈　Select X ψ )
　　 replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet　) →　( ψ x ∈　Replace X ψ )　

ってな感じ。Agda は高階関数型だから一階述語論理と違ってAxiom Schemeとか関係なく、任意の関数を含む公理を記述可能。

これをモデルが満たすかどうかをチェックにいきます。

順序数定義可能集合ODは単なる述語なので、こんな感じ。

　　record OD {n : Level}　: Set (suc n) where
　　　field
　　　　def : (x : Ordinal {n} ) → Set n

Agda で証明できない仮定の方は、o< が順序数の順序で、c< が集合の順序∈で、

　　postulate　　　
　　　od→ord : {n : Level} → OD {n} → Ordinal {n}
　　　ord→od : {n : Level} → Ordinal {n} → OD {n}
　　postulate　　　
　　　c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
　　　o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
　　　oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
　　　diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
　　　sup-od : {n : Level } → ( OD {n} → OD {n}) →　OD {n}
　　　sup-c< : {n : Level } → ( ψ : OD {n} →　OD {n}) → ∀ {x : OD {n}} → ψ x　c< sup-od ψ

これくらいです。Ordinal の方は泣くほど複雑になって、結構苦労したんですが、なんとか動いているみたい。

これで、pair/empty から始めて、regurarity, selection, union, extensionality　までできました。思ったより順調かな。
selection は分出公理とか subset とか呼ばれるものです。

Ordinal が複雑なのが残念すぎる。Union 公理の証明で順序数の osuc つまり、x ∪ {x} で

　　 y o< osuc x　→ x o< y → ⊥

を証明するのが Ordinal が正しくできているかにかかっていて厳しかったです。作り直しかと思ったよ。

残りは power set , infinity, replacement ですが、できるかな〜

　　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/ZF-in-agda/

来年のOS研究会

鬼が笑いますが、IT創造館が楽で良いんですけどね。那覇なので飲みに出るのは便利だし。いっそ、

　　懇親会はお酒抜きで安くして、あとは勝手に飲みに行け

でもいいのかも。

せっかくだから海が近い方がいいとか、北谷とか宜野湾のトロピカルビーチとか。そういえば、新しくできる浦添のは会議できる設備あるのかな。

いや、IT創造館が楽で良いです。ホテルとかはやっぱり大変。ホテルの方も儲けたいだろうけど、OS研究会は貧乏だからな。

琉大だったら会場費無料だし、(屋上に登れば)海も見れます。