先日、友人にこのPDFリーダーが有効な領域についての感想をもらったのですが、
「予めどういう単語が重要かが分かっているケース」、
とのことでした。
漫然と今までは教科書や論文の類でも使用していたのですが、これで使うと良い状況が一つ、明確になりました。
「一度読んだことのある教科書を、再度復習のために読む」
という状況です。
今回は実況(自分の心の声)ありの動画をご紹介します。（※１）
次回は、前回ご紹介した、Agdaというプログラミング言語で自然数と足し算の世界を作る動画を実況付きでご紹介する予定です。
（※１）対象は、Robert Harperさんという計算機科学の先生がオレゴンプログラミングサマースクール(OPLSS)の2014年の講義で使われた資料(https://www.cs.uoregon.edu/research/summerschool/summer14/rwh_notes/notes_week1.pdf)になります。
公式HPに動画が公開されています（https://www.cs.uoregon.edu/research/summerschool/summer14/curriculum.html）。
この講義資料（PDF）は、元々はカーネギーメロン大でなされた別講義の講義録のようです。このHarperさんの講義は、CoqやAgdaの理論的背景について丁寧に教えてくれるという内容のようです。CoqやAgdaはゲームっぽく進められちゃうけど、ちゃんと理論的背景も学びましょうということを動画で述べられていました。
自分がこの動画を作成した時の状況は、
(1) Harperさんの2014年の講義の第一回目を見た。
(2) よくわからない部分があったから、この講義録（pdf）を読んでみた。
(3) まだよくわからなかったので、再度読んでみようとした（★ここ）
となっています。
OPLSSは講義時の動画が無料で公開されていて、そこで自分はAgdaをEmacsでプログラミングするやり方を覚えました。具体的には2013年のDan LicataさんとIan Voyseyさんの講義(http://www.cs.cmu.edu/~drl/teaching/oplss13/)です。
内容的には、自分が紹介しようとしている簡単な数学の公式の証明と違って、計算機科学を専門とする人向けの難しい内容になっています。
自分は全部はまだ理解できていませんが、AgdaとHoTT（Homotopy Type Theory）についての今後の可能性を感じさせてくれる素晴らしい講義だと思います。
OPLSSは他にもAgdaの開発者の一人である Ulf Norellさんの講義も2014年にあります。