談話会
16:00-17:00
0とsuccessorとrecursorを持つsimple typed calculusをprimitive recursive functionalの中に埋め込むGandy translationを使って、strong normalizationの証明においてnormal formにいきつくまでのreductionの列の長さのupper boundを求める。upper boundそのものよりも、ruler orderingをprfのなかに定めるなど、技法としての面白さに注目して欲しい、とのこと。確かに構成は面白かったです。
