16:00-17:00 0とsuccessorとrecursorを持つsimple typed calculusをprimitive recursive functionalの中に埋め込むGandy translationを使って、strong normalizationの証明においてnormal formにいきつくまでのreductionの列の長さのupper boundを求める。up…

本日は出張。冷たい風が強く吹く。湿度が高く、大粒の雨が降ったり日がさしたりを繰り返す。また右ふくらはぎが寝ている間に攣る。起床は11時。読書。14時に家を出る。談話会と某用件、19時に帰宅、夕食はもらい物のアナゴとしらす。読書などをして26時に寝…