15時10分より16時40分まで。partial recursive functionをMartin-Lof type theoryで表現する。inductive definitionをtypeで表現するとき、普通にやるとstrictlyにpositiveなindexed definition でなくなるものが出てくるので、”indexed inductive recursive…

起床は8時。晴れてはいるが、大分寒い。落ち葉が目立つようになってきた。午前中は論文修正、合間に雑用。午後も論文の続き。今日は早めに帰宅、洗濯をし、夕食の餃子をCと一緒に詰める。 健康診断の結果、コレステロール値は減少傾向、昨年は要注意を言い渡…