前期の講義をやり遂げた
2019年の前期は数学の講義を担当することになって、えらい大変だった。特に自分は数学が専門じゃなくて、大学の数学の講義を受けた経験があまりないため、どう教えたものかとたいへん迷った。一応、数学自体は独学で勉強していたため何とかなったとは思いたいのだが、さすがに本職の先生には及ばないところもあるだろう。
講義内容的には計算の理論なのだが、せっかくだから、大阪大学の他の講義ではやっていないような面白い内容をやろうと思い、不完全性定理と型システムをやったが、これは本当に大変すぎた。おかげで、土日や帰ったあとからも講義資料の作成をしていたし、数学の証明だけではなくて、プログラミング課題の実装もしていたので時間がどれだけあってもたりなかった。大学はレジャーランドなので土日祝日もなくて大変である。レジャーランドに休園日はないのだ。
現在、講義の最終課題として単純型付きλ計算の型推論エンジンの実装に取り組んでもらっている。講義で得た数学の証明論の知識を、実際のプログラミングにまで活かせるので、大変ではあるがかなりの実力がつくのではないかと思う。
後期も講義をいくつか担当するので、また考えないと行けない。今の所、CPUキャッシュコヒーレンスや分散ハッシュテーブルのアルゴリズムを形式検証する講義と、パケットキャプチャを行い、自前で実装してもらった正規表現エンジンでフィルタリングする講義のようなものにしようかと思っているが、まだまだ未定である。前期の講義では、ネットワーク、プログラミング言語理論、数学基礎論、計算理論を行ったので、後期ではCPU、OS、システムプログラミング、分散コンピューティング、モデル検査、形式手法あたりを絡めて教えていきたい。しかし、分野が広すぎる。
サイバーセキュリティの講義と演習を行った
5月25〜26日にかけて大阪大学で高度サイバーセキュリティPBL Iという講義を行った（これも例のごとくProSecというコースの一環である）。講義と言っても講義が6割で演習が4割と言った配分である。この講義は自分以外に、情報通信研究機構から明石邦夫先生を招き講義してもらった。明石先生は、Interop Tokyoという日本最大のネットワークの展示会のネットワーク運用センター（通称NOC）で運用を行っているような人で、ガチでネットワークに詳しいので、かなり面白い話が聞けたと思う。
講義の内容は、ネットワークの基礎から学んで、最終的にOpenBSDのpfを設定してDMZのあるネットワークの構築を行うまでを目標にしている。1日目はネットワークの基本的な内容、いわゆるネットワークスペシャリストに出るような内容を講義し、その後学生同士でチームになってもらい、ウェブブラウザでURLを開いたときにスイッチやNAPTルータの内部で何が起きているかをプレゼンしてもらった。当初ネットワークは全然わからないと言っていた学生が、スイッチ内部のテーブルや、NAPTのアドレス変換について解説できるようになるのはなかなか凄いことではないだろうか。
2日目の講義ではネットワークスタックの実装方法や、radix treeを用いたルーティングテーブルのルックアップエンジンの実装方法といった内容の講義を行ったが、これは普通のネットワークの講義ではやらないような濃い内容になったと思う。また、OpenBSDのpfを使ったDMZネットワークの構築を行う演習の方だが、こちらも当初はBSDを使うのが初めてで、ましてやpfとは一体、という学生が大半だった。しかし、最終的には、完璧でないにしろpfでフィルタリングができるようになった学生がそれなりに居たため大変喜ばしい。
ネットワークの講義というと、いかんせん暗記科目になりがちで、暗記はしたけど実際問題いまいち良く分からないとなりがちだが、本講義では何故そうなっているか、実装はどうなっているかといった哲学と実際の仕組みを念入りに教え、さらにpfも使って演習したため、2日間で一気にネットワークセキュリティに詳しい人材が出来上がってしまった。
大学の講義は実社会で役に立たないと言われがちだが、これほど実社会に役に立つ講義もないのではないかと思う。準備がめちゃくちゃ大変だったが、無事に終わってよかった。終わって安堵するのもつかの間、そろそろ次の講義の準備をしないといけない。こんなに面白い内容が聞けて演習できるなんて（自画自賛）、大学はまことにレジャーランドである。
不完全性定理の理解不完全性
大阪大学に赴任してから半年たったぐらいの2019年2月頃に、離散数学と計算の理論という題目の講義を4月から担当することに決まった。その理由は、その講義を元々担当していた当時研究室の准教授だった先生が、他大学の教授へとご栄転されることが決まったからである。
自分はネットワークシステム、分散・P2Pコンピューティング、ネットワークセキュリティが専門でどちらかというと実装よりなので、数学はあまりやってこなかったのだが、今はプログラミング言語理論を習得するために論理学や計算モデルを勉強していたので引き受けることにした。この講義は大阪大学のProSecというコースを申し込むと、社会人でも受講することができるようになっている（コースは有料だけど）ので、詳細は「大阪大学 prosec」で検索してほしい。（現5月時点で申し込むと、秋からの受講になるだろうが）
プログラミング言語を真面目に初めた理由は、最近はネットワーク業界でもソフトウェア定義や、プログラマブルスイッチなどと言われているため、数年後にはプログラミング言語理論の知識が必要になるのではないかと漠然と思っていたからであった。実際に活かせるかどうかはこれからの研究にかかっているので、乞うご期待といったところである。
そんなこんなで講義を担当することが決まり慌ててシラバスを決めたのだが、自分の担当は以下のようにした。
4回で不完全性定理まで行くのはかなり駆け足な気がするが（2人の先生で15回なのでこんな感じに）、大阪大学の学生は優秀なので大丈夫だろう。問題は自分の方である。内容を決めたは良いが、勉強のし直しが大変だった。3月からは、家に帰ってからは数学の本を読むことに時間を使った気がする。今はゴールデンウィークだが、不完全性定理はめちゃくちゃ大変で、ゴールデンウィークの半分は不完全性定理で消えてしまった。なぜシラバスに入れたかと自分を恨んだりもしたものだ。ツライ。
不完全性定理を学ぶ上でいろいろな文献を参考にしたが、数年前に買った「コンピュータは数学者になれるのか？」という書籍がとてもためになった。しかし、この本は一般書の顔をしているが数学がある程度わかる人向けなので、誰得感が否めない。前半の1、2章で述語論理の導入から初めて不完全性定理まで行くというハイペースぶりである。自分はとてもためになったので、俺得ではあるのだが。まだ不完全性定理の理解は不完全なので、今後はもう少し落ち葉拾いをしていきたい。
コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ-
- 作者: 照井一成
- 出版社/メーカー: 青土社
- 発売日: 2015/02/24
- メディア: 単行本
- この商品を含むブログ (11件) を見る
この講義では簡単な原始帰納的関数をHaskellで実装したり、型付λ計算で簡単な型推論エンジンを実装したりもする予定なので、内容的にはかなり面白いのではないかと思う。特にうちは工学部なので、数学をプログラミングに活かせたほうが学生にもよいだろう。
他にも、大阪大学のProSecでは、ファイアウォール演習、レジスタマシンのエミュレータ実装演習、多層防御の演習なども自分が担当する予定なので、こちらも準備しないといけない。無事に乗り切りたいところである。
プログラミング言語と論理学の狭間にてさけぶけもの
情報科学をやってきたのだから、死ぬまでに一度自作のプログラミング言語を作ろうと思ったのが2016年後半ぐらいである。プログラミング言語とオペレーティングシステムは情報科学を志した者は誰もが一度は目指す道である（たぶん）。
しかし、思い立ったは良いが、プログラミング言語の研究は論理学を基礎としており、その当時は論理学のろの字もわからなかった。実際には、JAISTの学生時代に小野先生の数理論理学の講義を受けたのだが、その当時は「ANDとOR計算ね」ぐらいの認識しかなかったという体たらくであった。当時は大堀先生もJAISTでStandard MLの講義をしていたので、今にして思えば受講しておけばよかったと思う。
そんなこんなで基礎を習得するのに2年弱かかってしまって、今ようやく自作プログラミング言語の実装に取り掛かっているわけである。本報はプログラミングという情報科学にそびえ立つエベレスト、いやオリンポス山登頂を目指しているつもりが、論理学というジャングルへ踏み込むことになった結果得られた知見をまとめたものである。
論理学入り口
- 作者: 戸田山和久
- 出版社/メーカー: 名古屋大学出版会
- 発売日: 2000/10/10
- メディア: 単行本（ソフトカバー）
- 購入: 27人 クリック: 330回
- この商品を含むブログ (108件) を見る
『独習コンピュータ科学基礎 II 論理構造』と『論理学をつくる』は初学者におすすめしたい本である。論理学の教科書というと記号の羅列になりがちで、これがどう情報科学に生きていくのは分かりづらい部分がある。一方、『独習コンピュータ科学基礎 II 論理構造』の方は、論理学的な証明もしつつ、プログラムを証明するとはどういうことかや、プログラムで自動推論するにはどうするかなどを解説しており、論理学が情報科学にどう結びつくかが強くわかるようになっている。この『独習コンピュータ科学基礎 II 論理構造』はポートランド州立大学のコンピュータ科学基礎論の教科書であり、内容も大学の講義に耐えうるものだ。
『独習コンピュータ科学基礎 II 論理構造』は、論理学をどう使うかということが主題で、論理学そのものについてはあまり深くはない。例えば、演繹体系は自然演繹法のみ利用しており、様相論理や直観主義論理などの非古典的論理の解説はなく、演繹体系の健全性や完全性の証明はおざなりな感じは否めない。『論理学をつくる』では、情報科学に活かすというよりも、より論理学になった感じの書籍であるが、内容は大変明快で初学者にもわかりやすい。『独習コンピュータ科学基礎 II 論理構造』では触れられていなかった様相論理や直観主義論理も解説されている。
数学や論理学を専攻するのでなければ、この2冊、もしくはどちらかを抑えておけばよいのではないかと思う。つまり、『独習コンピュータ科学基礎 II 論理構造』∨『論理学をつくる』である。
論理学の奥地へ
自分は『情報科学における論理』は、JAIST時代に小野先生の数理論理学の講義教科書として購入した。本書は『独習コンピュータ科学基礎 II 論理構造』に比べるとずっと理論よりとなり、プログラミング言語などの関わりよりも、論理そのものを学ぶ、まさに数理論理学という本である。内容は、古典的論理から様相論理、直観主義論理、λ計算まで幅広く書かれている。
『論理と計算のしくみ』は『情報科学における論理』よりもさらに広い範囲をカバーしている。例えば、ゲーデルの不完全性定理や、型付きλ計算と型推論まで含んでいる。しかし、本書は極めて理論的であるため、論理学の応用を目指す人にとっては幾分難解な箇所もあるように感じた。例えば、無限の論理式を含む式とか、無限という言葉がカジュアルに出てきて抽象度がかなりあがっている。
『情報科学における論理』と『論理と計算のしくみ』は、論理学を応用として使ってみるうちに、その理論的背景を知りたくなった場合に読めばよいのではないかと思う。例えば、モデル検査の理論的背景にはクリプキ構造や様相論理があり、背景知識までを正確に理解するにはこれら書籍を参考にするしか無い。
そしてプログラミング言語へ
- 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
- 出版社/メーカー: オーム社
- 発売日: 2013/03/26
- メディア: 単行本（ソフトカバー）
- クリック: 68回
- この商品を含むブログ (11件) を見る
Programming Distributed Computing Systems: A Foundational Approach (The MIT Press) (English Edition)
- 作者: Carlos A. Varela
- 出版社/メーカー: The MIT Press
- 発売日: 2013/05/31
- メディア: Kindle版
- この商品を含むブログを見る
プログラミング言語の定番本として挙げられる本といえば『型システム入門』、通称TaPLがあるが、個人的には論理学の教科書で基礎を学んだあとに読んだほうがわかりやすいのではないかと思う。例えば、本書の22章 型再構築には単一化と呼ばれる操作のアルゴリズムが載っており、単一化アルゴリズムは『独習コンピュータ科学基礎 II 論理構造』、『情報科学における論理』、『論理と計算のしくみ』にも載っているが、『型システム入門』の説明が一番わかりにくい。
『Programming Distributed Computing Systems: A Fundamental Approach』は英語の本だが、λ計算、π計算、アクターモデル、Join計算、アンビエント計算など並行計算モデル書かれた良書である。λ計算の説明は本書が一番わかりやすかった。前半の理論部分の解説は良いのだが、後半の実装部分がツール類が古くて動かないものばかりなので読まなくても良いかもしれない。
以上が2年弱勉強して得られたざっくりとした知見である。自分は論理学の専門家では無く、あくまでも論理学のユーザであるため異なっている箇所もあるかもしれないが、なにかの役に立つかもしれないと思い簡単にまとめた。それでは良いハッキングライフを。
ネットでホテルを誤って当日予約してしまい1分後に即キャンセルするもキャンセル料100%請求された件
状況
- 2月前に楽天トラベルで来週のホテルの予約をしようとしたら、間違って当日に京王プレッソインの予約を取得してしまった
- あわてて1分後に予約キャンセルする
- 2月後の今になってキャンセル料100%全額請求されていることに気がついた
結論から言うと、楽天トラベルから予約しするも誤って当日予約してしまった場合は、ホテルに直接電話するとキャンセル料請求取り消しのチャンスが有ったようだ。
はじめに、京王プレッソインへ問い合わせてみた。
京王プレッソインの説明、その１
- システム的に無理
- 楽天トラベル側で無理と言っているので無理
楽天トラベル側で無理と言っていたので、楽天トラベルへ問い合わせてみた。
楽天トラベルの説明
- 楽天トラベルでは、キャンセル料については関与しない
- システム的には可能なので、ホテル側では可能
楽天トラベルでは可能と言われ、ホテル側と説明が食い違っていたので、再度ホテルに問い合わせてみた。
京王プレッソインの説明、その２
- システム的に無理
- 楽天トラベルで操作はできない
やはり説明が食い違っていたので、楽天トラベルに確認したが可能であると聞いたと問い合わせた。もう一度、楽天トラベル側へ問い合わせ、出来ると確認されればキャンセル料請求取消して頂けるという事でよいかと確認したら、担当が変更になる。
- 楽天トラベルのシステムで取り消し出来るかどうかは問題ではない
- 規約上、すでに契約は終えているので無理
- 1分後に取り消していようが無理なものは無理
- ただし、そういう場合は当日に連絡してくれれば可能であったかもしれない
という説明を受けた。規約上無理というのと、当日に連絡ならキャンセル料請求取り消し可能であるというのは矛盾している気もするが、どうも、間違って予約したらホテル側へ即電話を入れたほうが良いらしい。
最後に、消費者センターへ問い合わせてみた。
消費者センターの説明
- インターネットで契約を完了してしまったら無理
- 自分で契約に同意してしまっているから難しい
という説明を受けた。どうも、1万円払うしかないようだ。サンクコストであることが確定し、これ以上考えてもどうしようもないことであることが判明した。
