memo

今日のメモ。
Sg先生と話して直観主義と計算論は相性が良い、直観主義で証明が出来れば、計算可能であると聞く。
直観主義の証明のフォーマットさえきっちり決めれば、コンパイラ作って計算機に渡せて実際に計算出来るということか。しかも止まらずに正しく計算出来る。どっかに参考文献あるだろうから探すこと。