アカデミックごっこ

無事採録

この前出していた論文が採録された.これで卒論が浮かばれる.改善のための付帯意見も穏やかな感じだ. だがしかし.高階の系ってなんのことだろう.話に聞いていた n 重再帰によって定義される関数の話のことだろうか.ちょっと文献を探さないといけないか…

* と ?

* と ? のような,パターン検索するときに使う文字のことを一般的に「ワイルドカード」と呼ぶと思っていたら,若干違うらしい.Wikipedia だとそう書いているっぽいのだが… ワイルドカード (情報処理) - Wikipedia その筋に詳しい人(?)によると,要するに「…

2回目の感想

某アレが2回目.以下感想. 「前の手順を考慮したら,手のラベリングの精度が良くなる」という,当たり前っちゃあ当たり前の結果なので,もうちょっと踏み込んだ考察が聞けると面白かったなと思った.考慮する盤面の範囲が大きすぎると精度が悪くなるという…

名無し項に直しているだけ

なんか 1 日中寝ていた気がする. 単純型付きラムダ計算の CCC (Cartesian Closed Category) の意味論が,地味に Semantics of Programming Languages: Structures and Techniques の圏論の章に載ってて,読み直しているんだけど, Var と Abs と App しかな…

手巻き寿司2回目

2017 年 12 月 31 日に続いて,手巻き寿司 2 回目.今回は人が多くてたいへんに賑やか.やっぱりトロがないと満足度がかなり下がるな. 閑話休題.情報幾何とか,話だけ聞くと面白そうなんだけど,統計とか機械学習系統の素養がないので結構道のりが遠そうな…

Coq の Reference Manual が一新されてた

連休の飛び石部分1日目.連休といっても論文書かなきゃいけないので実質休みなし.まあ,どうでもいいことで時間取られるよりよっぽど有意義なので問題ない. 閑話休題.今日まで気づかなかったが, Coq の Reference manual のデザインが一新されている.お…

1周目無事終わり?

1 周目の勤務が無事終了.めでたしめでたし? 様子がわかっているので 2 周目以降は楽だろう. その副作用かなんなのかはよく知らないけど,ネットワークの仕組みがちょっとわかってきた.というか,どういう態度で理解しようとすればよいのかなんとなく理解…

map (f . g) = (map f) . (map g)

ゼミ中にちょっと話題になったのだが,Haskell の map は,任意の関数 f, g に対して, map (f . g) = (map f) . (map g) が成り立つ.んで,Bird 曰く,右辺よりも左辺の方が若干早いでしょ,と.たしかに eagar evaluation だったら,そうかもねという気が…

今年度初仕事?

ある意味で今年度初仕事.特にこれという話もなく終了.ちょっと手を抜きすぎたかもしれないが,まあ誤差の範囲.こういうときに,普段から資料を収集しておいてよかったとなるな. 閑話休題.とある Web サーバーの管理者が git を用意してくれているのだが…

4年間ありがとう for 家

なんだかんだで無事に引越しが終わり, 4 年間住んだ家を出ることに.空になった家を見るのはさみしいものである (が,これからの地獄を考えると涙も出ないが…). 思い返せば,4 年前に,札幌から身一つで,友達もいない知らない土地に来た自分を受け入れて…

電車プログラミング

色々とあった 1 日だった.午前中は "某所" で焼肉.外で BBQ 的なことをするという話もあったが,ちょっとめんどいとかなんとかいう理由で流れて,結局室内で肉を焼くに止まった. ところで,BBQ と焼肉の違いをいまだに理解していない.陽キャがやれば BBQ…

最終講義

弊学科名物,某 S 先生の最終講義があった.S 先生は,形式言語の帰納推論の人,というようなイメージがあったのだが,それだけではなく,検索についても色々な研究をされていたらしい.というか,一番驚いたのは,倉田先生の弟子でもあるのね.有川先生の弟…

某学会2018 2日目

昨日夜遅くまで(というか朝早くまで?)飲み部屋にいて,まあここに書きにくい話を聞きながらいろいろ盛り上がっていて疲れた.ねむい.ほとんど意識が朦朧としていた.ので,発表とかよく覚えていないのだが,そんな中での感想. モデル検査よくわからん.…

某学会2018 1日目

昨日は思いがけず到着が遅くなって,見られなくなってしまったので,朝早くから起きてホテルの周りを歩き回る. 90 m ぐらいの山を登って?,米子城跡.朝の運動としてちょうどよい. んで,そんなこんなで朝飯.スーパーホテルの朝食バイキングうまいよね. …

試問の傾向と対策メモ

色々な卒論の第1章を読んでもらい,諸々修正をかける.第1章だけは絶対に理解させる必要があるから…. んで,自分用のメモも兼ねて,卒論発表に向けてやるべきだと思ったことをまとめておく. 卒論の第1章(はじめに)と終章(まとめ)は,用語の定義・ロジ…

写真

