アカデミックごっこ

data functorを構成

Coq でやるには型合わせがとてもつらい.とてもバカな定義だができた. いずれ polynomial functor をもうちょい賢く扱う必要があるな.別に各 polynomial functor の initial algebra の standard な実装を作って仕舞えば良いだけで,具体的な Coq の実デー…

半年前の自分の論文

をよく読んで校正しろとか,もはやなんか罰ゲーム感ある.

燃えたらしい

先日行われた某研究会に某バカが行ってたが,予想通り燃えたらしい.野次馬として行きたかったなあ….

自分の KK 概要が書けない

他人の概要については散々文句言ったものの,自分のは書けない….どうごまかしたもんか. てか,圏論の初歩ぐらい必修講義で(以下略

夢に満ちた処理系

FPGA を載せたマシン上に載せた VM への処理系と,プログラムが走っているとき,動的に FPGA も書き換えて計算に使っていくマシンとか,トランスフォーマーみたいでカッコ良い. だがしかし.研究室がなくなる前に version 1.0 は出るのだろうか…?

無事炎上なしで終了?

心配していた KK 司会は,特に炎上騒ぎもなく無事終了.炎上すると嫌だったので,質問は事前に練っていた 4 つのうち,答えやすそうな 2 つを.なんか誤魔化された気もするけど,深追いすると後でツイッタで色々言われそうなので自重. ほかの発表は全然聞い…

未知帰納法

path induction よくわからんなあ.なんで とか みたいな argument を引き摺り回しているのかよくわからん. 帰納法原理て一般にどうやって理解すれば良いんだろうか.意外と普通の polynomial functor をテキトーに とかに持ち上げて, への catamorphism …

無事採録

この前出していた論文が採録された.これで卒論が浮かばれる.改善のための付帯意見も穏やかな感じだ. だがしかし.高階の系ってなんのことだろう.話に聞いていた 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 ぐらい散歩したりした.適当に色々話しつつ散歩するの楽しいので,春先に散歩部でもやりませんか.んまあ普段は歩…