某所の人からTwitterで呼び出されたので,「あれ俺の荷物なんか置いたまんまだっけ」と思って焦って某所に行くと,「集合写真をとってほしい」といわれる.まあミーティング中だったが別に自分のターンじゃないからいいかと思って,とりあえず了承.感想:な…

気軽に引き算するな

昼から晩までずっと,研究で開発したライブラリとその使用例を整理していた.まあ,結構綺麗な使用例ができたでしょう. ところで,Ackermann関数が原始再帰的でないことを証明するときに使う Lemma ack_inc : forall c1 c2 : nat , exists c3 : nat , foral…

家探し part 2

午前中は昨日に引き続き家探しその2.当たり前だけど,家賃高い家ほどまあ綺麗だわな.それにしても,あそこの立地は良いな.CoCo壱が近くにあるのは強い. 午後からは平常運転.といいつつ,特に何も仕事せずダラダラ過ごしてしまった感じもあるが,諸々疲…

お蔵入りプログラムを徹夜して書く

寝てない.というのも,なぜか行列乗算だのLU分解だのというC言語のプログラムを書いていた.まあこの程度のプログラムならCでもストレスにはならない.結局このプログラムは日の目を見ることなく役目を終えたのでバカみたいだが,まあ楽しかったのでよしと…

英語化

昼ごろ起床? 論文(といっても short paper だけんども)の abstract 英語化.久しぶりに英語を書いたので疲れる.といっても書いたのは実質私じゃないみたいなもんだが….まあ英語は今後の課題ということで(汗 高校の時から英語は苦手だったもんなあ.な…

さらに Coq

朝6時ごろ起床. 朝は線形代数のお話を聞く.絶賛 Coq に没頭中なので,かなり細かいところばかりに目がいってしまいよろしくない.が,まあ 1 年生相手だったらちょっとうるさいぐらい論理の訓練をしてもらった方が良いだろうということで許してほしい. ん…

Bool型を使った古典命題論理の埋め込み?

昼ごろ起床.昼夜逆転を半回転させるのに成功した. んで,本題.Coq というか Gallina の if-then-else を使った証明が扱いにくくて悩ましいが,if の後の bool 値は,中身の構造に立ち入らなくても, true だった場合と false だった場合に場合分けしてし…

昼夜逆転を巻き戻すために

とりあえず証明の目処がたったので[要出典],昼夜逆転を巻き戻すためにあとはほぼ一日寝ていた. 途中,うどんを食べるために, N さんと 5km ぐらい散歩したりした.適当に色々話しつつ散歩するの楽しいので,春先に散歩部でもやりませんか.んまあ普段は歩…

オーダー表記

日付がわかってからまだ寝てない.今から寝る.多分今日中に起きないので寝る前に日記を書いてしまう. 日付が変わるまでは論文書きと,追加のデモ実装.以外に捗る. んで,午後は某所にて某発表を聞いた.んで,その発表の本質とはあまり関係ないが,そこ…

わりかしおもしろい定理をみつける

Twitter でだべっていたら(論文書け),わりかし面白い定理を見つける. 人が,「全員が同じ帽子の色ということはない」という条件のもとで,赤・白の帽子をかぶって一列に並ぶ.このとき,各人は,自分より前の人の帽子の色は見えるが,自分の防止の色はみ…

初日の出とモナド

初日の出を拝むために,Kさんの車で阿蘇山につれていってもらう.ここを 03:00 ごろ出発して,5:30 ごろつく.まだまだ暗い. 寒すぎるので一旦車に戻り,N さんと「モナドは単なる自己函手の圏におけるモノイド対象だよ。何か問題でも?」という話をした.…

アレな研究室

11:00頃起床.昼は用事を済ませがてら散歩,無印良品まで散歩して金を浪費しすぎる.そのあとはしばらく研究. Initial Algebra と catamorphism をなんとなく理解したので,それを利用した program calculation の話を飛ばしてさっさと allegory の章に入っ…

焼肉

結局寝落ちして11時頃起床.昼飯はローストビーフ丼.久しぶりにsb研のnkmr君に会う. 「某大人気講義を受けてたら形式言語理論に興味が出てきた」という珍しい後輩がいるので,そりゃ頼もしいことだと,とりあえずオートマトンとか計算理論関係の本を無理や…

Catamorphism

結局11時頃起床.昨日走り過ぎた分の筋肉痛が痛い.昼間はちょっとした打ち合わせで,Ruby とか Rails とか書くことになるねー,という話し.まあネットワーク絡むプログラム全然わからんので,ちょうど良い機会だ.そのあとは久しぶりにずっと自分の数学と…

発表

-02:00 (要するに前日の 22:00) に起床し,そのまま起き続ける.久しぶりに早朝 7 km 走る.ちょっと足下が暗いので怖い. 割と朝早くに発表.質問はごもっともなのが 2 つぐらいと,よくわからんのが 1 つとんできた.よくわからんのは結局質問の前提が色々…